theorem VML.maxwellian_landau_flux_zero (Ψ : ℝ → ℝ) (f : (Fin 3 → ℝ) → ℝ) (a₀ : ℝ) (b : Fin 3 → ℝ) (c₀ : ℝ) (hf : ∀ (v : Fin 3 → ℝ), f v = Real.exp (a₀ + b ⬝ᵥ v + c₀ * normSq v)) (v w : Fin 3 → ℝ) : (landauMatrix Ψ (v - w)).mulVec (f w • vGrad f v - f v • vGrad f w) = 0

Gap 8: For a log-quadratic f = exp(a₀ + b·v + c₀|v|²), the Landau flux vanishes. This follows because ∇log f(v) - ∇log f(w) = 2c₀(v-w), so the flux is proportional to A(v-w)(v-w) = 0 by Lemma 3 (projection annihilation). Reference: Key step in the proof of Theorem 5 (thm:nullspace_sufficiency).

theorem VML.IsMaxwellian.landauOperator_eq_zero {f : (Fin 3 → ℝ) → ℝ} (Ψ : ℝ → ℝ) (hM : IsMaxwellian f) (v : Fin 3 → ℝ) : LandauOperator Ψ f v = 0

Maxwellians are in the nullspace of the Landau operator: Q(f,f) = 0. The flux A(v-w)[f(w)∇f(v) - f(v)∇f(w)] vanishes pointwise (because ∇log f is affine, so the score difference is proportional to v-w, which is annihilated by A(v-w)), making the integral and its divergence zero.

theorem VML.D_zero_implies_maxwellian (Ψ : ℝ → ℝ) (f : (Fin 3 → ℝ) → ℝ) (hΨ : ∀ (r : ℝ), 0 < Ψ r) (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (hf_smooth : ContDiff ℝ 3 f) (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (hD : entropyDissipation Ψ f = 0) (hScoreForm : entropyDissipation Ψ f = -(1 / 2) * ∫ (v : Fin 3 → ℝ) (w : Fin 3 → ℝ), PSDIntegrand Ψ f v w) (hPSD_cont : Continuous fun (p : (Fin 3 → ℝ) × (Fin 3 → ℝ)) => PSDIntegrand Ψ f p.1 p.2) (hPSD_inner : ∀ (v : Fin 3 → ℝ), MeasureTheory.Integrable (PSDIntegrand Ψ f v) MeasureTheory.volume) (hPSD_outer : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => ∫ (w : Fin 3 → ℝ), PSDIntegrand Ψ f v w) MeasureTheory.volume) : IsMaxwellian f

Gap 11: D(f) = 0 implies f is a Maxwellian. Chains: D=0 → parallelism (Lemma 6) → ∇log f affine (Lemma 7) → log f quadratic (Lemma 8) → f = exp(quadratic) → c₀ < 0 (L¹ integrability). Reference: Proof of Theorem 4 (thm:nullspace_necessity) + Corollary 2.