circulatingPart
plain-language theorem explainer
circulatingPart extracts the solenoidal component of a NESS vector field by adding its velocity field to the free energy gradient at each index. Researchers modeling non-equilibrium steady states via the free energy principle cite this definition when separating gradient-driven flow from divergence-free circulation. The definition is a direct pointwise sum with no additional computation or lemmas.
Claim. For a NESS vector field $X$ on index type $ι$, the circulating part is the function $i ↦ X.v(i) + X.freeEnergyGradient(i)$.
background
The module supplies a finite-dimensional Helmholtz decomposition for NESS dynamics as a bridge to the free energy principle. NESSVectorField is the structure holding a velocity field $v : ι → ℝ$, a density $ρ : ι → ℝ$, and a free energy gradient field, all indexed by the same type $ι$ (UPSTREAM: NESSVectorField doc). The decomposition isolates a gradient component from a circulating component whose divergence vanishes under the certificate conditions.
proof idea
The definition is a one-line wrapper that returns the pointwise sum of the velocity and free energy gradient components of the supplied NESSVectorField.
why it matters
circulatingPart supplies the second summand required by HelmholtzDecompositionCert and by the helmholtz_split theorem that proves the additive decomposition of any NESS vector field. It completes the local split used inside the Information domain for FEP-related vector-field analysis. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.