trivial_balanced
plain-language theorem explainer
The trivial RRF model with a single state satisfies the zero-strain balance condition. Model builders checking base-case consistency in Recognition Science would cite this to anchor their constructions. The proof reduces immediately to reflexivity on the definition of balance.
Claim. For the trivial state space consisting of a single element, the associated strain functional satisfies $isBalanced(trivialStrain) = true$.
background
The RRF.Models.Trivial module constructs the simplest model satisfying the Recognition Science axioms: a single state (the unit type), with J-cost identically zero and a ledger that is trivially closed. The isBalanced predicate, defined in RRF.Core.Glossary as the zero-strain condition, requires that the total cost of the ledger is zero, matching the definition from Cosmology.DarkEnergy where isBalanced(R) holds when R.totalCost = 0. This trivial model serves as the base case for verifying the internal consistency of the core axiom bundle.
proof idea
The proof is a one-line term that applies reflexivity to the definition of isBalanced on the trivial strain.
why it matters
This result establishes the base case for the trivial model, feeding directly into the minimizer property via StrainFunctional.equilibria_are_minimizers and the validity theorem trivial_is_valid. It confirms that the simplest RRF model is consistent, aligning with the framework's requirement for internal consistency before extending to non-trivial states or the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.