helmholtz_split
plain-language theorem explainer
The theorem establishes that the velocity component of any NESS vector field decomposes additively into a gradient part and a circulating part. Researchers applying the free-energy principle to discrete non-equilibrium models would cite this identity when verifying vector-field splits. The proof is a direct unfolding of the two component definitions followed by ring simplification.
Claim. For any NESS vector field $X$ on index type $ι$, with velocity $v$, density $ρ$, and free-energy gradient $∇F$, one has $∀ i, v(i) = gradPart(X)(i) + circulatingPart(X)(i)$, where $gradPart(X)(i) := -∇F(i)$ and $circulatingPart(X)(i) := v(i) + ∇F(i)$.
background
NESSVectorField is a structure on an index type $ι$ carrying a velocity field $v : ι → ℝ$, a density $ρ : ι → ℝ$, and a free-energy gradient $∇F : ι → ℝ$. The module develops a finite-dimensional Helmholtz decomposition for such fields to support the FEP bridge in NESS dynamics. The two auxiliary definitions are gradPart, which returns the negative free-energy gradient, and circulatingPart, which returns the velocity plus the free-energy gradient.
proof idea
The proof introduces the index $i$, unfolds the definitions of gradPart and circulatingPart, and applies the ring tactic to obtain the additive identity.
why it matters
This supplies the split map required by helmholtzDecompositionCert_holds, which assembles the full HelmholtzDecompositionCert. It completes the decomposition step inside the Information module for NESS dynamics, consistent with the framework's use of vector-field splits in non-equilibrium steady states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.