set_option linter.style.longLine false

Magnetic Field and Final Assembly (Section 8)

Proves the magnetic field is spatially constant (from curl B = 0 and div B = 0), derives E = 0 from the Poisson-Boltzmann equation, and assembles the abstract ConcreteTheorem42 combining all sections.

theorem VML.magnetic_field_constant {X : Type u_1} [FlatTorus3 X] (ss : VMLSteadyState X) : ∃ (B₀ : Fin 3 → ℝ), ∀ (x : X), ss.B x = B₀

Lemma 22: Magnetic field is spatially constant. Reference: lem:B_constant

With u∞ = 0, J = 0 so ∇×B = 0. Combined with ∇·B = 0, each Bᵢ is harmonic on T³, hence constant.