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.valDifferentiable fun u => electricField 𝓕.c A { val := -u / 𝓕.c.val } 0 d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valDifferentiable ((electricField 𝓕.c A) fun u => ({ val := -u / 𝓕.c.val }, 0)) d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valDifferentiable fun u => ({ val := -u / 𝓕.c.val }, 0) d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valDifferentiable fun u => { val := -u / 𝓕.c.val }d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valDifferentiable fun u => 0 d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valDifferentiable fun u => { val := -u / 𝓕.c.val } d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valDifferentiable (toRealCLE.symm fun u => -u / 𝓕.c.val) All goals completed! 🐙 d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valDifferentiable fun u => 0 All goals completed! 🐙d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valij:Fin d × Fin dDifferentiable 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 dDifferentiable 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 dDifferentiable ((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 dDifferentiable fun u => ({ val := -u / 𝓕.c.val }, 0) d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valij:Fin d × Fin dDifferentiable fun u => { val := -u / 𝓕.c.val }d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valij:Fin d × Fin dDifferentiable fun u => 0 d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valij:Fin d × Fin dDifferentiable fun u => { val := -u / 𝓕.c.val } d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valij:Fin d × Fin dDifferentiable (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 dDifferentiable 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 sSpace.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 dSpace.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 dDifferentiable 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 dDifferentiable (electricField 𝓕.c A t) d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valt:Timex:Space di:Fin dk:Fin ds.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 dDifferentiable 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 dDifferentiable (electricField 𝓕.c A t) d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valt:Timex:Space di:Fin dk:Fin dDifferentiable 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 dDifferentiable (electricField 𝓕.c A t) d:𝓕:FreeSpaceA:ElectromagneticPotential ds:Direction dP:IsPlaneWave 𝓕 A shA:ContDiff 2 A.valt:Timex:Space di:Fin dk:Fin dDifferentiable 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 dDifferentiable (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 ds.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 ds.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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiable 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 dDifferentiable 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 dDifferentiable 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 dSpace.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 ds.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.univDifferentiableAt (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.univDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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.valDifferentiableAt (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 ds.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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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.valDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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 dDifferentiableAt (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.valDifferentiableAt (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.valDifferentiable 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 dDifferentiable 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 dDifferentiable 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 dDifferentiable 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 dDifferentiable 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.univDifferentiableAt (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.univDifferentiable 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.univDifferentiable 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.univDifferentiable 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.univDifferentiableAt (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.univDifferentiable 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.univDifferentiable 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.valDifferentiable 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.univDifferentiable 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.univDifferentiable 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 dIsExtrema 𝓕 A 0 All goals completed! 🐙