Physlib.Electromagnetism.Vacuum.HarmonicWave — Physlib

Imports

/-
Copyright (c) 2025 Zhi Kai Pong. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Zhi Kai Pong, Joseph Tooby-Smith
-/
module

public import Physlib.Electromagnetism.Vacuum.IsPlaneWave

Harmonic Wave in Vacuum

i. Overview

In this module we define the electromagnetic potential for a monochromatic harmonic wave travelling in the x-direction in free space, and prove various properties about it, including that it satisfies Maxwell's equations in free space, that it is a plane wave.

We work here in a general dimension d so we use the magnetic field is the form of a matrix rather than a vector.

ii. Key results

harmonicWaveX : Definition of the electromagnetic potential for a harmonic wave travelling in the x-direction.

harmonicWaveX_isExtrema : The harmonic wave satisfies Maxwell's equations in free space.

harmonicWaveX_isPlaneWave : The harmonic wave is a plane wave.

harmonicWaveX_polarization_ellipse : The polarization ellipse equation for the harmonic wave.

iii. Table of contents

A. The electromagnetic potential for a harmonic wave

A.1. Differentiability of the electromagnetic potential

A.2. Smoothness of the electromagnetic potential

B. The scalar potential

C. The vector potential

C.1. Components of the vector potential

C.2. Space derivatives of the vector potential

D. The electric field

D.1. Components of the electric field

D.2. Spatial derivatives of the electric field

D.3. Time derivatives of the electric field

D.4. Divergence of the electric field

E. The magnetic field matrix for a harmonic wave

E.1. Components of the magnetic field matrix

E.2. Space derivatives of the magnetic field matrix

F. Maxwell's equations for a harmonic wave

G. The harmonic wave is a plane wave

H. Polarization ellipse of the harmonic wave

iv. References

@[expose] public section

A. The electromagnetic potential for a harmonic wave

@[simp]
lemma harmonicWaveX_inl_zero {d} (𝓕 : FreeSpace) (k : ℝ) (E₀ : Fin d → ℝ) (φ : Fin d → ℝ)
    (x : SpaceTime d.succ) :
    harmonicWaveX 𝓕 k E₀ φ x (Sum.inl 0) = 0 := byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝx:SpaceTime d.succ⊢ (harmonicWaveX 𝓕 k E₀ φ).val x (Sum.inl 0) = 0
  simp [harmonicWaveX]All goals completed! 🐙

@[simp]
lemma harmonicWaveX_inr_zero {d} (𝓕 : FreeSpace) (k : ℝ) (E₀ : Fin d → ℝ) (φ : Fin d → ℝ)
    (x : SpaceTime d.succ) :
    harmonicWaveX 𝓕 k E₀ φ x (Sum.inr 0) = 0 := byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝx:SpaceTime d.succ⊢ (harmonicWaveX 𝓕 k E₀ φ).val x (Sum.inr 0) = 0
  simp [harmonicWaveX]d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝx:SpaceTime d.succ⊢ (match Sum.inr 0 with
  | Sum.inl 0 => 0
  | Sum.inr ⟨0, ⋯⟩ => 0
  | Sum.inr ⟨i.succ, h⟩ =>
    -E₀ ⟨i, ⋯⟩ / (𝓕.c.val * k) *
      sin (k * (𝓕.c.val * (x (Sum.inl 0) / 𝓕.c.val) - (SpaceTime.space x).val 0) + φ ⟨i, ⋯⟩)) =
  0
  rflAll goals completed! 🐙

A.1. Differentiability of the electromagnetic potential



lemma harmonicWaveX_differentiable {d} (𝓕 : FreeSpace) (k : ℝ)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) :
    Differentiable ℝ (harmonicWaveX 𝓕 k E₀ φ) := byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝ⊢ Differentiable ℝ (harmonicWaveX 𝓕 k E₀ φ).val
  rw [← Lorentz.Vector.differentiable_applyd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝ⊢ ∀ (i : Fin 1 ⊕ Fin d.succ), Differentiable ℝ fun x => (harmonicWaveX 𝓕 k E₀ φ).val x id:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝ⊢ ∀ (i : Fin 1 ⊕ Fin d.succ), Differentiable ℝ fun x => (harmonicWaveX 𝓕 k E₀ φ).val x i]d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝ⊢ ∀ (i : Fin 1 ⊕ Fin d.succ), Differentiable ℝ fun x => (harmonicWaveX 𝓕 k E₀ φ).val x i
  intro μd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝμ:Fin 1 ⊕ Fin d.succ⊢ Differentiable ℝ fun x => (harmonicWaveX 𝓕 k E₀ φ).val x μ
  match μ with
  | Sum.inl 0 =>d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝμ:Fin 1 ⊕ Fin d.succ⊢ Differentiable ℝ fun x => (harmonicWaveX 𝓕 k E₀ φ).val x (Sum.inl 0) simpAll goals completed! 🐙
  | Sum.inr ⟨0, h⟩ =>d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝμ:Fin 1 ⊕ Fin d.succh:0 < d.succ⊢ Differentiable ℝ fun x => (harmonicWaveX 𝓕 k E₀ φ).val x (Sum.inr ⟨0, h⟩) simpAll goals completed! 🐙
  | Sum.inr ⟨Nat.succ i, h⟩ =>d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝμ:Fin 1 ⊕ Fin d.succi:ℕh:i.succ < d.succ⊢ Differentiable ℝ fun x => (harmonicWaveX 𝓕 k E₀ φ).val x (Sum.inr ⟨i.succ, h⟩)
    simp [harmonicWaveX]d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝμ:Fin 1 ⊕ Fin d.succi:ℕh:i.succ < d.succ⊢ Differentiable ℝ fun x =>
  -E₀ ⟨i, ⋯⟩ / (𝓕.c.val * k) * sin (k * (𝓕.c.val * (x (Sum.inl 0) / 𝓕.c.val) - (SpaceTime.space x).val 0) + φ ⟨i, ⋯⟩)
    fun_propAll goals completed! 🐙

A.2. Smoothness of the electromagnetic potential



lemma harmonicWaveX_contDiff {d} (n : WithTop ℕ∞) (𝓕 : FreeSpace) (k : ℝ)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) :
    ContDiff ℝ n (harmonicWaveX 𝓕 k E₀ φ) := byd:ℕn:WithTop ℕ∞𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝ⊢ ContDiff ℝ n (harmonicWaveX 𝓕 k E₀ φ).val
  rw [← Lorentz.Vector.contDiff_applyd:ℕn:WithTop ℕ∞𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝ⊢ ∀ (i : Fin 1 ⊕ Fin d.succ), ContDiff ℝ n fun x => (harmonicWaveX 𝓕 k E₀ φ).val x id:ℕn:WithTop ℕ∞𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝ⊢ ∀ (i : Fin 1 ⊕ Fin d.succ), ContDiff ℝ n fun x => (harmonicWaveX 𝓕 k E₀ φ).val x i]d:ℕn:WithTop ℕ∞𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝ⊢ ∀ (i : Fin 1 ⊕ Fin d.succ), ContDiff ℝ n fun x => (harmonicWaveX 𝓕 k E₀ φ).val x i
  intro μd:ℕn:WithTop ℕ∞𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝμ:Fin 1 ⊕ Fin d.succ⊢ ContDiff ℝ n fun x => (harmonicWaveX 𝓕 k E₀ φ).val x μ
  match μ with
  | Sum.inl 0 =>d:ℕn:WithTop ℕ∞𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝμ:Fin 1 ⊕ Fin d.succ⊢ ContDiff ℝ n fun x => (harmonicWaveX 𝓕 k E₀ φ).val x (Sum.inl 0) simp [harmonicWaveX]d:ℕn:WithTop ℕ∞𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝμ:Fin 1 ⊕ Fin d.succ⊢ ContDiff ℝ n fun x => 0; fun_propAll goals completed! 🐙
  | Sum.inr ⟨0, h⟩ =>d:ℕn:WithTop ℕ∞𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝμ:Fin 1 ⊕ Fin d.succh:0 < d.succ⊢ ContDiff ℝ n fun x => (harmonicWaveX 𝓕 k E₀ φ).val x (Sum.inr ⟨0, h⟩) simp [harmonicWaveX]d:ℕn:WithTop ℕ∞𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝμ:Fin 1 ⊕ Fin d.succh:0 < d.succ⊢ ContDiff ℝ n fun x =>
  match Sum.inr 0 with
  | Sum.inl 0 => 0
  | Sum.inr ⟨0, ⋯⟩ => 0
  | Sum.inr ⟨i.succ, h⟩ =>
    -E₀ ⟨i, ⋯⟩ / (𝓕.c.val * k) * sin (k * (𝓕.c.val * (x (Sum.inl 0) / 𝓕.c.val) - (SpaceTime.space x).val 0) + φ ⟨i, ⋯⟩); fun_propAll goals completed! 🐙
  | Sum.inr ⟨Nat.succ i, h⟩ =>d:ℕn:WithTop ℕ∞𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝμ:Fin 1 ⊕ Fin d.succi:ℕh:i.succ < d.succ⊢ ContDiff ℝ n fun x => (harmonicWaveX 𝓕 k E₀ φ).val x (Sum.inr ⟨i.succ, h⟩)
    simp [harmonicWaveX]d:ℕn:WithTop ℕ∞𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝμ:Fin 1 ⊕ Fin d.succi:ℕh:i.succ < d.succ⊢ ContDiff ℝ n fun x =>
  -E₀ ⟨i, ⋯⟩ / (𝓕.c.val * k) * sin (k * (𝓕.c.val * (x (Sum.inl 0) / 𝓕.c.val) - (SpaceTime.space x).val 0) + φ ⟨i, ⋯⟩)
    fun_propAll goals completed! 🐙

B. The scalar potential

