NonNeg
plain-language theorem explainer
NonNeg declares that a strain functional J satisfies J(x) ≥ 0 for every state x. Concrete models such as quadratic strain and trivial strain supply instances of the class. The declaration is a single-field class that supplies the nonnegativity hypothesis used by minimizer and morphism theorems.
Claim. A strain functional $S$ on a state space is non-negative when $S.J(x) ≥ 0$ for every state $x$.
background
In the RRF setting strain measures deviation from equilibrium, with the law that strain tends to zero. The StrainFunctional structure supplies a map $J$ from states to reals; the separate NonNeg class adds the requirement that this map is everywhere non-negative. The module states that $J(x) = 0$ precisely when the state is balanced.
proof idea
This is a class definition whose single field is the universal quantification ∀ x, 0 ≤ S.J x.
why it matters
NonNeg is invoked by equilibria_are_minimizers to conclude that balanced states are minimizers and by Octave.preserves_equilibria to transfer equilibrium across morphisms. It therefore supports the RRF claim that lower strain corresponds to greater consistency and feeds the forcing chain in which balance is the fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.