pageCurveDerivedWitness
plain-language theorem explainer
Inhabitant of the master-theorem hypothesis type for a derived Page curve. It packages the structural (kinematic triangular) existence proposition and its proof as the content of that hypothesis. Anyone assembling the structural or deeper-partial quantum-gravity master theorem cites this witness. Construction is a direct structure instance, not a new argument.
Claim. There is an inhabitant of the master-theorem hypothesis type "Page curve derived" whose proposition field is the structural claim: there exist $S_{\max}>0$ and $t_{\mathrm{Page}}>0$ such that the triangular Page curve equals $0$ at $t=0$, equals $S_{\max}$ at $t=t_{\mathrm{Page}}$, equals $0$ at $t=2 t_{\mathrm{Page}}$, and is nonnegative for all $t$; and whose holds field is a proof of that proposition.
background
Track 3.C of the quantum-gravity master plan asks for a Page curve from ledger structure. The full dynamical derivation (replica wormholes / quantum extremal surfaces, evaporation dynamics, back-reaction, unitary evolution on bulk ledger tensor Hawking radiation) is multi-session work. This module ships only the kinematic content: a piecewise-linear triangular shape and its shape lemmas, plus a master-theorem hypothesis witness.
The triangular curve rises linearly from $0$ to $S_{\max}$ on $[0,t_{\mathrm{Page}}]$, falls linearly back to $0$ on $[t_{\mathrm{Page}},2 t_{\mathrm{Page}}]$, and is identically zero thereafter. That encodes early thermal radiation growth, a Page-time peak equal to remaining black-hole entropy, late-time purification, and full information return at complete evaporation.
Upstream, PageCurveDerived is the open Track 3.C hypothesis structure: a proposition field plus a proof that it holds. The structural proposition asserts existence of positive $S_{\max},t_{\mathrm{Page}}$ with the four shape properties above; a sibling theorem proves it by exhibiting the unit parameters $(1,1)$ and invoking the pointwise triangle lemmas.
proof idea
Definitional structure instance, not a tactic proof. The proposition field is set to the structural existence proposition (exists positive peak entropy and Page time with zero/peak/end/nonnegativity for the triangular curve). The holds field is filled by the already-proved theorem that that proposition is true, which itself refines with witnesses $S_{\max}=1$, $t_{\mathrm{Page}}=1$ and applies the pointwise evaluations at zero, peak, and end together with nonnegativity.
why it matters
Retires the Page-curve hypothesis input on the conditional master theorem by supplying a concrete structural witness. Downstream it is wired into the fully structural master theorem (zero remaining hypothesis inputs at the Lean skeleton level), the structural master cert, the honest-scope statement that records which witnesses are inhabited, the deeper-partial conditional master theorem, and the one-statement Page-curve packaging in this module.
In framework terms this is kinematic closure of Track 3.C only: the triangular shape is theorem-grade with zero sorry. The discovery-grade claim still needs the dynamical upgrade named in the honest-scope note (ledger dynamics rather than a prescribed triangle). Page-time $M^3$ scaling is already closed elsewhere; entropy evolution remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.