VML Data Structures

Defines the core data structures for the VML steady state problem:

• VMLSteadyState: intermediate bundle of derived facts
• VMLEquilibrium: the equilibrium configuration
• VMLInput: minimal physical input for the steady state problem

structure VML.VMLSteadyState (X : Type u_1) [FlatTorus3 X] : Type u_1

Intermediate bundle of DERIVED facts about a VML steady state on T³ × ℝ³.

This is NOT an input specification — all fields are proved from physical hypotheses in VMLInput.toSteadyState (VMLInputDerive.lean). It serves as an internal API between the derivation logic (Sections 3-7) and the final assembly (main_steady_state).

Encodes:

• The VML equations at steady state (Vlasov, Ampère, Gauss, div B = 0)
• Analytical results from the H-theorem chain (Sections 3-4 of tex)
• Polynomial matching results (Section 5 of tex)
• Maximum principle conclusion (Section 7 of tex)

• x₀ : X

  A distinguished base point of the spatial domain.

• f : X → (Fin 3 → ℝ) → ℝ

  The velocity distribution function f(x, v).

• E : X → Fin 3 → ℝ

  The electric field.

• B : X → Fin 3 → ℝ

  The magnetic field.

• ν : ℝ

  The collision frequency.

• ρIon : ℝ

  The (constant) ion background charge density.

• Ψ : ℝ → ℝ

  The collision kernel weight Ψ.

• hν : 0 < self.ν
• hρ_ion : 0 < self.ρIon
• hΨ (r : ℝ) : 0 < self.Ψ r
• hf_pos (x : X) (v : Fin 3 → ℝ) : 0 < self.f x v
• ρ : X → ℝ

  The charge density ρ(x) = ∫ f(x, v) dv.

• hρ_pos (x : X) : 0 < self.ρ x
• hρ_cont : Continuous self.ρ
• J : X → Fin 3 → ℝ

  The current density.

• hAmpere (x : X) : FlatTorus3.curlX self.B x = self.J x
• hGauss (x : X) : FlatTorus3.divX self.E x = self.ρ x - self.ρIon
• hDivB (x : X) : FlatTorus3.divX self.B x = 0
• hDiff_B (i : Fin 3) : FlatTorus3.IsSpatiallySmooth 2 fun (y : X) => self.B y i
• aLoc : X → ℝ

  The local log-density parameter a(x) in the Maxwellian form of f.

• bLoc : X → Fin 3 → ℝ

  The local drift parameter b(x) in the Maxwellian form of f.

• cLoc : X → ℝ

  The local inverse-temperature parameter c(x) in the Maxwellian form of f.

• hc_neg (x : X) : self.cLoc x < 0
• hMaxwellianForm (x : X) (v : Fin 3 → ℝ) : self.f x v = Real.exp (self.aLoc x + self.bLoc x ⬝ᵥ v + self.cLoc x * normSq v)
• c₀ : ℝ

  The constant value of cLoc.

• hc₀_neg : self.c₀ < 0
• hc_const (x : X) : self.cLoc x = self.c₀
• b₀ : Fin 3 → ℝ

  The constant drift direction b₀.

• hb_const (x : X) : self.bLoc x = (-2 * self.c₀) • self.b₀
• hForceBalance (x : X) : FlatTorus3.gradX self.aLoc x = -(2 * self.c₀) • (self.E x + cross self.b₀ (self.B x))
• hJ_def (x : X) : self.J x = self.ρ x • self.b₀
• hDensityConst (x : X) : self.ρ x = self.ρIon
• hGradA_zero : self.b₀ = 0 → (∀ (x : X), self.ρ x = self.ρIon) → ∀ (x : X), FlatTorus3.gradX self.aLoc x = 0
• hNormalization : self.b₀ = 0 → (∀ (x : X), self.ρ x = self.ρIon) → ∀ (x : X) (v : Fin 3 → ℝ), self.f x v = equilibriumMaxwellian self.ρIon (-1 / (2 * self.c₀)) v

structure VML.VMLEquilibrium : Type

The equilibrium configuration of a VML steady state.

• T : ℝ

  The equilibrium temperature.

• B₀ : Fin 3 → ℝ

  The equilibrium (constant) magnetic field.

• hT : 0 < self.T

structure VML.VMLInput (X : Type u_1) [FlatTorus3 X] : Type u_1

Minimal physical input for the VML steady state problem.

Contains:

• The physical state (f, E, B) on a spatial domain X with [FlatTorus3 X]
• Physical parameters (ν, ρIon, Ψ)
• Maxwell equations at steady state
• Entropy dissipation vanishes (from H-theorem chain)
• Analytical interface hypotheses (polynomial identity, Gaussian integrals)

The spatial operators (grad, div, curl, ∫) and their properties come from the FlatTorus3 typeclass instance, NOT from this structure.

The key distinction from VMLSteadyState: this structure does NOT include the Maxwellian parameters (a, b, c), temperature/drift constancy, or density constancy — those are DERIVED in toSteadyState.

