MPForcesLedger
plain-language theorem explainer
MPForcesLedger encodes the hypothesis that a recognition structure on type X supplies a charge map to integers under which every non-trivial transaction list sums to zero. DerivationChain cites this class to record the meta-principle step from recognition to ledger conservation. The structure is witnessed by an explicit instance on the unit type that uses the trivial recognition relation and zero charge.
Claim. Let $X$ be a type. Then $X$ satisfies MPForcesLedger when it is equipped with a recognition structure (a binary relation recognizes together with a witness of self-recognition), a charge function $c:X→ℤ$, and the property that every list of length greater than one has charge sum zero.
background
The Meta-Principle asserts that recognition requires a recognizer, so the empty collection cannot recognize itself. RecognitionStructure on $X$ consists of a relation recognizes : $X→X→$Prop together with a witness that some element recognizes itself. LedgerForcing supplies the balanced predicate on event lists, which MPForcesLedger lifts to the charge-sum condition on transactions.
proof idea
The declaration is a class definition. An instance is supplied for the unit type by setting recognizes to the always-true relation, charge to the constant zero function, and verifying the balanced condition by simplification.
why it matters
This class is referenced inside DerivationChain as the ledger-forcing step that follows recognition existence and precedes self-similarity forcing of φ. It implements the meta-principle implication that recognition pairing forces conservation, feeding the chain MP → Ledger → φ → constants. No open question is closed; the entry remains a hypothesis interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.