NESSVectorField
plain-language theorem explainer
A structure that bundles a vector field v, density rho, and free-energy gradient on an arbitrary index type ι. Researchers applying the free-energy principle to non-equilibrium steady-state flows cite this record when preparing inputs for the Helmholtz split. The definition is a direct record constructor with three projections and no proof content.
Claim. A NESS vector field on an index set $ι$ consists of a vector field $v:ι→ℝ$, a density $ρ:ι→ℝ$, and a free-energy gradient $∇F:ι→ℝ$.
background
The module develops a finite-dimensional Helmholtz decomposition for non-equilibrium steady-state dynamics in the free-energy principle bridge. NESSVectorField supplies the three components required for the split: the total field v, the density rho, and the free-energy gradient. No prior lemmas are invoked; the structure is the foundational input type for gradPart, circulatingPart, and the decomposition certificate.
proof idea
Direct structure definition. The three fields are introduced by record syntax with no computational body or proof obligations.
why it matters
This record is the input type for helmholtz_split and HelmholtzDecompositionCert, which establish the decomposition v = gradPart + circulatingPart together with the divergence-free condition on the circulatory component. It therefore anchors the information-theoretic treatment of steady-state flows inside the Recognition Science information domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.