dynamical_page_curve_one_statement
plain-language theorem explainer
Packages the dynamical Page curve as one conjunction: radiation entropy equals the min of linear bulk and radiation capacities, capacities sum to total entropy S, the curve vanishes at t=0 and t=1, peaks at S/2 when t=1/2, stays nonnegative on [0,1], and supplies a nonempty PageCurveDerived witness. Gravity Track 3.C auditors cite it as the Session 112 one-statement. Proof is a seven-component term pairing rfl with named lemmas and the dynamical witness.
Claim. For all real $S,t$: the unitarity Page curve equals $\min(S(1-t),\, S t)$; bulk plus radiation capacity equals $S$; if $S\ge 0$ then the curve is $0$ at $t=0$ and at $t=1$; the curve at $t=1/2$ equals $S/2$; if $S\ge 0$ and $t\in[0,1]$ the curve is nonnegative; and the master-theorem structure ``Page curve derived'' is inhabited.
background
Gravity Track 3.C replaces the Session 101 kinematic triangular ansatz with a derivation from Schmidt purification on a pure joint bulk⊗radiation state. Evaporation is parameterized by $t\in[0,1]$: bulk Hilbert-space entropy capacity falls linearly as $S_{\mathrm{BH}}(1-t)$, radiation capacity rises as $S_{\mathrm{BH}} t$. Their sum is the conserved total $S_{\mathrm{BH}}$.
Because unitary evolution from a pure initial bulk keeps the joint state pure, Schmidt's theorem forces $S(\rho_{\mathrm{bulk}})=S(\rho_{\mathrm{rad}})$ and both are bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$. Saturating that bound under maximal entanglement yields the Page curve as $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$.
Upstream, capacity_sum_invariant records bulk+radiation $=S$ by ring algebra on the linear definitions; pageCurveFromUnitarity is exactly that min; endpoint and half-time evaluations and nonnegativity are separate lemmas. PageCurveDerived is the MasterTheorem Track 3.C hypothesis structure whose holds field this module inhabits via the dynamical witness.
proof idea
Term-mode seven-tuple. First conjunct is definitional: pageCurveFromUnitarity unfolds to the min, so fun _ _ => rfl. Second is capacity_sum_invariant. Third through sixth are the named endpoint, half-time, and nonnegativity lemmas (pageCurveFromUnitarity_at_zero, _at_one, _at_half, _nonneg). Seventh is ⟨pageCurveDerivedWitness_dynamical⟩, inhabiting Nonempty PageCurveDerived with the dynamical Schmidt-purification witness rather than the Session 101 kinematic one. No new algebra is done here; the statement only bundles prior results.
why it matters
Session 112 one-statement for dynamical Track 3.C: the triangular Page curve (ascent, peak $S/2$ at Page time $t=1/2$, descent to zero at full evaporation) is forced by min-of-two-monotone-capacities under linear transfer plus Schmidt balance, not drawn by hand. Doc-comment states this supersedes the Session 101 kinematic ansatz in PageCurveStructural.
It closes the structural half of the master-theorem input PageCurveDerived by supplying a derivation-grade witness (pageCurveDerivedWitness_dynamical). The remaining unconditional gap, flagged in the doc-comment, is deriving the linear-in-$t$ capacity evolution itself from recognition-ledger bulk-to-radiation transfer rates; that is multi-session substrate work beyond this packaging theorem. No downstream users yet (used_by empty); the declaration is the module's exportable summary for MasterTheorem consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.