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.ClassicalMechanics.WaveEquation.Basic public import Physlib.Electromagnetism.Dynamics.IsExtrema

Electromagnetic wave equation

i. Overview

In this module we define a proposition IsPlaneWave on electromagnetic potentials which is true if the potential corresponds to a plane wave. From this we derive various properties of plane waves including the orthogonality of the electric field, magnetic field and direction of propagation, in general dimensions.

ii. Key results

    IsPlaneWave : The proposition defining plane waves.

    IsPlaneWave.electricFunction : The electric function corresponding to a plane wave.

    IsPlaneWave.magneticFunction : The magnetic function corresponding to a plane wave.

    IsPlaneWave.magneticFieldMatrix_eq_propogator_cross_electricField : The magnetic field expressed in terms of the electric field and direction of propagation.

    IsPlaneWave.electricField_eq_propogator_cross_magneticFieldMatrix : The electric field expressed in terms of the magnetic field and direction of propagation.

iii. Table of contents

    A. The property of being a plane wave

      A.1. The electric and magnetic functions from a plane wave

        A.1.1. Electric function and magnetic function in terms of E and B fields

        A.1.2. Uniqueness of the electric function

        A.1.3. Uniqueness of the magnetic function

      A.2. Differentiability conditions

      A.3. Time derivative of electric and magnetic fields of a plane wave

      A.4. Space derivative of electric and magnetic fields of a plane wave

      A.5. Space derivative in terms of time derivative

    B. The magnetic field in terms of the electric field

      B.1. Time derivative of the magnetic field in terms of electric field

      B.2. Space derivative of the magnetic field in terms of electric field

      B.3. Magnetic field equal propogator cross electric field up to constant

    C. The electric field in terms of the magnetic field

      C.1. The time derivative of the electric field in terms of magnetic field

      C.2. The space derivative of the electric field in terms of magnetic field

      C.3. Electric field equal propogator cross magnetic field up to constant

iv. References

@[expose] public section

A. The property of being a plane wave

The proposition on a electromagnetic potential which is true if it corresponds to a plane wave.

def IsPlaneWave {d : ℕ} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (s : Direction d) : Prop := (∃ E₀, A.electricField 𝓕.c = planeWave E₀ 𝓕.c s) ∧ (∃ (B₀ : ℝ → Fin d × Fin d → ℝ), ∀ t x, A.magneticFieldMatrix 𝓕.c t x = B₀ (⟪x, s.unit⟫_ℝ - 𝓕.c * t))

A.1. The electric and magnetic functions from a plane wave

lemma electricField_eq_electricFunction {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Direction d} (P : IsPlaneWave 𝓕 A s) (t : Time) (x : Space d) : A.electricField 𝓕.c t x = P.electricFunction (⟪x, s.unit⟫_ℝ - 𝓕.c * t) := congrFun (congrFun (Classical.choose_spec P.1) t) xlemma magneticFieldMatrix_eq_magneticFunction {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Direction d} (P : IsPlaneWave 𝓕 A s) (t : Time) (x : Space d) : A.magneticFieldMatrix 𝓕.c t x = P.magneticFunction (⟪x, s.unit⟫_ℝ - 𝓕.c * t) := Classical.choose_spec P.2 t x
A.1.1. Electric function and magnetic function in terms of E and B fields
d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A su:ℝ⊢ P.electricFunction u = P.electricFunction (-(𝓕.c.val * { val := -u / 𝓕.c.val }.val)) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A su:ℝ⊢ u = -(𝓕.c.val * { val := -u / 𝓕.c.val }.val) All goals completed! 🐙d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A su:ℝ⊢ P.magneticFunction u = P.magneticFunction (-(𝓕.c.val * { val := -u / 𝓕.c.val }.val)) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A su:ℝ⊢ u = -(𝓕.c.val * { val := -u / 𝓕.c.val }.val) All goals completed! 🐙
A.1.2. Uniqueness of the electric function
d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A sE1:ℝ → EuclideanSpace ℝ (Fin d)hE₁:electricField 𝓕.c A = planeWave E1 𝓕.c.val st:ℝ⊢ E1 (⟪0, s.unit⟫_ℝ - 𝓕.c.val * t) = planeWave E1 𝓕.c.val s { val := t } 0 All goals completed! 🐙
A.1.3. Uniqueness of the magnetic function
All goals completed! 🐙

