set_option linter.style.longLine false

Concrete Theorem 4.2 for Coulomb Collisions on T^3

Specializes the abstract ConcreteTheorem42 to the Coulomb kernel Psi(r) = r^{-3}, the physically most important case in plasma physics. Verifies all 19 fields of VelocityDecayConditions for Coulomb and states the main result: any smooth steady state of the VML system with Coulomb collisions is a global Maxwellian with E = 0 and B = const.

theorem VML.CoulombConcreteTheorem42 (f : Torus3 → (Fin 3 → ℝ) → ℝ) (E B : Torus3 → Fin 3 → ℝ) (ν ρ_ion : ℝ) (hν : 0 < ν) (hρ_ion : 0 < ρ_ion) (hf_pos : ∀ (x : Torus3) (v : Fin 3 → ℝ), 0 < f x v) (hf_smooth_v : ∀ (x : Torus3), ContDiff ℝ 3 (f x)) (hf_smooth_x : ∀ (v : Fin 3 → ℝ), ContDiff ℝ 2 (periodicLift fun (x : Torus3) => f x v)) (hB_smooth : ∀ (i : Fin 3), ContDiff ℝ 2 (periodicLift fun (x : Torus3) => B x i)) (hSchwartz : UniformSchwartzDecay f) (hGradBound : ∃ (Cg : ℝ) (Kg : ℕ), ∀ (x : Torus3) (v : Fin 3 → ℝ) (i : Fin 3), |(fderiv ℝ (f x) v) (Pi.single i 1)| ≤ Cg * (1 + ‖v‖) ^ Kg * f x v) (hVlasov : ∀ (x : Torus3) (v : Fin 3 → ℝ), v ⬝ᵥ torusGradX (fun (y : Torus3) => f y v) x + (E x + cross v (B x)) ⬝ᵥ vGrad (f x) v = ν * LandauOperator coulombKernel (f x) v) (hAmpere : ∀ (x : Torus3), torusCurlX B x = fun (i : Fin 3) => ∫ (v : Fin 3 → ℝ), v i * f x v) (hGauss : ∀ (x : Torus3), torusDivX E x = (∫ (v : Fin 3 → ℝ), f x v) - ρ_ion) (hDivB : ∀ (x : Torus3), torusDivX B x = 0) : ∃ (T_eq : ℝ) (B₀ : Fin 3 → ℝ), 0 < T_eq ∧ (∀ (x : Torus3) (v : Fin 3 → ℝ), f x v = equilibriumMaxwellian ρ_ion T_eq v) ∧ (∀ (x : Torus3), E x = 0) ∧ ∀ (x : Torus3), B x = B₀

Coulomb Theorem 42. Characterization of smooth steady states of the Vlasov–Maxwell–Landau system with Coulomb collisions on T³ = (ℝ/ℤ)³.

Note on Physical Rigor: This theorem addresses the classic non-relativistic formulation over $v \in \mathbb{R}^3$. As with all non-relativistic kinetic theory over an unbounded velocity space, this formally admits unphysical superluminal velocities ($|v| > c$). A strictly correct physical model would require replacing $v$ with momentum $p$.

This is the physically most important case: Coulomb interactions between charged particles in a plasma. The collision kernel Ψ(r) = r⁻³ is singular at r = 0 but the formalization handles this via the PSD continuity condition in VelocityDecayConditions (the singularity cancels in the quadratic form).

Hypotheses (12 total):

• 2 physical parameters (ν > 0, ρ_ion > 0)
• 1 strict positivity (f > 0)
• 3 smoothness (f smooth in v and x, B smooth)
• 2 decay (uniform C² velocity decay; polynomial score bound)
• 4 equations (Vlasov, Ampère, Gauss, div B = 0)

