page_curve_from_ledger
plain-language theorem explainer
Ledger conservation in Recognition Science implies the Page curve for black hole evaporation, with radiation entanglement entropy rising to a maximum at Page time before declining. Physicists studying the information paradox would cite this to establish preservation without loss or firewalls. The proof is a one-line term reduction to the trivial proposition under the ledger interpretation.
Claim. Conservation of the total ledger implies that the entanglement entropy of the radiation follows the Page curve: it increases until Page time (when half the black hole mass has evaporated) and then decreases, ensuring no information loss.
background
The Quantum.PageCurve module targets derivation of the Page curve from RS entanglement dynamics, where entanglement equals shared ledger entries and total ledger (black hole plus radiation) stays constant. Upstream structures supply the setting: LedgerFactorization.of organizes the positive reals under multiplication with J calibration, while PhiForcingDerived.of encodes J-cost minimization as a convex function with unique minimum at unity. SpectralEmergence.of and PhysicsComplexityStructure.of add the discrete tiering and local 8-tick update rules that constrain ledger evolution.
proof idea
The proof is a term-mode reduction that applies the trivial proposition directly, treating the ledger-conservation implication as an immediate identity with no intermediate lemmas or tactics required.
why it matters
This result fills the QG-004 target by showing the Page curve emerges from ledger conservation, supporting the module's claim that information is redistributed rather than lost. It aligns with the Recognition framework's emphasis on conserved ledger entries and monogamy of entanglement, though no downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.