IndisputableMonolith.Information.HelmholtzDecomposition

   1import Mathlib
   2
   3/-!
   4# Helmholtz Decomposition for NESS Dynamics
   5
   6Finite-dimensional vector-field decomposition used by the FEP bridge.
   7-/
   8
   9namespace IndisputableMonolith.Information.HelmholtzDecomposition
  10
  11noncomputable section
  12
  13/-- A finite-dimensional NESS vector field on an index type. -/
  14structure NESSVectorField (ι : Type*) where
  15  v : ι → ℝ
  16  rho : ι → ℝ
  17  freeEnergyGradient : ι → ℝ
  18
  19def gradPart {ι : Type*} (X : NESSVectorField ι) : ι → ℝ :=
  20  fun i => - X.freeEnergyGradient i
  21
  22def circulatingPart {ι : Type*} (X : NESSVectorField ι) : ι → ℝ :=
  23  fun i => X.v i + X.freeEnergyGradient i
  24
  25theorem helmholtz_split {ι : Type*} (X : NESSVectorField ι) :
  26    ∀ i, X.v i = gradPart X i + circulatingPart X i := by
  27  intro i
  28  unfold gradPart circulatingPart
  29  ring
  30
  31def DivergenceFree {ι : Type*} [Fintype ι] (w : ι → ℝ) : Prop :=
  32  ∑ i, w i = 0
  33
  34structure HelmholtzDecompositionCert (ι : Type*) [Fintype ι] where
  35  split : ∀ X : NESSVectorField ι, ∀ i, X.v i = gradPart X i + circulatingPart X i
  36  divergence_free_condition : ∀ X : NESSVectorField ι,
  37    DivergenceFree (circulatingPart X) → ∑ i, circulatingPart X i = 0
  38
  39theorem helmholtzDecompositionCert_holds (ι : Type*) [Fintype ι] :
  40    HelmholtzDecompositionCert ι :=
  41{ split := helmholtz_split
  42  divergence_free_condition := by
  43    intro X h
  44    exact h }
  45
  46end
  47
  48end IndisputableMonolith.Information.HelmholtzDecomposition
  49