A.2. Differentiability conditions

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.val⊢ Differentiable ℝ fun u => electricField 𝓕.c A { val := -u / 𝓕.c.val } 0 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.val⊢ Differentiable ℝ (↿(electricField 𝓕.c A) ∘ fun u => ({ val := -u / 𝓕.c.val }, 0)) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.val⊢ Differentiable ℝ fun u => ({ val := -u / 𝓕.c.val }, 0) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.val⊢ Differentiable ℝ fun u => { val := -u / 𝓕.c.val }d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.val⊢ Differentiable ℝ fun u => 0 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.val⊢ Differentiable ℝ fun u => { val := -u / 𝓕.c.val } d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.val⊢ Differentiable ℝ (⇑toRealCLE.symm ∘ fun u => -u / 𝓕.c.val) All goals completed! 🐙 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.val⊢ Differentiable ℝ fun u => 0 All goals completed! 🐙d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valij:Fin d × Fin d⊢ Differentiable ℝ fun u => (fun u => magneticFieldMatrix 𝓕.c A { val := -u / 𝓕.c.val } 0) u ij d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valij:Fin d × Fin d⊢ Differentiable ℝ fun u => magneticFieldMatrix 𝓕.c A { val := -u / 𝓕.c.val } 0 ij d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valij:Fin d × Fin d⊢ Differentiable ℝ ((↿fun t x => magneticFieldMatrix 𝓕.c A t x ij) ∘ fun u => ({ val := -u / 𝓕.c.val }, 0)) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valij:Fin d × Fin d⊢ Differentiable ℝ fun u => ({ val := -u / 𝓕.c.val }, 0) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valij:Fin d × Fin d⊢ Differentiable ℝ fun u => { val := -u / 𝓕.c.val }d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valij:Fin d × Fin d⊢ Differentiable ℝ fun u => 0 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valij:Fin d × Fin d⊢ Differentiable ℝ fun u => { val := -u / 𝓕.c.val } d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valij:Fin d × Fin d⊢ Differentiable ℝ (⇑toRealCLE.symm ∘ fun u => -u / 𝓕.c.val) All goals completed! 🐙 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valij:Fin d × Fin d⊢ Differentiable ℝ fun u => 0 All goals completed! 🐙

A.3. Time derivative of electric and magnetic fields of a plane wave

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space dh:electricField 𝓕.c A = planeWave P.electricFunction 𝓕.c.val s⊢ (-𝓕.c.val • fun t => planeWave (fun x => (fderiv ℝ P.electricFunction x) 1) 𝓕.c.val s t x) t = -𝓕.c.val • (fderiv ℝ P.electricFunction (⟪x, s.unit⟫_ℝ - 𝓕.c.val * t.val)) 1 All goals completed! 🐙d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin d⊢ (fderiv ℝ (fun u => P.magneticFunction u (i, j)) (⟪x, s.unit⟫_ℝ - 𝓕.c.val * t.val) ∘SL (fderiv ℝ (fun t => ⟪x, s.unit⟫_ℝ) t - 𝓕.c.val • fderiv ℝ Time.val t)) 1 = -𝓕.c.val • (fderiv ℝ (fun u => P.magneticFunction u (i, j)) (⟪x, s.unit⟫_ℝ - 𝓕.c.val * t.val)) 1 All goals completed! 🐙

