NonNeg
NonNeg asserts that a strain functional J on states satisfies J(x) ≥ 0 for every state x. RRF model builders cite it to guarantee that balanced states achieve the global minimum strain value. The declaration is a direct class definition with no proof obligations beyond the nonnegativity axiom.
claimA strain functional $S$ is non-negative when $S.J(x) ≥ 0$ for every state $x$.
background
In the RRF Core Strain module, strain measures deviation from equilibrium: a StrainFunctional on State is a structure containing a cost map J : State → ℝ such that J(x) = 0 precisely when x is balanced. The NonNeg class constraint adds the requirement that this cost is everywhere non-negative, turning the functional into a valid Lyapunov-like quantity for the recognition dynamics. Module documentation states that strain → 0 is the governing law and that lower strain corresponds to greater consistency with recognition rules. Upstream dependencies supply concrete State types (from CPM2D) and balanced-ledger predicates (from LedgerForcing) that instantiate the abstract interface.
proof idea
The declaration is a class definition that directly introduces the nonnegativity axiom ∀ x, 0 ≤ S.J x. No lemmas or tactics are invoked; it functions purely as an interface constraint for downstream results.
why it matters in Recognition Science
NonNeg is required by equilibria_are_minimizers (same module) and preserves_equilibria (Octave), both of which conclude that balanced states are minimizers once non-negativity holds. It encodes the core RRF principle that strain tends to zero, consistent with the recognition composition law and the eight-tick octave structure. The class closes the abstract interface used by concrete models such as quadratic1DStrain and trivialStrain.
scope and limits
- Does not prescribe any particular functional form for J beyond non-negativity.
- Does not assert uniqueness of equilibria or minimizers.
- Does not embed specific constants such as phi or the alpha band.
- Does not extend outside the RRF strain-functional interface.
Lean usage
instance : StrainFunctional.NonNeg quadratic1DStrain where nonneg := fun x => sq_nonneg xformal statement (Lean)
37class NonNeg (S : StrainFunctional State) : Prop where
38 nonneg : ∀ x, 0 ≤ S.J x
39
40/-- A state is balanced/equilibrium if its strain is exactly zero. -/