The scalar potential of the harmonic wave is zero.

@[simp]
lemma harmonicWaveX_scalarPotential_eq_zero {d} (𝓕 : FreeSpace) (k : ℝ)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) :
    (harmonicWaveX 𝓕 k E₀ φ).scalarPotential 𝓕.c = 0 := byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝ⊢ scalarPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) = 0
  ext xd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝx:Timex✝:Space d.succ⊢ scalarPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) x x✝ = 0 x x✝
  simp [harmonicWaveX, scalarPotential]d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝx:Timex✝:Space d.succ⊢ (SpaceTime.timeSlice 𝓕.c) (fun x => 0) x x✝ = 0
  rflAll goals completed! 🐙

C. The vector potential

C.1. Components of the vector potential

              @[simp]
lemma harmonicWaveX_vectorPotential_zero_eq_zero {d} (𝓕 : FreeSpace) (k : ℝ)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ) :
    (harmonicWaveX 𝓕 k E₀ φ).vectorPotential 𝓕.c t x 0 = 0 := byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0 = 0
  simp [harmonicWaveX, vectorPotential, SpaceTime.timeSlice]d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ (match Sum.inr 0 with
  | Sum.inl 0 => 0
  | Sum.inr ⟨0, ⋯⟩ => 0
  | Sum.inr ⟨i.succ, h⟩ => -E₀ ⟨i, ⋯⟩ / (𝓕.c.val * k) * sin (k * (𝓕.c.val * t.val - x.val 0) + φ ⟨i, ⋯⟩)) =
  0
  rflAll goals completed! 🐙lemma harmonicWaveX_vectorPotential_succ {d} (𝓕 : FreeSpace) (k : ℝ)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : Fin d) :
    (harmonicWaveX 𝓕 k E₀ φ).vectorPotential 𝓕.c t x i.succ =
    - E₀ i * 1 / (𝓕.c * k) * Real.sin (k * (t.val * 𝓕.c - x 0) + φ i) := byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ =
  -E₀ i * 1 / (𝓕.c.val * k) * sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)
  simp [harmonicWaveX, vectorPotential, SpaceTime.timeSlice, Fin.succ]d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ sin (k * (𝓕.c.val * t.val - x.val 0) + φ i) = sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i) ∨ E₀ i = 0 ∨ k = 0
  leftd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ sin (k * (𝓕.c.val * t.val - x.val 0) + φ i) = sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)
  ring_nfAll goals completed! 🐙lemma harmonicWaveX_vectorPotential_succ' {d} (𝓕 : FreeSpace) (k : ℝ)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : ℕ)
    (hi : i.succ < d.succ) :
    (harmonicWaveX 𝓕 k E₀ φ).vectorPotential 𝓕.c t x ⟨i.succ, hi⟩ =
    - E₀ ⟨i, byOpticalMedium:Sort ?u.2OM:OpticalMediumd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:ℕhi:i.succ < d.succ⊢ i < d grindAll goals completed! 🐙⟩ * 1 / (𝓕.c * k) * Real.sin (k * (t.val * 𝓕.c - x 0) + φ ⟨i, byOpticalMedium:Sort ?u.2OM:OpticalMediumd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:ℕhi:i.succ < d.succ⊢ i < d grindAll goals completed! 🐙⟩) := byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:ℕhi:i.succ < d.succ⊢ (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩ =
  -E₀ ⟨i, ⋯⟩ * 1 / (𝓕.c.val * k) * sin (k * (t.val * 𝓕.c.val - x.val 0) + φ ⟨i, ⋯⟩)
  simp [harmonicWaveX, vectorPotential, SpaceTime.timeSlice]d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:ℕhi:i.succ < d.succ⊢ sin (k * (𝓕.c.val * t.val - x.val 0) + φ ⟨i, ⋯⟩) = sin (k * (t.val * 𝓕.c.val - x.val 0) + φ ⟨i, ⋯⟩) ∨
  E₀ ⟨i, ⋯⟩ = 0 ∨ k = 0
  leftd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:ℕhi:i.succ < d.succ⊢ sin (k * (𝓕.c.val * t.val - x.val 0) + φ ⟨i, ⋯⟩) = sin (k * (t.val * 𝓕.c.val - x.val 0) + φ ⟨i, ⋯⟩)
  ring_nfAll goals completed! 🐙

C.2. Space derivatives of the vector potential


@[simp]
lemma harmonicWaveX_vectorPotential_space_deriv_succ {d} (𝓕 : FreeSpace) (k : ℝ)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (j : Fin d)
    (i : Fin d.succ) :
    Space.deriv j.succ (fun x => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x i) x
    = 0 := byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di:Fin d.succ⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i) x = 0
  match i with
  | 0 =>d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di:Fin d.succ⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0) x = 0 simpAll goals completed! 🐙
  | ⟨Nat.succ i, hi⟩ =>d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succ⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0
    have transverse_deriv_eq_zero : ∀ (g : ℝ → ℝ), Differentiable ℝ g →
        Space.deriv j.succ (fun y => g (y 0)) x = 0 := byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di:Fin d.succ⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i) x = 0d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_eq_zero:∀ (g : ℝ → ℝ), Differentiable ℝ g → Space.deriv j.succ (fun y => g (y.val 0)) x = 0⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0
      intro g hgd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succg:ℝ → ℝhg:Differentiable ℝ g⊢ Space.deriv j.succ (fun y => g (y.val 0)) x = 0d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_eq_zero:∀ (g : ℝ → ℝ), Differentiable ℝ g → Space.deriv j.succ (fun y => g (y.val 0)) x = 0⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0
      rw [Space.deriv_eq,d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succg:ℝ → ℝhg:Differentiable ℝ g⊢ (fderiv ℝ (fun y => g (y.val 0)) x) (Space.basis j.succ) = 0d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succg:ℝ → ℝhg:Differentiable ℝ g⊢ (fderiv ℝ g (x.val 0) ∘SL fderiv ℝ (fun y => y.val 0) x) (Space.basis j.succ) = 0d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_eq_zero:∀ (g : ℝ → ℝ), Differentiable ℝ g → Space.deriv j.succ (fun y => g (y.val 0)) x = 0⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0 show (fun y : Space d.succ => g (y 0)) = g ∘ (fun y => y 0) from rfl,d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succg:ℝ → ℝhg:Differentiable ℝ g⊢ (fderiv ℝ (g ∘ fun y => y.val 0) x) (Space.basis j.succ) = 0d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succg:ℝ → ℝhg:Differentiable ℝ g⊢ (fderiv ℝ g (x.val 0) ∘SL fderiv ℝ (fun y => y.val 0) x) (Space.basis j.succ) = 0d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_eq_zero:∀ (g : ℝ → ℝ), Differentiable ℝ g → Space.deriv j.succ (fun y => g (y.val 0)) x = 0⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0
        fderiv_comp _ hg.differentiableAt (byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succg:ℝ → ℝhg:Differentiable ℝ g⊢ DifferentiableAt ℝ (fun y => y.val 0) xd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succg:ℝ → ℝhg:Differentiable ℝ g⊢ (fderiv ℝ g (x.val 0) ∘SL fderiv ℝ (fun y => y.val 0) x) (Space.basis j.succ) = 0d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_eq_zero:∀ (g : ℝ → ℝ), Differentiable ℝ g → Space.deriv j.succ (fun y => g (y.val 0)) x = 0⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0 fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succg:ℝ → ℝhg:Differentiable ℝ g⊢ (fderiv ℝ g (x.val 0) ∘SL fderiv ℝ (fun y => y.val 0) x) (Space.basis j.succ) = 0d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_eq_zero:∀ (g : ℝ → ℝ), Differentiable ℝ g → Space.deriv j.succ (fun y => g (y.val 0)) x = 0⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0)]d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succg:ℝ → ℝhg:Differentiable ℝ g⊢ (fderiv ℝ g (x.val 0) ∘SL fderiv ℝ (fun y => y.val 0) x) (Space.basis j.succ) = 0d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_eq_zero:∀ (g : ℝ → ℝ), Differentiable ℝ g → Space.deriv j.succ (fun y => g (y.val 0)) x = 0⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0
      simp [← Space.deriv_eq, Space.deriv_component, Fin.succ_ne_zero]d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_eq_zero:∀ (g : ℝ → ℝ), Differentiable ℝ g → Space.deriv j.succ (fun y => g (y.val 0)) x = 0⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_eq_zero:∀ (g : ℝ → ℝ), Differentiable ℝ g → Space.deriv j.succ (fun y => g (y.val 0)) x = 0⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0
    simp only [harmonicWaveX_vectorPotential_succ', mul_one]d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_eq_zero:∀ (g : ℝ → ℝ), Differentiable ℝ g → Space.deriv j.succ (fun y => g (y.val 0)) x = 0⊢ Space.deriv j.succ (fun x => -E₀ ⟨i, ⋯⟩ / (𝓕.c.val * k) * sin (k * (t.val * 𝓕.c.val - x.val 0) + φ ⟨i, ⋯⟩)) x = 0
    exact transverse_deriv_eq_zero
      (fun u => -E₀ ⟨i, byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_eq_zero:∀ (g : ℝ → ℝ), Differentiable ℝ g → Space.deriv j.succ (fun y => g (y.val 0)) x = 0u:ℝ⊢ i < d grindAll goals completed! 🐙⟩ / (𝓕.c.val * k) *
        sin (k * (t.val * 𝓕.c.val - u) + φ ⟨i, byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_eq_zero:∀ (g : ℝ → ℝ), Differentiable ℝ g → Space.deriv j.succ (fun y => g (y.val 0)) x = 0u:ℝ⊢ i < d grindAll goals completed! 🐙⟩)) (byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succj:Fin di✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_eq_zero:∀ (g : ℝ → ℝ), Differentiable ℝ g → Space.deriv j.succ (fun y => g (y.val 0)) x = 0⊢ Differentiable ℝ fun u => -E₀ ⟨i, ⋯⟩ / (𝓕.c.val * k) * sin (k * (t.val * 𝓕.c.val - u) + φ ⟨i, ⋯⟩) fun_propAll goals completed! 🐙)


@[simp]
lemma harmonicWaveX_vectorPotential_succ_space_deriv_zero {d} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : Fin d) :
    Space.deriv 0 (fun x => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x i.succ) x
    = E₀ i / 𝓕.c.val * Real.cos (𝓕.c.val * k * t.val - k * x 0 + φ i) := byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Space.deriv 0 (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) x =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  simp [harmonicWaveX_vectorPotential_succ]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Space.deriv 0 (fun x => -E₀ i / (𝓕.c.val * k) * sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) x =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  rw [Space.deriv_eq_fderiv_basis,d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ (fderiv ℝ (fun x => -E₀ i / (𝓕.c.val * k) * sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) x) (Space.basis 0) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ ((-E₀ i / (𝓕.c.val * k)) • fderiv ℝ (fun x => sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) x) (Space.basis 0) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i) fderiv_const_mul (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ DifferentiableAt ℝ (fun x => sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) xd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ ((-E₀ i / (𝓕.c.val * k)) • fderiv ℝ (fun x => sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) x) (Space.basis 0) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i) fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ ((-E₀ i / (𝓕.c.val * k)) • fderiv ℝ (fun x => sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) x) (Space.basis 0) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i))]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ ((-E₀ i / (𝓕.c.val * k)) • fderiv ℝ (fun x => sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) x) (Space.basis 0) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  simp only [FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / (𝓕.c.val * k) * (fderiv ℝ (fun x => sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) x) (Space.basis 0) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  rw [fderiv_sin (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ DifferentiableAt ℝ (fun x => k * (t.val * 𝓕.c.val - x.val 0) + φ i) xd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / (𝓕.c.val * k) *
    (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) • fderiv ℝ (fun x => k * (t.val * 𝓕.c.val - x.val 0) + φ i) x)
      (Space.basis 0) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i) fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / (𝓕.c.val * k) *
    (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) • fderiv ℝ (fun x => k * (t.val * 𝓕.c.val - x.val 0) + φ i) x)
      (Space.basis 0) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i))]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / (𝓕.c.val * k) *
    (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) • fderiv ℝ (fun x => k * (t.val * 𝓕.c.val - x.val 0) + φ i) x)
      (Space.basis 0) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  simp only [fderiv_add_const, FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / (𝓕.c.val * k) *
    (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) *
      (fderiv ℝ (fun y => k * (t.val * 𝓕.c.val - y.val 0)) x) (Space.basis 0)) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  rw [fderiv_const_mul (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ DifferentiableAt ℝ (fun y => t.val * 𝓕.c.val - y.val 0) xd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / (𝓕.c.val * k) *
    (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k • -fderiv ℝ (fun y => y.val 0) x) (Space.basis 0)) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i) fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / (𝓕.c.val * k) *
    (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k • -fderiv ℝ (fun y => y.val 0) x) (Space.basis 0)) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)), fderiv_const_subd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / (𝓕.c.val * k) *
    (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k • -fderiv ℝ (fun y => y.val 0) x) (Space.basis 0)) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / (𝓕.c.val * k) *
    (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k • -fderiv ℝ (fun y => y.val 0) x) (Space.basis 0)) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / (𝓕.c.val * k) *
    (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k • -fderiv ℝ (fun y => y.val 0) x) (Space.basis 0)) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  simp only [smul_neg, _root_.neg_apply, FunLike.coe_smul, Pi.smul_apply,
    smul_eq_mul, mul_neg]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) *
      (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k * (fderiv ℝ (fun y => y.val 0) x) (Space.basis 0)))) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  rw [← Space.deriv_eq_fderiv_basis,d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) * (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k * Space.deriv 0 (fun y => y.val 0) x))) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) * (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k * if 0 = 0 then 1 else 0))) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i) Space.deriv_componentd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) * (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k * if 0 = 0 then 1 else 0))) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) * (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k * if 0 = 0 then 1 else 0))) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) * (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k * if 0 = 0 then 1 else 0))) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  simp only [↓reduceIte, mul_one]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) * (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * k)) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  field_simpAll goals completed! 🐙