A.4. Space derivative of electric and magnetic fields of a plane wave

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dh:electricField 𝓕.c A = planeWave P.electricFunction 𝓕.c.val s⊢ Space.deriv i (fun x => planeWave P.electricFunction 𝓕.c.val s t x) x = s.unit.val i • (fderiv ℝ P.electricFunction (⟪x, s.unit⟫_ℝ - 𝓕.c.val * t.val)) 1 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dh:electricField 𝓕.c A = planeWave P.electricFunction 𝓕.c.val s⊢ (s.unit.val i • fun x => planeWave (fun x => (fderiv ℝ P.electricFunction x) 1) 𝓕.c.val s t x) x = s.unit.val i • (fderiv ℝ P.electricFunction (⟪x, s.unit⟫_ℝ - 𝓕.c.val * t.val)) 1 All goals completed! 🐙d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Space.deriv k (fun x => ⟪x, s.unit⟫_ℝ) x = s.unit.val k ∨ _root_.deriv (fun u => P.magneticFunction u (i, j)) (⟪x, s.unit⟫_ℝ - 𝓕.c.val * t.val) = 0 All goals completed! 🐙

A.5. Space derivative in terms of time derivative

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dk:Fin d⊢ (s.unit.val k • (fderiv ℝ P.electricFunction (⟪x, s.unit⟫_ℝ - 𝓕.c.val * t.val)) 1).ofLp i = -(s.unit.val k / 𝓕.c.val) • (-𝓕.c.val • (fderiv ℝ P.electricFunction (⟪x, s.unit⟫_ℝ - 𝓕.c.val * t.val)) 1).ofLp id:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dk:Fin d⊢ Differentiable ℝ fun x_1 => electricField 𝓕.c A x_1 xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dk:Fin d⊢ Differentiable ℝ (electricField 𝓕.c A t) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dk:Fin d⊢ s.unit.val k * (_root_.deriv P.electricFunction (⟪x, s.unit⟫_ℝ - 𝓕.c.val * t.val)).ofLp i = s.unit.val k / 𝓕.c.val * (𝓕.c.val * (_root_.deriv P.electricFunction (⟪x, s.unit⟫_ℝ - 𝓕.c.val * t.val)).ofLp i)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dk:Fin d⊢ Differentiable ℝ fun x_1 => electricField 𝓕.c A x_1 xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dk:Fin d⊢ Differentiable ℝ (electricField 𝓕.c A t) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dk:Fin d⊢ Differentiable ℝ fun x_1 => electricField 𝓕.c A x_1 xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dk:Fin d⊢ Differentiable ℝ (electricField 𝓕.c A t) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dk:Fin d⊢ Differentiable ℝ fun x_1 => electricField 𝓕.c A x_1 x All goals completed! 🐙 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dk:Fin d⊢ Differentiable ℝ (electricField 𝓕.c A t) All goals completed! 🐙d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ s.unit.val k • (fderiv ℝ (fun u => P.magneticFunction u (i, j)) (⟪x, s.unit⟫_ℝ - 𝓕.c.val * t.val)) 1 = -(s.unit.val k / 𝓕.c.val) • -𝓕.c.val • (fderiv ℝ (fun u => P.magneticFunction u (i, j)) (⟪x, s.unit⟫_ℝ - 𝓕.c.val * t.val)) 1 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ s.unit.val k * _root_.deriv (fun u => P.magneticFunction u (i, j)) (⟪x, s.unit⟫_ℝ - 𝓕.c.val * t.val) = s.unit.val k / 𝓕.c.val * (𝓕.c.val * _root_.deriv (fun u => P.magneticFunction u (i, j)) (⟪x, s.unit⟫_ℝ - 𝓕.c.val * t.val)) All goals completed! 🐙

B. The magnetic field in terms of the electric field

