LedgerState
plain-language theorem explainer
LedgerState packages a finite list of recognition events, each a positive real ratio encoding a physical fact with its associated J-cost. Information theorists formalizing Wheeler's it-from-bit as a ledger identity in Recognition Science cite this when deriving total information cost or thermodynamic bounds. The declaration is a direct structure with one field and no computational reduction.
Claim. A ledger state is a finite list of recognition events, where each event consists of a positive real ratio $x > 0$ together with a proof that the ratio is positive.
background
The module InformationIsLedger formalizes IC-001, the claim that information is the physical ledger rather than an abstraction. RecognitionEvent is the sibling structure holding a ratio : ℝ with ratio_pos : ratio > 0, so that every physical fact appears as a positive ratio whose information content is its J-cost. J(x) vanishes exactly at x = 1 (balanced state) and is symmetric under x ↦ 1/x, with J(x) → ∞ as x → 0⁺. Upstream results supply RecognitionEvent variants in LedgerForcing and ObserverForcing that already tie the ratio to a recognition process between agents or states.
proof idea
Direct structure definition. The single field events : List RecognitionEvent is declared with an inline doc-comment; no tactics or lemmas are invoked.
why it matters
LedgerState supplies the basic object for the IC-001 suite. It is the domain of totalInfoCost, which sums infoCost over the list, and of ledger_identity, which equates two states precisely when their event lists coincide. Downstream it feeds diagonalHamiltonian in HamiltonianEmergence and the thermodynamic hypothesis H_ThermodynamicsVerified. The structure therefore anchors the framework claim that information content equals J-cost and that the zero-cost state is the unique balanced ledger entry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.