trivialStrainLedger
plain-language theorem explainer
The trivial strain-ledger equips the single-point state space with a zero strain functional and a zero debit-credit ledger. Researchers checking internal consistency of the Recognition framework cite it as the base case for the RRF axiom bundle. The definition is a direct record construction that pairs the sibling trivial strain and trivial ledger components.
Claim. The trivial strain-ledger on the unit state space is the structure whose strain component is the always-zero functional and whose ledger component is the zero debit-credit constraint.
background
The RRF.Models.Trivial module constructs the simplest model satisfying the Recognition framework axioms. TrivialState is the unit type containing one state. StrainLedger is the structure that combines a strain functional with a ledger constraint; here both are set to zero so that J-cost is identically zero and the ledger is closed by construction.
proof idea
This definition constructs the StrainLedger record by direct field assignment of the trivial strain functional to the strain slot and the trivial ledger to the ledger slot. No lemmas or tactics are applied beyond the structural constructor.
why it matters
It supplies the base case used by the downstream theorem trivial_is_valid to establish that the trivial state satisfies the validity predicate. The module documentation states that this proves internal consistency of the core axiom bundle, serving as the minimal instance before non-trivial models are considered in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.