gradPart
plain-language theorem explainer
gradPart extracts the irrotational component of a finite-dimensional NESS vector field by negating its free energy gradient. Researchers applying the free energy principle to non-equilibrium dynamics cite this when splitting vector fields into conservative and circulatory parts. The definition is a direct one-line projection from the NESSVectorField record.
Claim. Let $X$ be a NESS vector field on index set $ι$. The gradient part is the map $i ↦ -∇F(i)$, where $∇F$ is the free energy gradient component of $X$.
background
The module supplies a finite-dimensional Helmholtz decomposition for NESS dynamics that serves as a bridge to the free energy principle. NESSVectorField is the structure holding a velocity field $v$, density $ρ$, and free energy gradient, all indexed by $ι$. This encodes the non-equilibrium steady-state vector field whose decomposition is certified by downstream results.
proof idea
The definition is a one-line wrapper that negates the freeEnergyGradient field of the input NESSVectorField.
why it matters
This definition supplies the gradient component required by HelmholtzDecompositionCert and the helmholtz_split theorem. It forms part of the vector-field decomposition used in the FEP bridge for information dynamics. No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.