D. The electric field

D.1. Components of the electric field


lemma harmonicWaveX_electricField_zero {d} (𝓕 : FreeSpace) (k : ℝ)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ) :
    (harmonicWaveX 𝓕 k E₀ φ).electricField 𝓕.c t x 0 = 0 := byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0 = 0
  simp [ElectromagneticPotential.electricField]d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ (∂ₜ (fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp 0 = 0
  rw [← Time.deriv_euclidd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ ∂ₜ (fun t => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0) t = 0hfd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t xd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ ∂ₜ (fun t => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0) t = 0hfd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x]d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ ∂ₜ (fun t => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0) t = 0hfd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
  simp only [harmonicWaveX_vectorPotential_zero_eq_zero, Time.deriv_const]hfd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
  exact vectorPotential_differentiable_time _ (harmonicWaveX_differentiable 𝓕 k E₀ φ) xAll goals completed! 🐙



lemma harmonicWaveX_electricField_succ {d} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : Fin d) :
    (harmonicWaveX 𝓕 k E₀ φ).electricField 𝓕.c t x i.succ =
    E₀ i * Real.cos (k * 𝓕.c * t.val - k * x 0 + φ i) := byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ = E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)
  simp [ElectromagneticPotential.electricField]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(∂ₜ (fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i.succ =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)
  rw [← Time.deriv_euclidd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -∂ₜ (fun t => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) t =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t xd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -∂ₜ (fun t => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) t =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -∂ₜ (fun t => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) t =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
  simp [harmonicWaveX_vectorPotential_succ]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -∂ₜ (fun t => -E₀ i / (𝓕.c.val * k) * sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) t =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
  rw [Time.deriv_eq,d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(fderiv ℝ (fun t => -E₀ i / (𝓕.c.val * k) * sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) t) 1 =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t xd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -((-E₀ i / (𝓕.c.val * k)) • fderiv ℝ (fun t => sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) t) 1 =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x fderiv_const_mul (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ DifferentiableAt ℝ (fun t => sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) td:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -((-E₀ i / (𝓕.c.val * k)) • fderiv ℝ (fun t => sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) t) 1 =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -((-E₀ i / (𝓕.c.val * k)) • fderiv ℝ (fun t => sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) t) 1 =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -((-E₀ i / (𝓕.c.val * k)) • fderiv ℝ (fun t => sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) t) 1 =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
  simp only [FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) * (fderiv ℝ (fun t => sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)) t) 1) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
  rw [fderiv_sin (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ DifferentiableAt ℝ (fun t => k * (t.val * 𝓕.c.val - x.val 0) + φ i) td:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) *
      (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) • k • fderiv ℝ (fun t => t.val * 𝓕.c.val - x.val 0) t) 1) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) *
      (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) • k • fderiv ℝ (fun t => t.val * 𝓕.c.val - x.val 0) t) 1) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x), fderiv_add_const,d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) *
      (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) • fderiv ℝ (fun t => k * (t.val * 𝓕.c.val - x.val 0)) t) 1) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t xd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) *
      (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) • k • fderiv ℝ (fun t => t.val * 𝓕.c.val - x.val 0) t) 1) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x fderiv_const_mul (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ DifferentiableAt ℝ (fun t => t.val * 𝓕.c.val - x.val 0) td:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) *
      (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) • k • fderiv ℝ (fun t => t.val * 𝓕.c.val - x.val 0) t) 1) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) *
      (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) • k • fderiv ℝ (fun t => t.val * 𝓕.c.val - x.val 0) t) 1) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) *
      (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) • k • fderiv ℝ (fun t => t.val * 𝓕.c.val - x.val 0) t) 1) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
  simp only [FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) *
      (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k * (fderiv ℝ (fun t => t.val * 𝓕.c.val - x.val 0) t) 1))) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
  rw [fderiv_sub_const,d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) *
      (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k * (fderiv ℝ (fun t => t.val * 𝓕.c.val) t) 1))) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t xd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) * (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k * (𝓕.c.val • fderiv ℝ Time.val t) 1))) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x fderiv_mul_const (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ DifferentiableAt ℝ Time.val td:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) * (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k * (𝓕.c.val • fderiv ℝ Time.val t) 1))) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) * (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k * (𝓕.c.val • fderiv ℝ Time.val t) 1))) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) * (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k * (𝓕.c.val • fderiv ℝ Time.val t) 1))) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
  simp only [FunLike.coe_smul, Pi.smul_apply, Time.fderiv_val, smul_eq_mul, mul_one]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / (𝓕.c.val * k) * (cos (k * (t.val * 𝓕.c.val - x.val 0) + φ i) * (k * 𝓕.c.val))) =
  E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
  field_simphfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
  exact vectorPotential_differentiable_time _ (harmonicWaveX_differentiable 𝓕 k E₀ φ) xAll goals completed! 🐙

D.2. Spatial derivatives of the electric field