B.1. Time derivative of the magnetic field in terms of electric field

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dhe:∀ (k : Fin d), DifferentiableAt ℝ (fun t => (electricField 𝓕.c A t x).ofLp k) t⊢ -(s.unit.val i / 𝓕.c.val) • ∂ₜ (fun x_1 => (electricField 𝓕.c A x_1 x).ofLp j) t - -(s.unit.val j / 𝓕.c.val) • ∂ₜ (fun x_1 => (electricField 𝓕.c A x_1 x).ofLp i) t = ∂ₜ (fun t => s.unit.val j / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp i - s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j) t conv_rhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dhe:∀ (k : Fin d), DifferentiableAt ℝ (fun t => (electricField 𝓕.c A t x).ofLp k) t| ((s.unit.val j / 𝓕.c.val) • fderiv ℝ (fun t => (electricField 𝓕.c A t x).ofLp i) t - (s.unit.val i / 𝓕.c.val) • fderiv ℝ (fun t => (electricField 𝓕.c A t x).ofLp j) t) 1 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dhe:∀ (k : Fin d), DifferentiableAt ℝ (fun t => (electricField 𝓕.c A t x).ofLp k) t⊢ -(s.unit.val i / 𝓕.c.val * ∂ₜ (fun x_1 => (electricField 𝓕.c A x_1 x).ofLp j) t) + s.unit.val j / 𝓕.c.val * ∂ₜ (fun x_1 => (electricField 𝓕.c A x_1 x).ofLp i) t = s.unit.val j / 𝓕.c.val * ∂ₜ (fun x_1 => (electricField 𝓕.c A x_1 x).ofLp i) t - s.unit.val i / 𝓕.c.val * ∂ₜ (fun x_1 => (electricField 𝓕.c A x_1 x).ofLp j) t d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dhe:∀ (k : Fin d), DifferentiableAt ℝ (fun t => (electricField 𝓕.c A t x).ofLp k) t⊢ -(s.unit.val i * ∂ₜ (fun x_1 => (electricField 𝓕.c A x_1 x).ofLp j) t) + s.unit.val j * ∂ₜ (fun x_1 => (electricField 𝓕.c A x_1 x).ofLp i) t = s.unit.val j * ∂ₜ (fun x_1 => (electricField 𝓕.c A x_1 x).ofLp i) t - s.unit.val i * ∂ₜ (fun x_1 => (electricField 𝓕.c A x_1 x).ofLp j) t All goals completed! 🐙

B.2. Space derivative of the magnetic field in terms of electric field

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ -(s.unit.val k / 𝓕.c.val * (s.unit.val j / 𝓕.c.val * ∂ₜ (fun t => (electricField 𝓕.c A t x).ofLp i) t - s.unit.val i / 𝓕.c.val * ∂ₜ (fun t => (electricField 𝓕.c A t x).ofLp j) t)) = s.unit.val j / 𝓕.c.val * -(s.unit.val k / 𝓕.c.val) • ∂ₜ (fun x_1 => (electricField 𝓕.c A x_1 x).ofLp i) t - s.unit.val i / 𝓕.c.val * -(s.unit.val k / 𝓕.c.val) • ∂ₜ (fun x_1 => (electricField 𝓕.c A x_1 x).ofLp j) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => (electricField 𝓕.c A t x).ofLp j) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => (electricField 𝓕.c A t x).ofLp i) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => s.unit.val j / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp i) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => (electricField 𝓕.c A t x).ofLp j) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => (electricField 𝓕.c A t x).ofLp i) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => s.unit.val j / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp i) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j) x d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ -(s.unit.val k / 𝓕.c.val * (s.unit.val j / 𝓕.c.val * ∂ₜ (fun t => (electricField 𝓕.c A t x).ofLp i) t - s.unit.val i / 𝓕.c.val * ∂ₜ (fun t => (electricField 𝓕.c A t x).ofLp j) t)) = -(s.unit.val j / 𝓕.c.val * (s.unit.val k / 𝓕.c.val * ∂ₜ (fun t => (electricField 𝓕.c A t x).ofLp i) t)) + s.unit.val i / 𝓕.c.val * (s.unit.val k / 𝓕.c.val * ∂ₜ (fun t => (electricField 𝓕.c A t x).ofLp j) t)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => (electricField 𝓕.c A t x).ofLp j) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => (electricField 𝓕.c A t x).ofLp i) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => s.unit.val j / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp i) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => (electricField 𝓕.c A t x).ofLp j) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => (electricField 𝓕.c A t x).ofLp i) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => s.unit.val j / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp i) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j) x d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ -(s.unit.val k * (s.unit.val j * ∂ₜ (fun t => (electricField 𝓕.c A t x).ofLp i) t - s.unit.val i * ∂ₜ (fun t => (electricField 𝓕.c A t x).ofLp j) t)) = s.unit.val k * (-(s.unit.val j * ∂ₜ (fun t => (electricField 𝓕.c A t x).ofLp i) t) + s.unit.val i * ∂ₜ (fun t => (electricField 𝓕.c A t x).ofLp j) t)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => (electricField 𝓕.c A t x).ofLp j) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => (electricField 𝓕.c A t x).ofLp i) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => s.unit.val j / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp i) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => (electricField 𝓕.c A t x).ofLp j) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => (electricField 𝓕.c A t x).ofLp i) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => s.unit.val j / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp i) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j) x d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => (electricField 𝓕.c A t x).ofLp j) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => (electricField 𝓕.c A t x).ofLp i) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => s.unit.val j / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp i) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun t => s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => (electricField 𝓕.c A t x).ofLp j) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => (electricField 𝓕.c A t x).ofLp i) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => s.unit.val j / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp i) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ DifferentiableAt ℝ (fun x => s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j) x any_goals d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ fun x => s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j any_goals d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ fun y => (electricField 𝓕.c A t y).ofLp j any_goals d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ fun y => (electricField 𝓕.c A t y).ofLp j any_goals All goals completed! 🐙

