HelmholtzDecompositionCert
plain-language theorem explainer
HelmholtzDecompositionCert packages the split identity and zero-sum implication for any finite-dimensional NESS vector field into gradient and circulating parts. Researchers bridging the free-energy principle to Recognition Science cite the structure when certifying that the circulating component obeys the divergence-free condition. The declaration is introduced as a plain structure definition that directly assembles the two properties from the sibling definitions of gradPart and circulatingPart.
Claim. Let $ι$ be a finite index set. A HelmholtzDecompositionCert consists of two properties: for every NESS vector field $X$ with velocity component $v$, free-energy gradient $g$, and density $ρ$, the identity $X.v(i) = -g(i) + (v(i) + g(i))$ holds for all $i$; and whenever the circulating part $w(i) = v(i) + g(i)$ satisfies $∑_i w(i) = 0$, the sum $∑_i w(i)$ equals zero.
background
The module supplies a finite-dimensional vector-field decomposition used by the FEP bridge. An NESSVectorField on index type $ι$ is the structure carrying a velocity map $v:ι→ℝ$, a density map $ρ:ι→ℝ$, and a freeEnergyGradient map $g:ι→ℝ$. The auxiliary definitions set gradPart$(X)(i) := -g(i)$ and circulatingPart$(X)(i) := v(i) + g(i)$. DivergenceFree on a map $w$ is the proposition $∑_i w(i) = 0$.
proof idea
The declaration is a direct structure definition. No lemmas or tactics are applied; the two fields are stated explicitly by reference to the sibling definitions of gradPart, circulatingPart, and DivergenceFree.
why it matters
The certificate is the type instantiated by the downstream theorem helmholtzDecompositionCert_holds, which supplies the split identity from helmholtz_split and discharges the zero-sum implication by reflexivity. It therefore supplies the interface required to certify the decomposition step inside the information-theoretic treatment of NESS dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.