page_curve_derived_structural_prop_holds
plain-language theorem explainer
Existence of positive parameters for which the triangular Page-curve shape satisfies its structural boundary and nonnegativity conditions. Gravity and quantum-information workers cite it as the kinematic witness that retires the Page-curve hypothesis on the RS quantum-gravity master theorem. The proof is a short term construction: fix unit peak and Page time, then discharge the four shape lemmas.
Claim. There exist $S_{\max}>0$ and $t_{\mathrm{Page}}>0$ such that the triangular Page curve $S(t)$ obeys $S(0)=0$, $S(t_{\mathrm{Page}})=S_{\max}$, $S(2 t_{\mathrm{Page}})=0$, and $S(t)\ge 0$ for all $t$.
background
Track 3.C of the RS quantum-gravity master plan asks for a Page curve from ledger structure. The full dynamical derivation (replicas, quantum extremal surfaces, back-reaction, unitary bulk-plus-radiation evolution) is heavy. This module ships only the kinematic content: a piecewise-linear triangular entropy profile that encodes the standard early-rise / late-fall / post-evaporation-zero shape.
Concretely, trianglePageCurve S_max t_Page t 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 stays identically zero thereafter. The sibling lemmas record the corner values and nonnegativity. The structural proposition packages existence of positive $S_{\max}$ and $t_{\mathrm{Page}}$ together with those four shape facts; that package is exactly the hypothesis input PageCurveDerived expected by rs_quantum_gravity_master_conditional in Gravity.MasterTheorem.
proof idea
Term-mode construction via refine on a six-field structure. Instantiate $S_{\max}=1$ and $t_{\mathrm{Page}}=1$, discharge positivity by norm_num, then fill the four remaining goals by the sibling shape lemmas: value $0$ at $t=0$, value $S_{\max}$ at the Page time, value $0$ at twice the Page time, and nonnegativity for every $t$ (the last under the same positivity side conditions, again by norm_num). No analysis beyond the piecewise-linear definition is required.
why it matters
This is the proved inhabitant that lets pageCurveDerivedWitness assemble a PageCurveDerived record for the master theorem. Downstream, that witness retires the Page-curve hypothesis from rs_quantum_gravity_master_conditional, converting one conditional arm of the Session-97 quantum-gravity master package into an unconditional structural input.
In the broader RS gravity track it closes the kinematic half of Track 3.C ("Page curve from ledger structure"): the triangular profile is the shape every unitary evaporation story must reproduce at the entropy level. It does not yet supply the ledger dynamics or the replica/QES construction; those remain the open heavy sessions flagged in the module status. Framework-wise it sits on the gravity side of the forcing chain rather than on T5–T8, but it is the concrete entropy-shape fact the master QG theorem consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.