lemma harmonicWaveX_electricField_space_deriv_same {d} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : Fin d.succ) :
    Space.deriv i (fun x => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x i) x
    = 0 := byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succ⊢ Space.deriv i (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i) x = 0
  match i with
  | 0 =>d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succ⊢ Space.deriv 0 (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0) x = 0 simp [harmonicWaveX_electricField_zero]All goals completed! 🐙
  | ⟨Nat.succ i, hi⟩ =>d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succ⊢ Space.deriv ⟨i.succ, hi⟩ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0
    have transverse_deriv_cos_eq_zero : ∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ),
        Space.deriv l.succ (fun x => C * Real.cos (a - k * x 0 + b)) y = 0 := byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succ⊢ Space.deriv i (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i) x = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv ⟨i.succ, hi⟩ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0
      intro C a k b l yd:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv ⟨i.succ, hi⟩ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0
      rw [Space.deriv_eq,d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun x => C * cos (a - k * x.val 0 + b)) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun u => C * cos (a - k * u + b)) (y.val 0) ∘SL fderiv ℝ (fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv ⟨i.succ, hi⟩ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0 show (fun x : Space d.succ => C * Real.cos (a - k * x 0 + b))
          = (fun u => C * Real.cos (a - k * u + b)) ∘ (fun x => x 0) from rfl,d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ ((fun u => C * cos (a - k * u + b)) ∘ fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun u => C * cos (a - k * u + b)) (y.val 0) ∘SL fderiv ℝ (fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv ⟨i.succ, hi⟩ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0
        fderiv_comp _ (byd:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ DifferentiableAt ℝ (fun u => C * cos (a - k * u + b)) (y.val 0)d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun u => C * cos (a - k * u + b)) (y.val 0) ∘SL fderiv ℝ (fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv ⟨i.succ, hi⟩ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0 fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun u => C * cos (a - k * u + b)) (y.val 0) ∘SL fderiv ℝ (fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv ⟨i.succ, hi⟩ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0) (byd:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ DifferentiableAt ℝ (fun x => x.val 0) yd:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun u => C * cos (a - k * u + b)) (y.val 0) ∘SL fderiv ℝ (fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv ⟨i.succ, hi⟩ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0 fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun u => C * cos (a - k * u + b)) (y.val 0) ∘SL fderiv ℝ (fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv ⟨i.succ, hi⟩ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0)]d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun u => C * cos (a - k * u + b)) (y.val 0) ∘SL fderiv ℝ (fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv ⟨i.succ, hi⟩ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0
      simp [← Space.deriv_eq, Space.deriv_component, Fin.succ_ne_zero]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv ⟨i.succ, hi⟩ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv ⟨i.succ, hi⟩ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩) x = 0
    rw [← Fin.succ_mk _ _ (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ i < dd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv ⟨i, ⋯⟩.succ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i, ⋯⟩.succ) x = 0 grindAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv ⟨i, ⋯⟩.succ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i, ⋯⟩.succ) x = 0)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv ⟨i, ⋯⟩.succ (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i, ⋯⟩.succ) x = 0
    conv_lhs =>
      enter [2, x]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex✝:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0x:Space d.succ| (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i, ⋯⟩.succ
      rw [harmonicWaveX_electricField_succ _ _ hk]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex✝:Space d.succi✝:Fin d.succi:ℕhi:i.succ < d.succtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0x:Space d.succ| E₀ ⟨i, ⋯⟩ * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ ⟨i, ⋯⟩)
    apply transverse_deriv_cos_eq_zeroAll goals completed! 🐙

D.3. Time derivatives of the electric field



lemma harmonicWaveX_electricField_succ_time_deriv {d} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : Fin d) :
    Time.deriv (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x i.succ) t
    = - k * 𝓕.c * E₀ i * Real.sin (k * 𝓕.c * t.val - k * x 0 + φ i) := byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ ∂ₜ (fun t => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) t =
  -k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)
  conv_lhs =>
    enter [1, t]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt✝:Timex:Space d.succi:Fin dt:Time| (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ
    rw [harmonicWaveX_electricField_succ _ _ hk]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt✝:Timex:Space d.succi:Fin dt:Time| E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)
  rw [Time.deriv_eq,d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ (fderiv ℝ (fun t => E₀ i * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)) t) 1 =
  -k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ (E₀ i • fderiv ℝ (fun t => cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)) t) 1 =
  -k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i) fderiv_const_mul (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ DifferentiableAt ℝ (fun t => cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)) td:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ (E₀ i • fderiv ℝ (fun t => cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)) t) 1 =
  -k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i) fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ (E₀ i • fderiv ℝ (fun t => cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)) t) 1 =
  -k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i))]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ (E₀ i • fderiv ℝ (fun t => cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)) t) 1 =
  -k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)
  simp only [Nat.succ_eq_add_one, FunLike.coe_smul, Pi.smul_apply, smul_eq_mul,
    neg_mul]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ E₀ i * (fderiv ℝ (fun t => cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)) t) 1 =
  -(k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i))
  rw [fderiv_cos (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ DifferentiableAt ℝ (fun t => k * 𝓕.c.val * t.val - k * x.val 0 + φ i) td:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ E₀ i *
    (-sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i) • fderiv ℝ (fun t => k * 𝓕.c.val * t.val - k * x.val 0 + φ i) t) 1 =
  -(k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)) fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ E₀ i *
    (-sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i) • fderiv ℝ (fun t => k * 𝓕.c.val * t.val - k * x.val 0 + φ i) t) 1 =
  -(k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)))]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ E₀ i *
    (-sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i) • fderiv ℝ (fun t => k * 𝓕.c.val * t.val - k * x.val 0 + φ i) t) 1 =
  -(k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i))
  simp only [fderiv_add_const, neg_smul, _root_.neg_apply,
    FunLike.coe_smul, Pi.smul_apply, smul_eq_mul, mul_neg, neg_inj]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ E₀ i * (sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i) * (fderiv ℝ (fun y => k * 𝓕.c.val * y.val - k * x.val 0) t) 1) =
  k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)
  rw [fderiv_sub_const,d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ E₀ i * (sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i) * (fderiv ℝ (fun y => k * 𝓕.c.val * y.val) t) 1) =
  k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ E₀ i * (sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i) * ((k * 𝓕.c.val) • fderiv ℝ Time.val t) 1) =
  k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i) fderiv_const_mul (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ DifferentiableAt ℝ Time.val td:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ E₀ i * (sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i) * ((k * 𝓕.c.val) • fderiv ℝ Time.val t) 1) =
  k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i) fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ E₀ i * (sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i) * ((k * 𝓕.c.val) • fderiv ℝ Time.val t) 1) =
  k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i))]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ E₀ i * (sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i) * ((k * 𝓕.c.val) • fderiv ℝ Time.val t) 1) =
  k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)
  simp only [FunLike.coe_smul, Pi.smul_apply, Time.fderiv_val, smul_eq_mul, mul_one]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ E₀ i * (sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i) * (k * 𝓕.c.val)) =
  k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)
  ringAll goals completed! 🐙

D.4. Divergence of the electric field

@[simp]
lemma harmonicWaveX_div_electricField_eq_zero {d} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ) :
    Space.div (fun x => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) x = 0 := byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ div (fun x => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) x = 0
  simp [Space.div]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ ∑ x_1, Space.deriv x_1 (fun x => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp x_1) x = 0
  exact Finset.sum_eq_zero fun i _ =>
    harmonicWaveX_electricField_space_deriv_same 𝓕 k hk E₀ φ t x iAll goals completed! 🐙

E. The magnetic field matrix for a harmonic wave

E.1. Components of the magnetic field matrix

              

@[simp]
lemma harmonicWaveX_magneticFieldMatrix_succ_succ {d} (𝓕 : FreeSpace) (k : ℝ)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ)
    (i j : Fin d) :
    (harmonicWaveX 𝓕 k E₀ φ).magneticFieldMatrix 𝓕.c t x (i.succ, j.succ) = 0 := byd:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin dj:Fin d⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i.succ, j.succ) = 0
  rw [magneticFieldMatrix_eq_vectorPotential _ (harmonicWaveX_differentiable 𝓕 k E₀ φ)d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin dj:Fin d⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) x -
    Space.deriv i.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp j.succ) x =
  0d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin dj:Fin d⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) x -
    Space.deriv i.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp j.succ) x =
  0]d:ℕ𝓕:FreeSpacek:ℝE₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin dj:Fin d⊢ Space.deriv j.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) x -
    Space.deriv i.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp j.succ) x =
  0
  simp only [Nat.succ_eq_add_one, harmonicWaveX_vectorPotential_space_deriv_succ, sub_self]All goals completed! 🐙

lemma harmonicWaveX_magneticFieldMatrix_zero_succ {d} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ)
    (i : Fin d) :
    (harmonicWaveX 𝓕 k E₀ φ).magneticFieldMatrix 𝓕.c t x (0, i.succ) =
    (- E₀ i / 𝓕.c.val) * cos (𝓕.c.val * k * t.val - k * x 0 + φ i) := byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, i.succ) =
  -E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  rw [magneticFieldMatrix_eq_vectorPotential _ (harmonicWaveX_differentiable 𝓕 k E₀ φ)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Space.deriv i.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0) x -
    Space.deriv 0 (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) x =
  -E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Space.deriv i.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0) x -
    Space.deriv 0 (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) x =
  -E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Space.deriv i.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0) x -
    Space.deriv 0 (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) x =
  -E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  simp only [Nat.succ_eq_add_one, harmonicWaveX_vectorPotential_zero_eq_zero, Space.deriv_const,
    zero_sub]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -Space.deriv 0 (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) x =
  -E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  rw [harmonicWaveX_vectorPotential_succ_space_deriv_zerod:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)) =
  -E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)hkd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ k ≠ 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)) =
  -E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)hkd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ k ≠ 0]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)) =
  -E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)hkd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ k ≠ 0
  simp only [Nat.succ_eq_add_one]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)) =
  -E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)hkd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ k ≠ 0
  ringhkd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ k ≠ 0
  exact hkAll goals completed! 🐙

