module module moderate

`IndisputableMonolith.Quantum.PageCurve`

The Quantum.PageCurve module constructs the Page curve for black hole entropy evolution inside Recognition Science. It defines the Boltzmann constant k_B together with evolving black hole states, page time, and ledger-derived entropy functions. Researchers modeling quantum information and black hole evaporation cite these objects to link RS cost primitives to the standard Page curve. The module is purely definitional, importing constants and cost functions to assemble the entropy expressions.

claimThe module introduces the Boltzmann constant $k_B$ in RS-native units, the page time $t_p$, the page entropy $S_{page}(t)$ for an evolving black hole, and the derived statements that information is preserved by the page curve with no firewall.

background

Recognition Science builds all constants from the forcing chain T0-T8, with the fundamental time quantum τ₀ = 1 tick supplied by the Constants module. The Cost module provides the J-cost function and defect distance used to track energy and information flow. This module applies those primitives to the quantum black hole sector, defining an evolving black hole whose radiation entropy follows the Page curve constructed from ledger evolution.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These definitions feed the downstream declarations information_preserved_by_page_curve and no_firewall. The module supplies the quantum-sector objects needed to connect the phi-ladder mass formula and the Recognition Composition Law to black hole evaporation, closing the link between the eight-tick octave and the observed Page curve.

scope and limits

Does not derive numerical Page time values outside RS units.
Does not model external fields or matter interactions.
Does not prove unitarity of ledger evolution.
Does not address firewall issues beyond the no_firewall declaration.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (17)

def k_B L42
structure EvolvingBlackHole L47
def remainingEntropy L57
def radiationEntropyNaive L61
def pageTime L68
def pageEntropy L79
theorem page_entropy_max_at_half L86
theorem page_entropy_final L92
theorem page_curve_from_ledger L105
structure LedgerEvolution L116
theorem information_preserved_by_page_curve L130
theorem no_firewall L145
def scramblingTime L157
theorem bh_fastest_scrambler L161
def recentBreakthroughs L174
def predictions L189
structure PageCurveFalsifier L202