trivial_is_valid
plain-language theorem explainer
The trivial strain-ledger system meets the validity criterion at its single state. Model builders in the Recognition framework cite this result to verify the base case of the RRF axioms. The proof constructs the required conjunction directly from the balanced-strain and closed-ledger facts.
Claim. Let $S$ be the trivial strain-ledger system on the unit state. Then $S$ is valid, i.e., its strain is balanced and its ledger is closed at that state.
background
In the RRF framework a StrainLedger pairs a strain function with a ledger. Validity of a state $x$ requires the strain to be balanced at $x$ and the ledger to be closed at $x$, per the definition that a state is valid if it has zero strain and closed ledger. The trivial model takes the state space as the unit type, with zero strain (always balanced) and a trivially closed ledger; this pair is assembled as the trivial strain-ledger system. Upstream results establish that the single state is balanced and that the ledger is closed.
proof idea
The proof is a term-mode construction that directly supplies the pair consisting of the balanced-strain theorem and the closed-ledger theorem. This witnesses the conjunction inside the validity definition.
why it matters
This theorem confirms the internal consistency of the RRF axiom bundle in its simplest instantiation. It anchors the base case for the trivial model and thereby supports the broader claim that the core axioms are satisfiable. No downstream uses are recorded, but the result closes the consistency check for the Recognition framework's simplest RRF model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.