IndisputableMonolith.RRF.Core.Strain
The RRF.Core.Strain module defines the strain functional as a non-negative real-valued cost on states that vanishes precisely at equilibrium. Framework researchers cite this when formalizing cost structures for minimization and state ordering in RRF. The module supplies a collection of definitions for StrainFunctional, balance predicates, and minimizer properties with no theorem proofs.
claimA strain functional is a map $J: S → ℝ$ such that $J(x) ≥ 0$ for all states $x$, with equality if and only if $x$ is balanced.
background
In the Reality Recognition Framework the strain functional supplies the cost measure for states. The module defines StrainFunctional with real codomain and nonnegativity as a class constraint, together with the key property that cost is zero exactly at equilibrium. It introduces supporting notions such as isBalanced for equilibrium states, equilibria for the zero-strain set, LedgerConstraint for balance conditions, and net for aggregate strain. These definitions establish the vocabulary for comparing states by cost.
proof idea
This is a definition module, no proofs. It declares the StrainFunctional structure, adds the NonNeg constraint, and defines auxiliary predicates including isBalanced, strictlyBetter, weaklyBetter, isMinimizer, hasUniqueMin, and equilibria_are_minimizers by direct unfolding of the cost-zero condition.
why it matters in Recognition Science
This module supplies the core strain concept re-exported in RRF.Core and referenced in Glossary, Octave, VantageCategory, and OrderPreservation. It fills the foundational role for defining costs that enables theorems on order preservation under strain-based comparisons. The definitions align with the framework emphasis on relative ordering of states by strain rather than absolute values.
scope and limits
- Does not specify any concrete functional form for J beyond nonnegativity and zero at equilibrium.
- Does not introduce physical constants, phi scalings, or octave relations.
- Does not prove existence or uniqueness of equilibria or minimizers.
- Does not extend beyond real-valued codomain or basic order predicates.