StrainFunctional
plain-language theorem explainer
A strain functional on a state space S is a map J: S → ℝ that assigns a real cost to each state. Workers in the RRF layer of Recognition Science cite this structure when they need an abstract cost that vanishes exactly at balanced equilibria. The declaration is a plain structure definition that introduces the J field together with a namespace containing the derived predicates isBalanced and isMinimizer.
Claim. A strain functional on a state space $S$ is a function $J:S→ℝ$ that assigns a cost to each state, with the understanding that $J(x)=0$ precisely when $x$ is balanced.
background
In the RRF core module, strain is the primitive measure of deviation from equilibrium: lower strain corresponds to greater consistency with recognition laws, and the governing principle is that strain tends to zero. The structure therefore supplies only the codomain ℝ and the J field; non-negativity and the zero-at-equilibrium property are imposed later by class constraints and predicates. Upstream results that calibrate J appear in LedgerFactorization (structure of (ℝ₊,×) and calibration of J) and in the multiplicative recognizer cost functions.
proof idea
This is a structure definition. It declares the single field J: State → ℝ and opens a namespace in which the predicates isBalanced, isMinimizer, and the associated lemmas are stated.
why it matters
The structure is the common interface for every later RRF object that carries a cost: it is instantiated inside the Octave structure, supplies the J abbreviation and the JMinimizationLaw in the Glossary, and is the hypothesis of the preserves_equilibria theorem. It therefore realizes the abstract “J → 0” drive that the framework places at the center of RRF before any concrete φ-ladder or eight-tick octave is added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.