BlackHoleLedger
plain-language theorem explainer
BlackHoleLedger records a list of falling entries compressed on the horizon together with their aggregate information count under an explicit summation invariant. Physicists resolving the black hole information paradox cite the structure to enforce unitarity via ledger preservation rather than loss. The definition is a direct structure bundling the list, the natural-number total, and the equality constraint with no separate proof obligations.
Claim. A black hole ledger is a triple $(E, I, C)$ where $E$ is a list of falling entries, $I$ is a natural number giving total information bits, and $C$ is the equality $I = sum_{e in E} information(e)$.
background
Recognition Science resolves the black hole information paradox by making the horizon a compressed ledger rather than an erasure surface. A falling entry carries its original bit count, infall time, and an explicit preservation assertion that the entry is compressed but not destroyed. The module frames the setting as QG-003, where every physical event is a ledger entry, black-hole formation performs holographic compression to the Planck-area bound, and Hawking radiation performs the corresponding decompression.
proof idea
This is a structure definition that directly assembles the entries list, the total-information natural number, and the summation equality as a single field. No lemmas or tactics are invoked; the consistency predicate is part of the type itself.
why it matters
BlackHoleLedger supplies the data type for the downstream results addEntry, information_preserved_on_infall, and information_conservation, which together establish that information is neither created nor lost during infall or evaporation. It instantiates the QG-003 claim that the ledger remains unitary throughout the process, aligning with the framework's insistence that information is fundamental and with the holographic bound realized by phi-ladder compression.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.