lemma harmonicWaveX_magneticFieldMatrix_succ_zero {d} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ)
    (i : Fin d) :
    (harmonicWaveX 𝓕 k E₀ φ).magneticFieldMatrix 𝓕.c t x (i.succ, 0) =
    (E₀ i / 𝓕.c.val) * cos (𝓕.c.val * k * t.val - k * x 0 + φ i) := byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i.succ, 0) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  rw [magneticFieldMatrix_eq_vectorPotential _ (harmonicWaveX_differentiable 𝓕 k E₀ φ)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Space.deriv 0 (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) x -
    Space.deriv i.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0) x =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Space.deriv 0 (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) x -
    Space.deriv i.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0) x =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Space.deriv 0 (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) x -
    Space.deriv i.succ (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0) x =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  simp only [Nat.succ_eq_add_one, harmonicWaveX_vectorPotential_zero_eq_zero, Space.deriv_const,
    sub_zero]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Space.deriv 0 (fun x => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) x =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  rw [harmonicWaveX_vectorPotential_succ_space_deriv_zerod:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i) =
  E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)hkd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ k ≠ 0hkd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ k ≠ 0]hkd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ k ≠ 0
  exact hkAll goals completed! 🐙

E.2. Space derivatives of the magnetic field matrix



lemma harmonicWaveX_magneticFieldMatrix_space_deriv_succ {d} (𝓕 : FreeSpace) (k : ℝ)
    (hk : k ≠ 0)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ)
    (i j : Fin d.succ) (l : Fin d) :
    Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i, j)) x
    = 0 := byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl:Fin d⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i, j)) x = 0
  have transverse_deriv_cos_eq_zero : ∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ),
      Space.deriv l.succ (fun x => C * Real.cos (a - k * x 0 + b)) y = 0 := by
    intro C a k b l yd:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl✝:Fin dC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i, j)) x = 0
    rw [Space.deriv_eq,d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl✝:Fin dC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun x => C * cos (a - k * x.val 0 + b)) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl✝:Fin dC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun u => C * cos (a - k * u + b)) (y.val 0) ∘SL fderiv ℝ (fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i, j)) x = 0 show (fun x : Space d.succ => C * Real.cos (a - k * x 0 + b))
        = (fun u => C * Real.cos (a - k * u + b)) ∘ (fun x => x 0) from rfl,d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl✝:Fin dC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ ((fun u => C * cos (a - k * u + b)) ∘ fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl✝:Fin dC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun u => C * cos (a - k * u + b)) (y.val 0) ∘SL fderiv ℝ (fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i, j)) x = 0
      fderiv_comp _ (byd:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl✝:Fin dC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ DifferentiableAt ℝ (fun u => C * cos (a - k * u + b)) (y.val 0)d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl✝:Fin dC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun u => C * cos (a - k * u + b)) (y.val 0) ∘SL fderiv ℝ (fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i, j)) x = 0 fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl✝:Fin dC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun u => C * cos (a - k * u + b)) (y.val 0) ∘SL fderiv ℝ (fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i, j)) x = 0) (byd:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl✝:Fin dC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ DifferentiableAt ℝ (fun x => x.val 0) yd:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl✝:Fin dC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun u => C * cos (a - k * u + b)) (y.val 0) ∘SL fderiv ℝ (fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i, j)) x = 0 fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl✝:Fin dC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun u => C * cos (a - k * u + b)) (y.val 0) ∘SL fderiv ℝ (fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i, j)) x = 0)]d:ℕ𝓕:FreeSpacek✝:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl✝:Fin dC:ℝa:ℝk:ℝb:ℝl:Fin dy:Space d.succ⊢ (fderiv ℝ (fun u => C * cos (a - k * u + b)) (y.val 0) ∘SL fderiv ℝ (fun x => x.val 0) y) (Space.basis l.succ) = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i, j)) x = 0
    simp [← Space.deriv_eq, Space.deriv_component, Fin.succ_ne_zero]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i, j)) x = 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i, j)) x = 0
  match i, j with
  | 0, 0 =>d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, 0)) x = 0 simpAll goals completed! 🐙
  | ⟨Nat.succ i, hi⟩, ⟨Nat.succ j, hj⟩ =>d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succj✝:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0i:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succ⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i.succ, hi⟩, ⟨j.succ, hj⟩)) x = 0
    conv_lhs =>
      enter [2, x]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex✝:Space d.succi✝:Fin d.succj✝:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0i:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succx:Space (d + 1)| magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i.succ, hi⟩, ⟨j.succ, hj⟩)
      rw [← Fin.succ_mk _ _ (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex✝:Space d.succi✝:Fin d.succj✝:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0i:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succx:Space (d + 1)⊢ i < d grindAll goals completed! 🐙)]
      rw [← Fin.succ_mk _ _ (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex✝:Space d.succi✝:Fin d.succj✝:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0i:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succx:Space (d + 1)⊢ j < d grindAll goals completed! 🐙)]
      rw [harmonicWaveX_magneticFieldMatrix_succ_succ _ _]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex✝:Space d.succi✝:Fin d.succj✝:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0i:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succx:Space (d + 1)| 0
    simpAll goals completed! 🐙
  | 0, ⟨Nat.succ j, hj⟩ =>d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj✝:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0j:ℕhj:j.succ < d.succ⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, ⟨j.succ, hj⟩)) x = 0
    conv_lhs =>
      enter [2, x]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex✝:Space d.succi:Fin d.succj✝:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0j:ℕhj:j.succ < d.succx:Space (d + 1)| magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, ⟨j.succ, hj⟩)
      rw [← Fin.succ_mk _ _ (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex✝:Space d.succi:Fin d.succj✝:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0j:ℕhj:j.succ < d.succx:Space (d + 1)⊢ j < d grindAll goals completed! 🐙)]
      rw [harmonicWaveX_magneticFieldMatrix_zero_succ _ k hk]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex✝:Space d.succi:Fin d.succj✝:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0j:ℕhj:j.succ < d.succx:Space (d + 1)| -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ ⟨j, ⋯⟩)
    apply transverse_deriv_cos_eq_zeroAll goals completed! 🐙
  | ⟨Nat.succ j, hj⟩, 0 =>d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succj✝:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0j:ℕhj:j.succ < d.succ⊢ Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨j.succ, hj⟩, 0)) x = 0
    conv_lhs =>
      enter [2, x]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex✝:Space d.succi:Fin d.succj✝:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0j:ℕhj:j.succ < d.succx:Space (d + 1)| magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨j.succ, hj⟩, 0)
      rw [← Fin.succ_mk _ _ (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex✝:Space d.succi:Fin d.succj✝:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0j:ℕhj:j.succ < d.succx:Space (d + 1)⊢ j < d grindAll goals completed! 🐙)]
      rw [harmonicWaveX_magneticFieldMatrix_succ_zero _ k hk]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex✝:Space d.succi:Fin d.succj✝:Fin d.succl:Fin dtransverse_deriv_cos_eq_zero:∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ), Space.deriv l.succ (fun x => C * cos (a - k * x.val 0 + b)) y = 0j:ℕhj:j.succ < d.succx:Space (d + 1)| E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ ⟨j, ⋯⟩)
    apply transverse_deriv_cos_eq_zeroAll goals completed! 🐙



lemma harmonicWaveX_magneticFieldMatrix_zero_succ_space_deriv_zero {d} (𝓕 : FreeSpace) (k : ℝ)
    (hk : k ≠ 0)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ)
    (i : Fin d) :
    Space.deriv 0 (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, i.succ)) x
    = -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x 0 + φ i) := byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Space.deriv 0 (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, i.succ)) x =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  conv_lhs =>
    enter [2, x]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex✝:Space d.succi:Fin dx:Space d.succ| magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, i.succ)
    rw [harmonicWaveX_magneticFieldMatrix_zero_succ _ k hk]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex✝:Space d.succi:Fin dx:Space d.succ| -E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  rw [Space.deriv_eq,d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ (fderiv ℝ (fun x => -E₀ i / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)) x) (Space.basis 0) =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ ((-E₀ i / 𝓕.c.val) • fderiv ℝ (fun x => cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)) x) (Space.basis 0) =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) fderiv_const_mul (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ DifferentiableAt ℝ (fun x => cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)) xd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ ((-E₀ i / 𝓕.c.val) • fderiv ℝ (fun x => cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)) x) (Space.basis 0) =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ ((-E₀ i / 𝓕.c.val) • fderiv ℝ (fun x => cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)) x) (Space.basis 0) =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i))]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ ((-E₀ i / 𝓕.c.val) • fderiv ℝ (fun x => cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)) x) (Space.basis 0) =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  simp only [Nat.succ_eq_add_one, FunLike.coe_smul, Pi.smul_apply, smul_eq_mul,
    neg_mul]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val * (fderiv ℝ (fun x => cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)) x) (Space.basis 0) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  rw [fderiv_cos (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ DifferentiableAt ℝ (fun x => 𝓕.c.val * k * t.val - k * x.val 0 + φ i) xd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val *
    (-sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) • fderiv ℝ (fun x => 𝓕.c.val * k * t.val - k * x.val 0 + φ i) x)
      (Space.basis 0) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val *
    (-sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) • fderiv ℝ (fun x => 𝓕.c.val * k * t.val - k * x.val 0 + φ i) x)
      (Space.basis 0) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i))]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val *
    (-sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) • fderiv ℝ (fun x => 𝓕.c.val * k * t.val - k * x.val 0 + φ i) x)
      (Space.basis 0) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  simp only [fderiv_add_const, neg_smul, _root_.neg_apply,
    FunLike.coe_smul, Pi.smul_apply, smul_eq_mul, mul_neg]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / 𝓕.c.val *
      (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) *
        (fderiv ℝ (fun y => 𝓕.c.val * k * t.val - k * y.val 0) x) (Space.basis 0))) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  rw [fderiv_const_subd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / 𝓕.c.val *
      (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) * (-fderiv ℝ (fun y => k * y.val 0) x) (Space.basis 0))) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / 𝓕.c.val *
      (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) * (-fderiv ℝ (fun y => k * y.val 0) x) (Space.basis 0))) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(-E₀ i / 𝓕.c.val *
      (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) * (-fderiv ℝ (fun y => k * y.val 0) x) (Space.basis 0))) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  simp only [_root_.neg_apply, mul_neg, neg_neg]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val *
    (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) * (fderiv ℝ (fun y => k * y.val 0) x) (Space.basis 0)) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  rw [fderiv_const_mul (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ DifferentiableAt ℝ (fun y => y.val 0) xd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val *
    (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) * (k • fderiv ℝ (fun y => y.val 0) x) (Space.basis 0)) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val *
    (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) * (k • fderiv ℝ (fun y => y.val 0) x) (Space.basis 0)) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i))]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val *
    (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) * (k • fderiv ℝ (fun y => y.val 0) x) (Space.basis 0)) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  simp only [FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val *
    (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) * (k * (fderiv ℝ (fun y => y.val 0) x) (Space.basis 0))) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  rw [← Space.deriv_eq,d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val * (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) * (k * Space.deriv 0 (fun y => y.val 0) x)) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val * (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) * (k * if 0 = 0 then 1 else 0)) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) Space.deriv_componentd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val * (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) * (k * if 0 = 0 then 1 else 0)) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val * (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) * (k * if 0 = 0 then 1 else 0)) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val * (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) * (k * if 0 = 0 then 1 else 0)) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  simp only [↓reduceIte, mul_one]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -E₀ i / 𝓕.c.val * (sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i) * k) =
  -(E₀ i * k) / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
  ringAll goals completed! 🐙