• x₀ : X

  A distinguished base point of the spatial domain.

• f : X → (Fin 3 → ℝ) → ℝ

  The velocity distribution function f(x, v).

• E : X → Fin 3 → ℝ

  The electric field.

• B : X → Fin 3 → ℝ

  The magnetic field.

• ν : ℝ

  The collision frequency.

• ρIon : ℝ

  The (constant) ion background charge density.

• Ψ : ℝ → ℝ

  The collision kernel weight Ψ.

• hν : 0 < self.ν
• hρ_ion : 0 < self.ρIon
• hΨ (r : ℝ) : 0 < self.Ψ r
• hf_pos (x : X) (v : Fin 3 → ℝ) : 0 < self.f x v
• hf_smooth (x : X) : ContDiff ℝ 3 (self.f x)
• hf_int (x : X) : MeasureTheory.Integrable (self.f x) MeasureTheory.volume
• ρ : X → ℝ

  The charge density ρ(x) = ∫ f(x, v) dv.

• hρ_eq (x : X) : self.ρ x = ∫ (v : Fin 3 → ℝ), self.f x v
• hρ_pos (x : X) : 0 < self.ρ x
• hρ_cont : Continuous self.ρ
• J : X → Fin 3 → ℝ

  The current density.

• hAmpere (x : X) : FlatTorus3.curlX self.B x = self.J x
• hGauss (x : X) : FlatTorus3.divX self.E x = self.ρ x - self.ρIon
• hDivB (x : X) : FlatTorus3.divX self.B x = 0
• hDiff_fv (v : Fin 3 → ℝ) : FlatTorus3.IsSpatiallySmooth 2 fun (x : X) => self.f x v
• hDiff_B (i : Fin 3) : FlatTorus3.IsSpatiallySmooth 2 fun (y : X) => self.B y i
• hD_zero (x : X) : entropyDissipation self.Ψ (self.f x) = 0
• hScoreForm (x : X) : entropyDissipation self.Ψ (self.f x) = -(1 / 2) * ∫ (v : Fin 3 → ℝ) (w : Fin 3 → ℝ), PSDIntegrand self.Ψ (self.f x) v w
• hPSD_cont (x : X) : Continuous fun (p : (Fin 3 → ℝ) × (Fin 3 → ℝ)) => PSDIntegrand self.Ψ (self.f x) p.1 p.2
• hPSD_inner (x : X) (v : Fin 3 → ℝ) : MeasureTheory.Integrable (PSDIntegrand self.Ψ (self.f x) v) MeasureTheory.volume
• hPSD_outer (x : X) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => ∫ (w : Fin 3 → ℝ), PSDIntegrand self.Ψ (self.f x) v w) MeasureTheory.volume
• hDiff_maxwellian (a : X → ℝ) (b : X → Fin 3 → ℝ) (c : X → ℝ) : (∀ (x : X) (v : Fin 3 → ℝ), self.f x v = Real.exp (a x + b x ⬝ᵥ v + c x * normSq v)) → FlatTorus3.IsSpatiallySmooth 2 a ∧ (∀ (j : Fin 3), FlatTorus3.IsSpatiallySmooth 2 fun (y : X) => b y j) ∧ FlatTorus3.IsSpatiallySmooth 2 c
• hPolynomialIdentity (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 → ℝ), self.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 + self.E x ⬝ᵥ b x + v ⬝ᵥ ((2 * c x) • self.E x + cross (self.B x) (b x)) = 0
• hJ_from_maxwellian (b : X → Fin 3 → ℝ) (c₀ : ℝ) : (∀ (x : X), ∃ (a₀ : ℝ), ∀ (v : Fin 3 → ℝ), self.f x v = Real.exp (a₀ + b x ⬝ᵥ v + c₀ * normSq v)) → ∀ (x : X), self.J x = self.ρ x • (-1 / (2 * c₀)) • b x
• xMax : X

  A point where ρ attains its maximum (exists by compactness of T³).

• hmax (x : X) : self.ρ x ≤ self.ρ self.xMax
• xMin : X

  A point where ρ attains its minimum (exists by compactness of T³).

• hmin (x : X) : self.ρ self.xMin ≤ self.ρ x
• hPB_eq (c₀ : ℝ) : c₀ < 0 → (∀ (x : X), ∃ (a₀ : ℝ), ∀ (v : Fin 3 → ℝ), self.f x v = Real.exp (a₀ + c₀ * normSq v)) → ∀ (x : X), -1 / (2 * c₀) * FlatTorus3.divX (FlatTorus3.gradX (Real.log ∘ self.ρ)) x = self.ρ x - self.ρIon
• hNormalization (a₀ c₀ : ℝ) : c₀ < 0 → (∀ (x : X) (v : Fin 3 → ℝ), self.f x v = Real.exp (a₀ + c₀ * normSq v)) → (∀ (x : X), self.ρ x = self.ρIon) → ∀ (x : X) (v : Fin 3 → ℝ), self.f x v = equilibriumMaxwellian self.ρIon (-1 / (2 * c₀)) v