TrivialState
plain-language theorem explainer
The TrivialState abbreviation supplies the singleton state space for the minimal RRF model. Researchers verifying internal consistency of the Recognition axiom bundle cite it when constructing explicit realizations with zero strain. The definition is a direct one-line alias to the unit type.
Claim. The state space of the trivial RRF model is the singleton set given by the unit type.
background
The RRF.Models.Trivial module builds the simplest model satisfying the RRF axioms. State equals the unit type (one state), the strain functional J is identically zero (always balanced), and the ledger is 0/0 (trivially closed). This proves internal consistency of the core axiom bundle as stated in the module documentation.
proof idea
One-line abbreviation that directly sets TrivialState to the unit type.
why it matters
This supplies the base state space for all trivial constructions in the module, including trivialStrain, trivialLedger, trivialChannel, trivialChannelBundle, trivialOctave, and trivialStrainLedger. It closes the consistency proof for the RRF axiom system by exhibiting an explicit model where J-cost is zero and the ledger constraint holds. The construction aligns with the Recognition Science goal of deriving physics from a single functional equation by providing a minimal fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.