F. Maxwell's equations for a harmonic wave



lemma harmonicWaveX_isExtrema {d} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) :
    IsExtrema 𝓕 (harmonicWaveX 𝓕 k E₀ φ) 0 := byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ IsExtrema 𝓕 (harmonicWaveX 𝓕 k E₀ φ) 0
  rw [isExtrema_iff_gauss_ampere_magneticFieldMatrixd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ∀ (t : Time) (x : Space d.succ),
  div (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t) x = LorentzCurrentDensity.chargeDensity 𝓕.c 0 t x / 𝓕.ε₀ ∧
    ∀ (i : Fin d.succ),
      𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i =
        ∑ j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (j, i)) x -
          𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp ihAd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ContDiff ℝ (↑⊤) (harmonicWaveX 𝓕 k E₀ φ).valhJd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ContDiff ℝ (↑⊤) 0d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ∀ (t : Time) (x : Space d.succ),
  div (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t) x = LorentzCurrentDensity.chargeDensity 𝓕.c 0 t x / 𝓕.ε₀ ∧
    ∀ (i : Fin d.succ),
      𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i =
        ∑ j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (j, i)) x -
          𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp ihAd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ContDiff ℝ (↑⊤) (harmonicWaveX 𝓕 k E₀ φ).valhJd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ContDiff ℝ (↑⊤) 0]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ∀ (t : Time) (x : Space d.succ),
  div (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t) x = LorentzCurrentDensity.chargeDensity 𝓕.c 0 t x / 𝓕.ε₀ ∧
    ∀ (i : Fin d.succ),
      𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i =
        ∑ j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (j, i)) x -
          𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp ihAd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ContDiff ℝ (↑⊤) (harmonicWaveX 𝓕 k E₀ φ).valhJd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ContDiff ℝ (↑⊤) 0
  intro t xd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ div (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t) x = LorentzCurrentDensity.chargeDensity 𝓕.c 0 t x / 𝓕.ε₀ ∧
  ∀ (i : Fin d.succ),
    𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i =
      ∑ j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (j, i)) x -
        𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp ihAd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ContDiff ℝ (↑⊤) (harmonicWaveX 𝓕 k E₀ φ).valhJd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ContDiff ℝ (↑⊤) 0
  apply And.introleftd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ div (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t) x = LorentzCurrentDensity.chargeDensity 𝓕.c 0 t x / 𝓕.ε₀rightd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ ∀ (i : Fin d.succ),
  𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i =
    ∑ j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (j, i)) x -
      𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp ihAd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ContDiff ℝ (↑⊤) (harmonicWaveX 𝓕 k E₀ φ).valhJd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ContDiff ℝ (↑⊤) 0
  /- Gauss's law -/
  ·leftd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ div (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t) x = LorentzCurrentDensity.chargeDensity 𝓕.c 0 t x / 𝓕.ε₀ simpleftd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ div (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t) x = 0
    rw [harmonicWaveX_div_electricField_eq_zero 𝓕 k hk E₀ φ t xleftd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙
  /- Ampère's law -/
  ·rightd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ ∀ (i : Fin d.succ),
  𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i =
    ∑ j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (j, i)) x -
      𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp i intro irightd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succ⊢ 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i =
  ∑ j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (j, i)) x -
    𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp i
    rw [Fin.sum_univ_succrightd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succ⊢ 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i =
  Space.deriv 0 (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, i)) x +
      ∑ i_1, Space.deriv i_1.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i_1.succ, i)) x -
    𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp irightd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succ⊢ 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i =
  Space.deriv 0 (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, i)) x +
      ∑ i_1, Space.deriv i_1.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i_1.succ, i)) x -
    𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp i]rightd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succ⊢ 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i =
  Space.deriv 0 (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, i)) x +
      ∑ i_1, Space.deriv i_1.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i_1.succ, i)) x -
    𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp i
    conv_rhs =>
      enter [1, 2, 2, i]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:Fin d| Space.deriv i.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i.succ, i✝)) x
      rw [harmonicWaveX_magneticFieldMatrix_space_deriv_succ _ _ hk]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:Fin d| 0
    simprightd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succ⊢ 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i =
  Space.deriv 0 (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, i)) x
    rcases Fin.eq_zero_or_eq_succ i with rfl | ⟨i, rfl⟩right.inld:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp 0 =
  Space.deriv 0 (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, 0)) xright.inrd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i.succ =
  Space.deriv 0 (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, i.succ)) x
    ·right.inld:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp 0 =
  Space.deriv 0 (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, 0)) x simpright.inld:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp 0 = 0
      rw [← Time.deriv_euclidright.inld:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ ∂ₜ (fun t => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0) t = 0right.inl.hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ Differentiable ℝ fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t xright.inld:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ ∂ₜ (fun t => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0) t = 0right.inl.hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ Differentiable ℝ fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x]right.inld:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ ∂ₜ (fun t => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0) t = 0right.inl.hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ Differentiable ℝ fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
      conv_lhs =>
        enter [1, t]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt✝:Timex:Space d.succt:Time| (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0
        rw [harmonicWaveX_electricField_zero 𝓕 k E₀]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt✝:Timex:Space d.succt:Time| 0
      simp only [Time.deriv_const]right.inl.hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ Differentiable ℝ fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
      exact electricField_differentiable_time (harmonicWaveX_contDiff 2 𝓕 k E₀ φ) xAll goals completed! 🐙
    rw [harmonicWaveX_magneticFieldMatrix_zero_succ_space_deriv_zero _ k hkright.inrd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i.succ =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)right.inrd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i.succ =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)]right.inrd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) t).ofLp i.succ =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)
    rw [← Time.deriv_euclidright.inrd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ 𝓕.μ₀ * 𝓕.ε₀ * ∂ₜ (fun t => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) t =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)right.inr.hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t xright.inrd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ 𝓕.μ₀ * 𝓕.ε₀ * ∂ₜ (fun t => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) t =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)right.inr.hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x]right.inrd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ 𝓕.μ₀ * 𝓕.ε₀ * ∂ₜ (fun t => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) t =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)right.inr.hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
    rw [harmonicWaveX_electricField_succ_time_deriv _ _ hkright.inrd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ 𝓕.μ₀ * 𝓕.ε₀ * (-k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)) =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)right.inr.hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t xright.inrd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ 𝓕.μ₀ * 𝓕.ε₀ * (-k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)) =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)right.inr.hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x]right.inrd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ 𝓕.μ₀ * 𝓕.ε₀ * (-k * 𝓕.c.val * E₀ i * sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)) =
  -E₀ i * k / 𝓕.c.val * sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)right.inr.hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
    field_simpright.inrd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ -(𝓕.μ₀ * 𝓕.ε₀ * 𝓕.c.val ^ 2 * E₀ i * sin (k * (𝓕.c.val * t.val - x.val 0) + φ i)) =
  -(E₀ i * sin (k * (𝓕.c.val * t.val - x.val 0) + φ i))right.inr.hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
    simp [𝓕.c_sq]right.inrd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ 𝓕.μ₀ * 𝓕.ε₀ * (𝓕.μ₀⁻¹ * 𝓕.ε₀⁻¹) * E₀ i = E₀ i ∨ sin (k * (𝓕.c.val * t.val - x.val 0) + φ i) = 0right.inr.hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
    field_simpright.inrd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ True ∨ sin (k * (𝓕.c.val * t.val - x.val 0) + φ i) = 0right.inr.hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
    tautoright.inr.hfd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ fun t => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x
    exact electricField_differentiable_time (harmonicWaveX_contDiff 2 𝓕 k E₀ φ) xAll goals completed! 🐙
  ·hAd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ContDiff ℝ (↑⊤) (harmonicWaveX 𝓕 k E₀ φ).val apply harmonicWaveX_contDiffAll goals completed! 🐙
  ·hJd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ContDiff ℝ (↑⊤) 0 change ContDiff ℝ _ (fun _ => 0)hJd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ContDiff ℝ ↑⊤ fun x => 0
    fun_propAll goals completed! 🐙

G. The harmonic wave is a plane wave