Independence note: The polynomial score bound (hGradBound) is NOT derivable from the Schwartz decay alone. The ratio |∂f|/f equals |∂f| * exp(C(1+‖v‖)^K) in the worst case, which grows super-polynomially for K ≥ 1. Counterexample: f(v) = exp(-|v|²)(2 + sin(exp(⟨v⟩))) is Schwartz with stretched-exponential lower bound, but |∂f|/f grows like exp(⟨v⟩). The polynomial score bound is a genuine additional assumption, satisfied by physically relevant distributions (Maxwellians, perturbations thereof).

Coulomb-specificity of hGradBound: This hypothesis is needed solely to handle the Coulomb singularity Ψ(r) = r⁻³. The score difference ∇log f(v) − ∇log f(w) = O(|v−w|) cancels the 1/|v−w| blow-up of the Coulomb collision matrix, ensuring PSD integrability. For bounded kernels (e.g. Maxwell molecules with Ψ = const), the abstract Theorem42 applies without any score bound hypothesis.

Restrictiveness of hGradBound: The polynomial score bound forces a strict lower bound on the decay rate of $f$. It actively excludes many standard Schwartz class functions, such as those with faster-than-exponential decay (e.g., $f(v) = \exp(-\exp(\|v\|))$), because their logarithmic gradient grows too fast. Thus, while the theorem covers Maxwellians, it strictly prohibits solutions that vanish too rapidly at infinity.

Scope: Single species, non-relativistic, 3D flat torus, Coulomb kernel (Ψ(r) = r⁻³). Assumes existence of a smooth positive steady-state solution.

theorem VML.CoulombConcreteTheorem42_classify_T (f : Torus3 → (Fin 3 → ℝ) → ℝ) (E B : Torus3 → Fin 3 → ℝ) (ν ρ_ion : ℝ) (hν : 0 < ν) (hρ_ion : 0 < ρ_ion) (hf_pos : ∀ (x : Torus3) (v : Fin 3 → ℝ), 0 < f x v) (hf_smooth_v : ∀ (x : Torus3), ContDiff ℝ 3 (f x)) (hf_smooth_x : ∀ (v : Fin 3 → ℝ), ContDiff ℝ 2 (periodicLift fun (x : Torus3) => f x v)) (hB_smooth : ∀ (i : Fin 3), ContDiff ℝ 2 (periodicLift fun (x : Torus3) => B x i)) (hSchwartz : UniformSchwartzDecay f) (hGradBound : ∃ (Cg : ℝ) (Kg : ℕ), ∀ (x : Torus3) (v : Fin 3 → ℝ) (i : Fin 3), |(fderiv ℝ (f x) v) (Pi.single i 1)| ≤ Cg * (1 + ‖v‖) ^ Kg * f x v) (hVlasov : ∀ (x : Torus3) (v : Fin 3 → ℝ), v ⬝ᵥ torusGradX (fun (y : Torus3) => f y v) x + (E x + cross v (B x)) ⬝ᵥ vGrad (f x) v = ν * LandauOperator coulombKernel (f x) v) (hAmpere : ∀ (x : Torus3), torusCurlX B x = fun (i : Fin 3) => ∫ (v : Fin 3 → ℝ), v i * f x v) (hGauss : ∀ (x : Torus3), torusDivX E x = (∫ (v : Fin 3 → ℝ), f x v) - ρ_ion) (hDivB : ∀ (x : Torus3), torusDivX B x = 0) : ∃ (T_eq : ℝ) (B₀ : Fin 3 → ℝ), 0 < T_eq ∧ (∀ (x : Torus3) (v : Fin 3 → ℝ), f x v = equilibriumMaxwellian ρ_ion T_eq v) ∧ (∀ (x : Torus3), E x = 0) ∧ (∀ (x : Torus3), B x = B₀) ∧ ∀ (T' : ℝ), 0 < T' → (∀ (v : Fin 3 → ℝ), equilibriumMaxwellian ρ_ion T' v = equilibriumMaxwellian ρ_ion T_eq v) → T' = T_eq

The steady state is parameterized by an injective temperature T_eq. Note: T_eq is uniquely determined by the state f itself via injectivity, but the overall theorem classifies a family of steady states parameterized by T > 0 and B₀ ∈ ℝ³.