ledger_identity
plain-language theorem explainer
Ledger states are identical precisely when their lists of recognition events coincide. This encodes the it-from-bit principle inside Recognition Science by making the ledger the sole carrier of physical identity. The proof splits the biconditional via constructor, reduces the forward direction by cases and simp_all, and closes the reverse by rewriting.
Claim. For any two ledger states $s_1$ and $s_2$, $s_1 = s_2$ if and only if the lists of recognition events in $s_1$ and $s_2$ are identical.
background
LedgerState is the structure whose sole field is a finite list of RecognitionEvent objects; each event encodes a recognition ratio carrying a J-cost. The module InformationIsLedger treats this structure as the physical substrate, so that information content is literally the ledger content rather than an abstraction layered on top. Upstream, the same LedgerState pattern appears in VariationalDynamics (with tick and configuration) and in Thermodynamics (with active bonds), but the local version strips to events alone to isolate the information identity.
proof idea
The term proof opens with constructor to split the biconditional. The left-to-right direction cases on both structures and invokes simp_all to obtain equality from matching event lists. The right-to-left direction applies rw on the supplied equality hypothesis to finish the identification.
why it matters
The theorem supplies the basic extensionality axiom for the ledger in the IC-001 cluster, directly supporting the Landauer connection and the claim that Shannon entropy equals expected J-cost. It closes the identity step required before any cost or entropy calculation can be performed on ledger states. No open scaffolding remains for this identity itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.