PageCurveDerived
plain-language theorem explainer
Packages the still-open claim that the dynamical black-hole Page curve has been derived as a Lean theorem in Recognition Science. Gravity and quantum-information workers cite it as the Track 3.C hypothesis input to the quantum-gravity master statement. It is a bare structure (proposition plus a proof field); no derivation is supplied here.
Claim. A witness consisting of a proposition asserting that the dynamical Page curve has been derived, together with a proof that this proposition holds. Intended content: unitary joint matter-radiation entropy evolution with replica-wormhole / quantum-extremal-surface comparison (Page-time $M^3$ scaling already closed elsewhere).
background
Module Gravity.MasterTheorem authors the Track 7.A master statement of the RS quantum-gravity program as a twelve-clause conjunction. Eight clauses are already discharged from Sessions 89–96 anchors; five remain open and are exposed as named hypothesis structures.
This structure is the Track 3.C slot. The classical Page curve says that the entanglement entropy of Hawking radiation first rises then falls back, restoring unitarity. In RS the Page-time $M^3$ scaling is already closed (Sessions 89, 91), but the dynamical entropy evolution of the joint matter-radiation system (replica wormholes, quantum extremal surfaces) is not yet a theorem.
Sibling hypothesis packages cover the D2 classical continuum limit, unconditional amplitude-linear forcing, PTA stochastic-GW distinctness from inflation, and strong-field tests distinct from GR. The master conditional theorem takes all five as inputs.
proof idea
No proof body: this is a structure definition with two fields, a proposition page_curve_derived and a proof holds that the proposition is true. Inhabiting an instance means supplying a completed dynamical Page-curve derivation. Downstream conditional masters simply thread the structure as a hypothesis; they do not construct it.
why it matters
One of the five open gates on the unconditional quantum-gravity master theorem. RSQuantumGravityMaster and rs_quantum_gravity_master_conditional (and the one-statement and partial variants) all take a PageCurveDerived argument; until Track 3.C closes, the master remains conditional.
In the framework this sits after the closed Hawking-temperature and black-hole-entropy SI anchors and beside the echo and discriminator certificates. It does not touch the T0–T8 forcing chain, RCL, or phi-ladder mass formula directly; it is the information-theoretic unitarity clause of the gravity track. Closing path: a multi-session theorem deriving dynamical entropy evolution (not merely Page-time scaling) that can inhabit this structure and retire the hypothesis from the master list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.