B.3. Magnetic field equal propogator cross electric field up to constant

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.vali:Fin dj:Fin dt:Timex:Space dk:Fin d⊢ Space.deriv k (fun x => s.unit.val j / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp i - s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j) x = Space.deriv k (fun x => 1 / 𝓕.c.val * (s.unit.val j * (electricField 𝓕.c A t x).ofLp i - s.unit.val i * (electricField 𝓕.c A t x).ofLp j)) x d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.vali:Fin dj:Fin dt:Timex:Space dk:Fin d⊢ (fun x => s.unit.val j / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp i - s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j) = fun x => 1 / 𝓕.c.val * (s.unit.val j * (electricField 𝓕.c A t x).ofLp i - s.unit.val i * (electricField 𝓕.c A t x).ofLp j) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ 2 A.vali:Fin dj:Fin dt:Timex✝:Space dk:Fin dx:Space d⊢ s.unit.val j / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp i - s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j = 1 / 𝓕.c.val * (s.unit.val j * (electricField 𝓕.c A t x).ofLp i - s.unit.val i * (electricField 𝓕.c A t x).ofLp j) All goals completed! 🐙

C. The electric field in terms of the magnetic field

C.1. The time derivative of the electric field in terms of magnetic field

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dhBd:∀ (k : Fin d), Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, k)h1:∂ₜ (fun t => ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j) t = ∑ j, ∂ₜ (fun x_1 => magneticFieldMatrix 𝓕.c A x_1 x (i, j)) t * s.unit.val jk:Fin d⊢ -(s.unit.val k * (-fderiv ℝ (fun t => magneticFieldMatrix 𝓕.c A t x (i, k)) t) 1) = s.unit.val k * ∂ₜ (fun x_1 => magneticFieldMatrix 𝓕.c A x_1 x (i, k)) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dhBd:∀ (k : Fin d), Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, k)⊢ DifferentiableAt ℝ (fun t => ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dhBd:∀ (k : Fin d), Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, k)⊢ ContDiff ℝ ∞ 0d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dhBd:∀ (k : Fin d), Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, k)⊢ Differentiable ℝ fun x_1 => electricField 𝓕.c A x_1 x d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dhBd:∀ (k : Fin d), Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, k)⊢ DifferentiableAt ℝ (fun t => ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dhBd:∀ (k : Fin d), Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, k)⊢ ContDiff ℝ ∞ 0d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dhBd:∀ (k : Fin d), Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, k)⊢ Differentiable ℝ fun x_1 => electricField 𝓕.c A x_1 x d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dhBd:∀ (k : Fin d), Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, k)⊢ DifferentiableAt ℝ (fun t => ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j) t d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dhBd:∀ (k : Fin d), Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, k)⊢ ∀ i_1 ∈ Finset.univ, DifferentiableAt ℝ (fun t => magneticFieldMatrix 𝓕.c A t x (i, i_1) * s.unit.val i_1) t d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dhBd:∀ (k : Fin d), Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, k)k:Fin da✝:k ∈ Finset.univ⊢ DifferentiableAt ℝ (fun t => magneticFieldMatrix 𝓕.c A t x (i, k) * s.unit.val k) t d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dhBd:∀ (k : Fin d), Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, k)k:Fin da✝:k ∈ Finset.univ⊢ DifferentiableAt ℝ (fun y => magneticFieldMatrix 𝓕.c A y x (i, k)) t All goals completed! 🐙 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dhBd:∀ (k : Fin d), Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, k)⊢ ContDiff ℝ ∞ 0 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dhBd:∀ (k : Fin d), Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, k)⊢ ContDiff ℝ ∞ fun x => 0 All goals completed! 🐙 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dhBd:∀ (k : Fin d), Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, k)⊢ Differentiable ℝ fun x_1 => electricField 𝓕.c A x_1 x All goals completed! 🐙

