pageCurveDerivedWitness_dynamical
plain-language theorem explainer
Packages the dynamical Schmidt-purification derivation of the triangular Page curve as a witness for the master-theorem interface that expects a derived Page curve. Gravity and black-hole information workers cite it when discharging the Page-curve hypothesis without a kinematic ansatz. The body is a structure inhabitant: it points the interface field at the dynamical proposition and its already-proved holds lemma.
Claim. There is a witness of type $\mathsf{PageCurveDerived}$ whose derived-curve field is the dynamical proposition: radiation entropy equals $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$ under linear bulk$\otimes$radiation transfer and Schmidt balance for pure joint states, with the holds proof supplied by the corresponding dynamical lemma.
background
Track 3.C derives the Page curve from Schmidt-balanced ledger dynamics rather than postulating a piecewise-linear shape. Evaporation is parameterized by $t\in[0,1]$: bulk capacity falls as $S_{BH}(1-t)$, radiation capacity rises as $S_{BH},t$, and their sum is conserved. Unitary evolution from a pure bulk state keeps the joint bulk$\otimes$radiation state pure, so Schmidt forces equal reduced entropies bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$.
Under maximal Schmidt entanglement the radiation entropy saturates that bound, yielding $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$. That minimum is the triangular Page curve, with peak forced at $t=1/2$. Session 101 only installed the triangle as a kinematic ansatz; this module replaces that ansatz by the capacity-min form.
The master theorem exposes a hypothesis interface $\mathsf{PageCurveDerived}$ that packages "the Page curve has been derived." This definition is the dynamical inhabitant of that interface.
proof idea
One-line structure construction. The definition fills the $\mathsf{PageCurveDerived}$ record by setting the derived-curve field to the dynamical proposition page_curve_derived_dynamical_prop and the holds field to the already-established lemma that that proposition is true. No new algebra is performed here; it is a witness assembly point over the dynamical derivation already proved in-module.
why it matters
Closes the master-theorem input for a derivation-grade Page curve: the triangular shape is $\min$ of two monotone capacities, not a hand-built piecewise linear function. Downstream, dynamical_page_curve_one_statement packages the full one-statement claim (curve equals the min, capacity sum invariant, endpoints zero, peak $S_{BH}/2$ at Page time), and pageCurveDynamicalCert bundles the certificate fields (curve def, invariant, phase equalities, peak). Together they supersede the Session 101 kinematic witness with a structural theorem (module status: 0 sorry, 0 RS-internal axiom). In the broader RS gravity track this is the information-theoretic half of black-hole evaporation bookkeeping on the ledger, complementary to eight-tick and $D=3$ forcing elsewhere in the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.