lemma harmonicWaveX_isPlaneWave {d} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0)
    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) :
    IsPlaneWave 𝓕 (harmonicWaveX 𝓕 k E₀ φ) ⟨Space.basis 0, byOpticalMedium:Sort ?u.2OM:OpticalMediumd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ‖Space.basis 0‖ = 1 simpAll goals completed! 🐙⟩ := byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ IsPlaneWave 𝓕 (harmonicWaveX 𝓕 k E₀ φ) { unit := Space.basis 0, norm := ⋯ }
  apply And.introleftd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ∃ E₀_1, electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) = planeWave E₀_1 𝓕.c.val { unit := Space.basis 0, norm := ⋯ }rightd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ∃ B₀,
  ∀ (t : Time) (x : Space d.succ),
    magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x =
      B₀ (⟪x, { unit := Space.basis 0, norm := ⋯ }.unit⟫_ℝ - 𝓕.c.val * t.val)
  ·leftd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ∃ E₀_1, electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) = planeWave E₀_1 𝓕.c.val { unit := Space.basis 0, norm := ⋯ } use fun u => WithLp.toLp 2 fun i =>
      match i with
      | 0 => 0
      | ⟨Nat.succ i, h⟩ => E₀ ⟨i, byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝu:ℝi✝:Fin d.succi:ℕh:i.succ < d.succ⊢ i < d grindAll goals completed! 🐙⟩ * cos (-k * u + φ ⟨i, byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝu:ℝi✝:Fin d.succi:ℕh:i.succ < d.succ⊢ i < d grindAll goals completed! 🐙⟩)
    ext t x ihd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succ⊢ (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i =
  (planeWave
        (fun u =>
          WithLp.toLp 2 fun i =>
            match i with
            | ⟨0, ⋯⟩ => 0
            | ⟨i.succ, h⟩ => E₀ ⟨i, ⋯⟩ * cos (-k * u + φ ⟨i, ⋯⟩))
        𝓕.c.val { unit := Space.basis 0, norm := ⋯ } t x).ofLp
    i
    match i with
    | 0 =>d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succ⊢ (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0 =
  (planeWave
        (fun u =>
          WithLp.toLp 2 fun i =>
            match i with
            | ⟨0, ⋯⟩ => 0
            | ⟨i.succ, h⟩ => E₀ ⟨i, ⋯⟩ * cos (-k * u + φ ⟨i, ⋯⟩))
        𝓕.c.val { unit := Space.basis 0, norm := ⋯ } t x).ofLp
    0
      simp [harmonicWaveX_electricField_zero, planeWave]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi:Fin d.succ⊢ 0 =
  match 0 with
  | ⟨0, ⋯⟩ => 0
  | ⟨i.succ, h⟩ => E₀ ⟨i, ⋯⟩ * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨i, ⋯⟩)
      rflAll goals completed! 🐙
    | ⟨Nat.succ i, h⟩ =>d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕh:i.succ < d.succ⊢ (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, h⟩ =
  (planeWave
        (fun u =>
          WithLp.toLp 2 fun i =>
            match i with
            | ⟨0, ⋯⟩ => 0
            | ⟨i.succ, h⟩ => E₀ ⟨i, ⋯⟩ * cos (-k * u + φ ⟨i, ⋯⟩))
        𝓕.c.val { unit := Space.basis 0, norm := ⋯ } t x).ofLp
    ⟨i.succ, h⟩
      simp only [Nat.succ_eq_add_one, neg_mul]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕh:i.succ < d.succ⊢ (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i + 1, h⟩ =
  (planeWave
        (fun u =>
          WithLp.toLp 2 fun i =>
            match i with
            | ⟨0, ⋯⟩ => 0
            | ⟨i.succ, h⟩ => E₀ ⟨i, ⋯⟩ * cos (-(k * u) + φ ⟨i, ⋯⟩))
        𝓕.c.val { unit := Space.basis 0, norm := ⋯ } t x).ofLp
    ⟨i + 1, h⟩
      rw [← Fin.succ_mk _ _ (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕh:i.succ < d.succ⊢ i < dd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕh:i.succ < d.succ⊢ (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i, ⋯⟩.succ =
  (planeWave
        (fun u =>
          WithLp.toLp 2 fun i =>
            match i with
            | ⟨0, ⋯⟩ => 0
            | ⟨i.succ, h⟩ => E₀ ⟨i, ⋯⟩ * cos (-(k * u) + φ ⟨i, ⋯⟩))
        𝓕.c.val { unit := Space.basis 0, norm := ⋯ } t x).ofLp
    ⟨i, ⋯⟩.succ grindAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕh:i.succ < d.succ⊢ (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i, ⋯⟩.succ =
  (planeWave
        (fun u =>
          WithLp.toLp 2 fun i =>
            match i with
            | ⟨0, ⋯⟩ => 0
            | ⟨i.succ, h⟩ => E₀ ⟨i, ⋯⟩ * cos (-(k * u) + φ ⟨i, ⋯⟩))
        𝓕.c.val { unit := Space.basis 0, norm := ⋯ } t x).ofLp
    ⟨i, ⋯⟩.succ)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕh:i.succ < d.succ⊢ (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i, ⋯⟩.succ =
  (planeWave
        (fun u =>
          WithLp.toLp 2 fun i =>
            match i with
            | ⟨0, ⋯⟩ => 0
            | ⟨i.succ, h⟩ => E₀ ⟨i, ⋯⟩ * cos (-(k * u) + φ ⟨i, ⋯⟩))
        𝓕.c.val { unit := Space.basis 0, norm := ⋯ } t x).ofLp
    ⟨i, ⋯⟩.succ
      rw [harmonicWaveX_electricField_succ _ _ hkd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕh:i.succ < d.succ⊢ E₀ ⟨i, ⋯⟩ * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ ⟨i, ⋯⟩) =
  (planeWave
        (fun u =>
          WithLp.toLp 2 fun i =>
            match i with
            | ⟨0, ⋯⟩ => 0
            | ⟨i.succ, h⟩ => E₀ ⟨i, ⋯⟩ * cos (-(k * u) + φ ⟨i, ⋯⟩))
        𝓕.c.val { unit := Space.basis 0, norm := ⋯ } t x).ofLp
    ⟨i, ⋯⟩.succd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕh:i.succ < d.succ⊢ E₀ ⟨i, ⋯⟩ * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ ⟨i, ⋯⟩) =
  (planeWave
        (fun u =>
          WithLp.toLp 2 fun i =>
            match i with
            | ⟨0, ⋯⟩ => 0
            | ⟨i.succ, h⟩ => E₀ ⟨i, ⋯⟩ * cos (-(k * u) + φ ⟨i, ⋯⟩))
        𝓕.c.val { unit := Space.basis 0, norm := ⋯ } t x).ofLp
    ⟨i, ⋯⟩.succ]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕh:i.succ < d.succ⊢ E₀ ⟨i, ⋯⟩ * cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ ⟨i, ⋯⟩) =
  (planeWave
        (fun u =>
          WithLp.toLp 2 fun i =>
            match i with
            | ⟨0, ⋯⟩ => 0
            | ⟨i.succ, h⟩ => E₀ ⟨i, ⋯⟩ * cos (-(k * u) + φ ⟨i, ⋯⟩))
        𝓕.c.val { unit := Space.basis 0, norm := ⋯ } t x).ofLp
    ⟨i, ⋯⟩.succ
      simp [planeWave]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕh:i.succ < d.succ⊢ cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ ⟨i, ⋯⟩) = cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨i, ⋯⟩) ∨ E₀ ⟨i, ⋯⟩ = 0
      leftd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succi✝:Fin d.succi:ℕh:i.succ < d.succ⊢ cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ ⟨i, ⋯⟩) = cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨i, ⋯⟩)
      ring_nfAll goals completed! 🐙
  ·rightd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝ⊢ ∃ B₀,
  ∀ (t : Time) (x : Space d.succ),
    magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x =
      B₀ (⟪x, { unit := Space.basis 0, norm := ⋯ }.unit⟫_ℝ - 𝓕.c.val * t.val) use fun u ij =>
      match ij with
      | (0, 0) => 0
      | (0, ⟨Nat.succ j, hj⟩) =>
        (- E₀ ⟨j, byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝu:ℝij:Fin d.succ × Fin d.succj:ℕhj:j.succ < d.succ⊢ j < d grindAll goals completed! 🐙⟩ / 𝓕.c.val) * cos (-k * u + φ ⟨j, byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝu:ℝij:Fin d.succ × Fin d.succj:ℕhj:j.succ < d.succ⊢ j < d grindAll goals completed! 🐙⟩)
      | (⟨Nat.succ i, hi⟩, 0) =>
        (E₀ ⟨i, byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝu:ℝij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succ⊢ i < d grindAll goals completed! 🐙⟩ / 𝓕.c.val) * cos (-k * u + φ ⟨i, byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝu:ℝij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succ⊢ i < d grindAll goals completed! 🐙⟩)
      | (⟨Nat.succ i, hi⟩, ⟨Nat.succ j, hj⟩) => 0
    intro t xhd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x =
  (fun u ij =>
      match ij with
      | (⟨0, ⋯⟩, ⟨0, ⋯⟩) => 0
      | (⟨0, ⋯⟩, ⟨j.succ, hj⟩) => -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (-k * u + φ ⟨j, ⋯⟩)
      | (⟨i.succ, hi⟩, ⟨0, ⋯⟩) => E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (-k * u + φ ⟨i, ⋯⟩)
      | (⟨i.succ, hi⟩, ⟨j.succ, hj⟩) => 0)
    (⟪x, { unit := Space.basis 0, norm := ⋯ }.unit⟫_ℝ - 𝓕.c.val * t.val)
    ext ijhd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x ij =
  (fun u ij =>
      match ij with
      | (⟨0, ⋯⟩, ⟨0, ⋯⟩) => 0
      | (⟨0, ⋯⟩, ⟨j.succ, hj⟩) => -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (-k * u + φ ⟨j, ⋯⟩)
      | (⟨i.succ, hi⟩, ⟨0, ⋯⟩) => E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (-k * u + φ ⟨i, ⋯⟩)
      | (⟨i.succ, hi⟩, ⟨j.succ, hj⟩) => 0)
    (⟪x, { unit := Space.basis 0, norm := ⋯ }.unit⟫_ℝ - 𝓕.c.val * t.val) ij
    match ij with
    | (0, 0) =>d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, 0) =
  (fun u ij =>
      match ij with
      | (⟨0, ⋯⟩, ⟨0, ⋯⟩) => 0
      | (⟨0, ⋯⟩, ⟨j.succ, hj⟩) => -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (-k * u + φ ⟨j, ⋯⟩)
      | (⟨i.succ, hi⟩, ⟨0, ⋯⟩) => E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (-k * u + φ ⟨i, ⋯⟩)
      | (⟨i.succ, hi⟩, ⟨j.succ, hj⟩) => 0)
    (⟪x, { unit := Space.basis 0, norm := ⋯ }.unit⟫_ℝ - 𝓕.c.val * t.val) (0, 0)
      simp only [Nat.succ_eq_add_one, magneticFieldMatrix_diag_eq_zero, inner_basis, neg_mul]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succ⊢ 0 =
  match (0, 0) with
  | (⟨0, ⋯⟩, ⟨0, ⋯⟩) => 0
  | (⟨0, ⋯⟩, ⟨j.succ, hj⟩) => -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨j, ⋯⟩)
  | (⟨i.succ, hi⟩, ⟨0, ⋯⟩) => E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨i, ⋯⟩)
  | (⟨i.succ, hi⟩, ⟨j.succ, hj⟩) => 0
      rflAll goals completed! 🐙
    | (⟨0, h0⟩, ⟨Nat.succ j, hj⟩) =>d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succh0:0 < d.succj:ℕhj:j.succ < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨0, h0⟩, ⟨j.succ, hj⟩) =
  (fun u ij =>
      match ij with
      | (⟨0, ⋯⟩, ⟨0, ⋯⟩) => 0
      | (⟨0, ⋯⟩, ⟨j.succ, hj⟩) => -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (-k * u + φ ⟨j, ⋯⟩)
      | (⟨i.succ, hi⟩, ⟨0, ⋯⟩) => E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (-k * u + φ ⟨i, ⋯⟩)
      | (⟨i.succ, hi⟩, ⟨j.succ, hj⟩) => 0)
    (⟪x, { unit := Space.basis 0, norm := ⋯ }.unit⟫_ℝ - 𝓕.c.val * t.val) (⟨0, h0⟩, ⟨j.succ, hj⟩)
      simp only [Nat.succ_eq_add_one, Fin.zero_eta, inner_basis, neg_mul]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succh0:0 < d.succj:ℕhj:j.succ < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, ⟨j + 1, hj⟩) =
  -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨j, ⋯⟩)
      rw [← Fin.succ_mk _ _ (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succh0:0 < d.succj:ℕhj:j.succ < d.succ⊢ j < dd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succh0:0 < d.succj:ℕhj:j.succ < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, ⟨j, ⋯⟩.succ) =
  -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨j, ⋯⟩) grindAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succh0:0 < d.succj:ℕhj:j.succ < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, ⟨j, ⋯⟩.succ) =
  -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨j, ⋯⟩))]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succh0:0 < d.succj:ℕhj:j.succ < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, ⟨j, ⋯⟩.succ) =
  -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨j, ⋯⟩)
      rw [harmonicWaveX_magneticFieldMatrix_zero_succ _ k hkd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succh0:0 < d.succj:ℕhj:j.succ < d.succ⊢ -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ ⟨j, ⋯⟩) =
  -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨j, ⋯⟩)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succh0:0 < d.succj:ℕhj:j.succ < d.succ⊢ -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ ⟨j, ⋯⟩) =
  -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨j, ⋯⟩)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succh0:0 < d.succj:ℕhj:j.succ < d.succ⊢ -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ ⟨j, ⋯⟩) =
  -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨j, ⋯⟩)
      simp only [Nat.succ_eq_add_one, mul_eq_mul_left_iff, div_eq_zero_iff, neg_eq_zero,
        SpeedOfLight.val_ne_zero, or_false]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succh0:0 < d.succj:ℕhj:j.succ < d.succ⊢ cos (𝓕.c.val * k * t.val - k * x.val 0 + φ ⟨j, ⋯⟩) = cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨j, ⋯⟩) ∨ E₀ ⟨j, ⋯⟩ = 0
      leftd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succh0:0 < d.succj:ℕhj:j.succ < d.succ⊢ cos (𝓕.c.val * k * t.val - k * x.val 0 + φ ⟨j, ⋯⟩) = cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨j, ⋯⟩)
      ring_nfAll goals completed! 🐙
    | (⟨Nat.succ i, hi⟩, ⟨0, h0⟩) =>d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succh0:0 < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i.succ, hi⟩, ⟨0, h0⟩) =
  (fun u ij =>
      match ij with
      | (⟨0, ⋯⟩, ⟨0, ⋯⟩) => 0
      | (⟨0, ⋯⟩, ⟨j.succ, hj⟩) => -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (-k * u + φ ⟨j, ⋯⟩)
      | (⟨i.succ, hi⟩, ⟨0, ⋯⟩) => E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (-k * u + φ ⟨i, ⋯⟩)
      | (⟨i.succ, hi⟩, ⟨j.succ, hj⟩) => 0)
    (⟪x, { unit := Space.basis 0, norm := ⋯ }.unit⟫_ℝ - 𝓕.c.val * t.val) (⟨i.succ, hi⟩, ⟨0, h0⟩)
      simp only [Nat.succ_eq_add_one, Fin.zero_eta, inner_basis, neg_mul]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succh0:0 < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i + 1, hi⟩, 0) =
  E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨i, ⋯⟩)
      rw [← Fin.succ_mk _ _ (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succh0:0 < d.succ⊢ i < dd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succh0:0 < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i, ⋯⟩.succ, 0) =
  E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨i, ⋯⟩) grindAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succh0:0 < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i, ⋯⟩.succ, 0) =
  E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨i, ⋯⟩))]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succh0:0 < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i, ⋯⟩.succ, 0) =
  E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨i, ⋯⟩)
      rw [harmonicWaveX_magneticFieldMatrix_succ_zero _ k hkd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succh0:0 < d.succ⊢ E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ ⟨i, ⋯⟩) =
  E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨i, ⋯⟩)d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succh0:0 < d.succ⊢ E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ ⟨i, ⋯⟩) =
  E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨i, ⋯⟩)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succh0:0 < d.succ⊢ E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (𝓕.c.val * k * t.val - k * x.val 0 + φ ⟨i, ⋯⟩) =
  E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨i, ⋯⟩)
      simp only [Nat.succ_eq_add_one, mul_eq_mul_left_iff, div_eq_zero_iff,
        SpeedOfLight.val_ne_zero, or_false]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succh0:0 < d.succ⊢ cos (𝓕.c.val * k * t.val - k * x.val 0 + φ ⟨i, ⋯⟩) = cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨i, ⋯⟩) ∨ E₀ ⟨i, ⋯⟩ = 0
      leftd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succh0:0 < d.succ⊢ cos (𝓕.c.val * k * t.val - k * x.val 0 + φ ⟨i, ⋯⟩) = cos (-(k * (x.val 0 - 𝓕.c.val * t.val)) + φ ⟨i, ⋯⟩)
      ring_nfAll goals completed! 🐙
    | (⟨Nat.succ i, hi⟩, ⟨Nat.succ j, hj⟩) =>d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i.succ, hi⟩, ⟨j.succ, hj⟩) =
  (fun u ij =>
      match ij with
      | (⟨0, ⋯⟩, ⟨0, ⋯⟩) => 0
      | (⟨0, ⋯⟩, ⟨j.succ, hj⟩) => -E₀ ⟨j, ⋯⟩ / 𝓕.c.val * cos (-k * u + φ ⟨j, ⋯⟩)
      | (⟨i.succ, hi⟩, ⟨0, ⋯⟩) => E₀ ⟨i, ⋯⟩ / 𝓕.c.val * cos (-k * u + φ ⟨i, ⋯⟩)
      | (⟨i.succ, hi⟩, ⟨j.succ, hj⟩) => 0)
    (⟪x, { unit := Space.basis 0, norm := ⋯ }.unit⟫_ℝ - 𝓕.c.val * t.val) (⟨i.succ, hi⟩, ⟨j.succ, hj⟩)
      simp only [Nat.succ_eq_add_one]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i + 1, hi⟩, ⟨j + 1, hj⟩) = 0
      rw [← Fin.succ_mk _ _ (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succ⊢ i < dd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i, ⋯⟩.succ, ⟨j + 1, hj⟩) = 0 grindAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i, ⋯⟩.succ, ⟨j + 1, hj⟩) = 0)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i, ⋯⟩.succ, ⟨j + 1, hj⟩) = 0
      rw [← Fin.succ_mk _ _ (byd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succ⊢ j < dd:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i, ⋯⟩.succ, ⟨j, ⋯⟩.succ) = 0 grindAll goals completed! 🐙d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i, ⋯⟩.succ, ⟨j, ⋯⟩.succ) = 0)]d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succ⊢ magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (⟨i, ⋯⟩.succ, ⟨j, ⋯⟩.succ) = 0
      rw [harmonicWaveX_magneticFieldMatrix_succ_succ _ _d:ℕ𝓕:FreeSpacek:ℝhk:k ≠ 0E₀:Fin d → ℝφ:Fin d → ℝt:Timex:Space d.succij:Fin d.succ × Fin d.succi:ℕhi:i.succ < d.succj:ℕhj:j.succ < d.succ⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙

H. Polarization ellipse of the harmonic wave