set_option linter.style.longLine false

Deriving VMLInput from Concrete Hypotheses

Constructs a VMLInput from a VMLSteadyState and VelocityDecayConditions, then applies the abstract proof chain (Sections 2-8) to derive the main theorem ConcreteTheorem42 with minimal physical hypotheses.

theorem VML.main_steady_state {X : Type u_1} [FlatTorus3 X] (ss : VMLSteadyState X) : ∃ (eq : VMLEquilibrium), (∀ (x : X) (v : Fin 3 → ℝ), ss.f x v = equilibriumMaxwellian ss.ρ_ion eq.T v) ∧ (∀ (x : X), ss.E x = 0) ∧ ∀ (x : X), ss.B x = eq.B₀

Main Theorem: Global steady state of the VML system. Reference: Theorem 12 (thm:main)

Any smooth steady state (f, E, B) on T³ × ℝ³ with ν > 0 is: (i) f = ρ_ion/(2πT∞)^{3/2} exp(-|v|²/(2T∞)) (global Maxwellian, zero drift) (ii) E = 0 (iii) B = B∞ (spatially constant) (iv) T∞ > 0 is a constant parameter characterizing the steady-state family

Proof assembles: Step 1: f is local Maxwellian (Corollary 2, via H-theorem chain) Step 2: T is constant (Lemma 14, O(|v|³) terms) Step 3: u is constant (Lemma 15, Killing's equation on T³) Step 4: u = 0 (Lemma 19, Ampère + divergence theorem) Step 5: n ≡ ρ_ion, E = 0 (Lemmas 20-21, Poisson–Boltzmann + max principle) Step 6: B constant (Lemma 22, harmonic on T³) Step 7: Parameters from conservation (Lemmas 24-28)

noncomputable def VML.VMLInput.a_loc {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) : X → ℝ

Equations

• p.a_loc x = Exists.choose ⋯

noncomputable def VML.VMLInput.b_loc {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) : X → Fin 3 → ℝ

Equations

• p.b_loc x = ⋯.choose

noncomputable def VML.VMLInput.c_loc {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) : X → ℝ

Equations

• p.c_loc x = ⋯.choose

theorem VML.VMLInput.hc_neg {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) (x : X) : p.c_loc x < 0

theorem VML.VMLInput.hMaxwellianForm {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) (x : X) (v : Fin 3 → ℝ) : p.f x v = Real.exp (p.a_loc x + p.b_loc x ⬝ᵥ v + p.c_loc x * normSq v)

theorem VML.VMLInput.hDiff_abc {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) : FlatTorus3.IsSpatiallySmooth 2 p.a_loc ∧ (∀ (j : Fin 3), FlatTorus3.IsSpatiallySmooth 2 fun (y : X) => p.b_loc y j) ∧ FlatTorus3.IsSpatiallySmooth 2 p.c_loc

IsSpatiallySmooth 2 for the Maxwellian parameters a_loc, b_loc, c_loc.

theorem VML.VMLInput.hc_const_grad {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) (x : X) : FlatTorus3.gradX p.c_loc x = 0

Temperature is spatially constant: c(x) ≡ c₀.

noncomputable def VML.VMLInput.c₀ {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) : ℝ

Extract the constant temperature parameter c₀.

Equations

• p.c₀ = p.c_loc p.x₀

theorem VML.VMLInput.hc₀_neg {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) : p.c₀ < 0

theorem VML.VMLInput.hc_const {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) (x : X) : p.c_loc x = p.c₀

theorem VML.VMLInput.hKilling {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) (x : X) (i j : Fin 3) : FlatTorus3.gradX (fun (y : X) => p.b_loc y j) x i + FlatTorus3.gradX (fun (y : X) => p.b_loc y i) x j = 0

The O(|v|²) Killing equation from the polynomial identity.

theorem VML.VMLInput.hb_const_exists {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) : ∃ (b₀ : Fin 3 → ℝ), ∀ (x : X), p.b_loc x = b₀

Drift velocity b is constant on T³.

noncomputable def VML.VMLInput.b₀ {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) : Fin 3 → ℝ

Extract the constant drift parameter b₀.

Equations

• p.b₀ = ⋯.choose

theorem VML.VMLInput.hb_const {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) (x : X) : p.b_loc x = p.b₀

theorem VML.VMLInput.hForceBalance {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) (x : X) : FlatTorus3.gradX p.a_loc x = -(2 * p.c₀) • p.E x + cross p.b₀ (p.B x)

Force balance from the polynomial identity.

theorem VML.VMLInput.hJ_def' {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) (x : X) : p.J x = p.ρ x • (-1 / (2 * p.c₀)) • p.b₀

Current density J = ρ · drift velocity.

theorem VML.VMLInput.hb₀_zero {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) : p.b₀ = 0

The drift parameter b₀ vanishes. Proof: Ampère + Stokes on T³ gives |u₀|² ∫ ρ = 0, and ∫ ρ > 0, so u₀ = (-1/(2c₀))b₀ = 0, hence b₀ = 0 since c₀ ≠ 0.

theorem VML.VMLInput.hPB {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) (x : X) : -1 / (2 * p.c₀) * FlatTorus3.divX (FlatTorus3.gradX (Real.log ∘ p.ρ)) x = p.ρ x - p.ρ_ion

Poisson-Boltzmann equation for the density.

theorem VML.VMLInput.hDensityConst {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) (x : X) : p.ρ x = p.ρ_ion

Density is constant: ρ(x) = ρ_ion.

theorem VML.VMLInput.hGradA_zero {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) : p.b₀ = 0 → (∀ (x : X), p.ρ x = p.ρ_ion) → ∀ (x : X), FlatTorus3.gradX p.a_loc x = 0

∇a vanishes when b₀ = 0 and ρ = ρ_ion.

theorem VML.VMLInput.hNorm {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) : p.b₀ = 0 → (∀ (x : X), p.ρ x = p.ρ_ion) → ∀ (x : X) (v : Fin 3 → ℝ), p.f x v = equilibriumMaxwellian p.ρ_ion (-1 / (2 * p.c₀)) v

f is the equilibrium Maxwellian when b₀ = 0 and ρ = ρ_ion.

noncomputable def VML.VMLInput.toSteadyState {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) : VMLSteadyState X

Build VMLSteadyState from VMLInput by deriving all analytical conclusions.

Equations

• One or more equations did not get rendered due to their size.

theorem VML.main_from_physics {X : Type u_1} [FlatTorus3 X] (p : VMLInput X) : ∃ (eq : VMLEquilibrium), (∀ (x : X) (v : Fin 3 → ℝ), p.f x v = equilibriumMaxwellian p.ρ_ion eq.T v) ∧ (∀ (x : X), p.E x = 0) ∧ ∀ (x : X), p.B x = eq.B₀

Main theorem (honest version): From physical inputs alone, any smooth steady state (f, E, B) on T³ × ℝ³ with ν > 0 is: (i) f = ρ_ion/(2πT∞)^{3/2} exp(-|v|²/(2T∞)) (global Maxwellian, zero drift) (ii) E = 0 (iii) B = B∞ (spatially constant) (iv) T∞ > 0 is a constant parameter characterizing the steady-state family