trivialLedger
plain-language theorem explainer
The trivial ledger supplies a zero-valued debit and credit map on the single-point state space. Researchers checking internal consistency of the RRF axiom bundle cite this base case before moving to non-trivial states. It is realized by a direct definition that populates the two fields of the LedgerConstraint structure with constant-zero functions.
Claim. Let $U$ be the trivial state space consisting of a single point. The trivial ledger is the structure $LedgerConstraint(U)$ with $debit(u) := 0$ and $credit(u) := 0$ for the unique element $u$ of $U$.
background
The module presents the simplest model satisfying RRF axioms: state space reduced to the unit type (one state), J-cost identically zero, and ledger entries zero on both sides. The LedgerConstraint structure requires two maps from states to integers (debit and credit) whose sums are equal, thereby enforcing closure. This construction is imported from the core strain module and serves as the base case that verifies the axiom bundle admits at least the trivial solution.
proof idea
Direct definition that instantiates the LedgerConstraint structure by supplying the constant-zero function for both the debit and credit fields on TrivialState.
why it matters
This definition supplies the ledger component of the trivial strain-ledger system, which is invoked by the downstream theorems trivial_ledger_closed and trivialStrainLedger. It fills the base case confirming that the core RRF axiom bundle (including the ledger constraint) is internally consistent, prior to deriving physical content such as the eight-tick octave or spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.