ledger_identity
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not address ledger states with infinite event lists.
- Does not incorporate tick indices or temporal evolution.
- Does not define or compute J-cost or entropy values.
- Does not assert uniqueness or ordering of events within the list.
formal statement (Lean)
203theorem ledger_identity (s₁ s₂ : LedgerState) :
204 s₁.events = s₂.events ↔ s₁ = s₂ := by
proof body
Term-mode proof.
205 constructor
206 · intro h; cases s₁; cases s₂; simp_all
207 · intro h; rw [h]
208
209/-! ## §VI. The Landauer Connection -/
210
211/-- The Landauer constant: k_B ln(2) (in J/K). -/