C.2. The space derivative of the electric field in terms of magnetic field

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ -(s.unit.val k / 𝓕.c.val * (𝓕.c.val * (s.unit.val j * (fderiv ℝ (fun t => magneticFieldMatrix 𝓕.c A t x (i, j)) t) 1))) = 𝓕.c.val * (s.unit.val j * -(s.unit.val k / 𝓕.c.val) • ∂ₜ (fun x_1 => magneticFieldMatrix 𝓕.c A x_1 x (i, j)) t)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ DifferentiableAt ℝ (fun x => magneticFieldMatrix 𝓕.c A t x (i, j)) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ DifferentiableAt ℝ (fun x => magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ DifferentiableAt ℝ (fun t => magneticFieldMatrix 𝓕.c A t x (i, j)) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.val⊢ ∀ i_1 ∈ Finset.univ, DifferentiableAt ℝ (fun x => 𝓕.c.val * (magneticFieldMatrix 𝓕.c A t x (i, i_1) * s.unit.val i_1)) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.val⊢ ∀ i_1 ∈ Finset.univ, DifferentiableAt ℝ (fun t => magneticFieldMatrix 𝓕.c A t x (i, i_1) * s.unit.val i_1) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.val⊢ DifferentiableAt ℝ (fun t => ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j) t d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ s.unit.val k / 𝓕.c.val * (𝓕.c.val * (s.unit.val j * ∂ₜ (fun t => magneticFieldMatrix 𝓕.c A t x (i, j)) t)) = 𝓕.c.val * (s.unit.val j * (s.unit.val k / 𝓕.c.val * ∂ₜ (fun t => magneticFieldMatrix 𝓕.c A t x (i, j)) t))d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ DifferentiableAt ℝ (fun x => magneticFieldMatrix 𝓕.c A t x (i, j)) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ DifferentiableAt ℝ (fun x => magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ DifferentiableAt ℝ (fun t => magneticFieldMatrix 𝓕.c A t x (i, j)) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.val⊢ ∀ i_1 ∈ Finset.univ, DifferentiableAt ℝ (fun x => 𝓕.c.val * (magneticFieldMatrix 𝓕.c A t x (i, i_1) * s.unit.val i_1)) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.val⊢ ∀ i_1 ∈ Finset.univ, DifferentiableAt ℝ (fun t => magneticFieldMatrix 𝓕.c A t x (i, i_1) * s.unit.val i_1) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.val⊢ DifferentiableAt ℝ (fun t => ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j) t d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ DifferentiableAt ℝ (fun x => magneticFieldMatrix 𝓕.c A t x (i, j)) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ DifferentiableAt ℝ (fun x => magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ DifferentiableAt ℝ (fun t => magneticFieldMatrix 𝓕.c A t x (i, j)) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.val⊢ ∀ i_1 ∈ Finset.univ, DifferentiableAt ℝ (fun x => 𝓕.c.val * (magneticFieldMatrix 𝓕.c A t x (i, i_1) * s.unit.val i_1)) xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.val⊢ ∀ i_1 ∈ Finset.univ, DifferentiableAt ℝ (fun t => magneticFieldMatrix 𝓕.c A t x (i, i_1) * s.unit.val i_1) td:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.val⊢ DifferentiableAt ℝ (fun t => ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j) t any_goals d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.val⊢ Differentiable ℝ fun t => ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ Differentiable ℝ fun x => magneticFieldMatrix 𝓕.c A t x (i, j) All goals completed! 🐙 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ Differentiable ℝ fun x => magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ Differentiable ℝ fun y => magneticFieldMatrix 𝓕.c A t y (i, j) All goals completed! 🐙 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.valj:Fin d⊢ Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i, j) All goals completed! 🐙 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.val⊢ ∀ i_1 ∈ Finset.univ, DifferentiableAt ℝ (fun x => 𝓕.c.val * (magneticFieldMatrix 𝓕.c A t x (i, i_1) * s.unit.val i_1)) x d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di✝:Fin dk:Fin dhA2:ContDiff ℝ 2 A.vali:Fin da✝:i ∈ Finset.univ⊢ DifferentiableAt ℝ (fun x => 𝓕.c.val * (magneticFieldMatrix 𝓕.c A t x (i✝, i) * s.unit.val i)) x d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di✝:Fin dk:Fin dhA2:ContDiff ℝ 2 A.vali:Fin da✝:i ∈ Finset.univ⊢ Differentiable ℝ fun x => 𝓕.c.val * (magneticFieldMatrix 𝓕.c A t x (i✝, i) * s.unit.val i) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di✝:Fin dk:Fin dhA2:ContDiff ℝ 2 A.vali:Fin da✝:i ∈ Finset.univ⊢ Differentiable ℝ fun y => magneticFieldMatrix 𝓕.c A t y (i✝, i) * s.unit.val i d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di✝:Fin dk:Fin dhA2:ContDiff ℝ 2 A.vali:Fin da✝:i ∈ Finset.univ⊢ Differentiable ℝ fun y => magneticFieldMatrix 𝓕.c A t y (i✝, i) All goals completed! 🐙 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.val⊢ ∀ i_1 ∈ Finset.univ, DifferentiableAt ℝ (fun t => magneticFieldMatrix 𝓕.c A t x (i, i_1) * s.unit.val i_1) t d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di✝:Fin dk:Fin dhA2:ContDiff ℝ 2 A.vali:Fin da✝:i ∈ Finset.univ⊢ DifferentiableAt ℝ (fun t => magneticFieldMatrix 𝓕.c A t x (i✝, i) * s.unit.val i) t d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di✝:Fin dk:Fin dhA2:ContDiff ℝ 2 A.vali:Fin da✝:i ∈ Finset.univ⊢ Differentiable ℝ fun t => magneticFieldMatrix 𝓕.c A t x (i✝, i) * s.unit.val i d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di✝:Fin dk:Fin dhA2:ContDiff ℝ 2 A.vali:Fin da✝:i ∈ Finset.univ⊢ Differentiable ℝ fun y => magneticFieldMatrix 𝓕.c A y x (i✝, i) All goals completed! 🐙 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.val⊢ Differentiable ℝ fun t => ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di:Fin dk:Fin dhA2:ContDiff ℝ 2 A.val⊢ ∀ i_1 ∈ Finset.univ, Differentiable ℝ fun y => magneticFieldMatrix 𝓕.c A y x (i, i_1) * s.unit.val i_1 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di✝:Fin dk:Fin dhA2:ContDiff ℝ 2 A.vali:Fin da✝:i ∈ Finset.univ⊢ Differentiable ℝ fun y => magneticFieldMatrix 𝓕.c A y x (i✝, i) * s.unit.val i d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0t:Timex:Space di✝:Fin dk:Fin dhA2:ContDiff ℝ 2 A.vali:Fin da✝:i ∈ Finset.univ⊢ Differentiable ℝ fun y => magneticFieldMatrix 𝓕.c A y x (i✝, i) All goals completed! 🐙

C.3. Electric field equal propogator cross magnetic field up to constant

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff ℝ ∞ A.valh:IsExtrema 𝓕 A 0i✝:Fin dhA2:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ IsExtrema 𝓕 A 0 All goals completed! 🐙