Polynomial Matching (Section 5)

Temperature is spatially constant, Lorentz force expansion, and polynomial identity matching that constrains the Maxwellian parameters (a, b, c) from the Vlasov transport equation.

theorem VML.lorentz_force_expansion (E b B v : Fin 3 → ℝ) (c : ℝ) : (E + cross v B) ⬝ᵥ (b + (2 * c) • v) = E ⬝ᵥ b + v ⬝ᵥ ((2 * c) • E + cross B b)

Expansion of (E + v×B)·(b + 2cv) = E·b + v·(2cE + B×b). Uses (v×B)·v = 0 and (v×B)·b = v·(B×b). Proved by Aristotle (Harmonic).

theorem VML.temperature_constant (X : Type u_1) (c : X → ℝ) (gradX : (X → ℝ) → X → Fin 3 → ℝ) (hcubic : ∀ (x : X) (v : Fin 3 → ℝ), v ⬝ᵥ gradX c x * normSq v = 0) (x : X) : gradX c x = 0

Lemma 14 (Temperature is spatially constant). Reference: lem:T_constant

Under the conditions of Lemma 13, ∇ₓc = 0, i.e., T(x) ≡ T∞ is a global constant.

Proof: The O(|v|³) terms give (v · ∇c)|v|² = 0 for all v. Choosing v = t eᵢ for t → ∞ shows ∂ₓᵢ c = 0 for each i. Since c = -1/(2T), T is constant.

theorem VML.polynomial_identity_from_vlasov {X : Type u_1} [FlatTorus3 X] (f : X → (Fin 3 → ℝ) → ℝ) (E B : X → Fin 3 → ℝ) (Ψ : ℝ → ℝ) (ν : ℝ) (_hf_pos : ∀ (x : X) (v : Fin 3 → ℝ), 0 < f x v) (_hf_smooth : ∀ (x : X), ContDiff ℝ 3 (f x)) (_hf_int : ∀ (x : X), MeasureTheory.Integrable (f x) MeasureTheory.volume) (_hΨ : ∀ (r : ℝ), 0 < Ψ r) (_hVlasov : ∀ (x : X) (v : Fin 3 → ℝ), v ⬝ᵥ FlatTorus3.gradX (fun (y : X) => f y v) x + (E x + cross v (B x)) ⬝ᵥ vGrad (f x) v = ν * LandauOperator Ψ (f x) v) (a : X → ℝ) (b : X → Fin 3 → ℝ) (c : X → ℝ) : FlatTorus3.IsSpatiallySmooth 2 a → (∀ (j : Fin 3), FlatTorus3.IsSpatiallySmooth 2 fun (y : X) => b y j) → FlatTorus3.IsSpatiallySmooth 2 c → (∀ (x : X) (v : Fin 3 → ℝ), f x v = Real.exp (a x + b x ⬝ᵥ v + c x * normSq v)) → ∀ (x : X) (v : Fin 3 → ℝ), v ⬝ᵥ FlatTorus3.gradX c x * normSq v + ∑ i : Fin 3, ∑ j : Fin 3, v i * v j * FlatTorus3.gradX (fun (y : X) => b y j) x i + v ⬝ᵥ FlatTorus3.gradX a x + E x ⬝ᵥ b x + v ⬝ᵥ ((2 * c x) • E x + cross (B x) (b x)) = 0

Polynomial identity from the Vlasov equation. When f has Maxwellian form exp(a + b·v + c|v|²), the Landau operator vanishes (nullspace sufficiency), so the Vlasov equation reduces to collisionless transport. Expanding and dividing by f > 0 gives a polynomial in v. Reference: Lemma 13 (lem:polynomial_identity) in H-theorem-formal.tex.