DivergenceFree
plain-language theorem explainer
DivergenceFree encodes the discrete divergence-free condition for a real vector field on a finite index set by requiring its components to sum to zero. Workers on the free-energy principle bridge cite it when certifying circulation in finite NESS approximations. The definition is introduced as a direct equational predicate with no auxiliary lemmas.
Claim. A map $w:ι→ℝ$ on a finite set $ι$ is divergence-free when $∑_{i∈ι} w(i)=0$.
background
The module supplies a finite-dimensional Helmholtz decomposition for vector fields in non-equilibrium steady-state dynamics, serving the free-energy principle bridge. Sibling definitions introduce NESSVectorField together with its decomposition into a gradient part and a circulating part. The local setting is the information domain, where finite-type assumptions from Mathlib enable the discrete sum condition.
proof idea
One-line definition that directly equates the predicate to the vanishing of the total sum over the finite index set.
why it matters
The definition supplies the divergence-free condition required by the HelmholtzDecompositionCert structure, which certifies the split of any NESS vector field. It anchors the finite-dimensional treatment inside the information module of the Recognition Science framework. No open questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.