StrainLedger
plain-language theorem explainer
StrainLedger pairs a strain functional with a ledger constraint to represent the complete RRF state evaluation. Model builders constructing consistent state spaces in recognition-based physics cite this structure when assembling valid configurations. The definition is a direct bundling of the two component structures with no additional axioms or reductions.
Claim. A strain ledger on a state space $S$ consists of a strain functional $J:S→ℝ$ (non-negative and zero precisely at equilibrium) together with a ledger constraint supplying debit and credit maps $S→ℤ$.
background
Strain is the fundamental measure of deviation from equilibrium in RRF, with the associated functional assigning a non-negative real cost to each state such that the cost vanishes if and only if the state is balanced. The ledger constraint requires that the sum of debits equals the sum of credits for every state. The module supplies the abstract interface for these objects, where strain approaching zero encodes the recognition law and lower strain corresponds to greater consistency.
proof idea
The declaration is a structure definition that directly assembles the StrainFunctional and LedgerConstraint records; no lemmas or tactics are applied.
why it matters
This structure supplies the core data type for RRF state evaluation and is referenced by consistentStates, isConsistent, isValid and validStates. It is instantiated in the quadratic 1D and trivial models, thereby operationalizing the combination of J-cost minimization with ledger balance inside the recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.