pageCurveDerivedWitness_recognitionTicks
plain-language theorem explainer
Packages the dynamical Page-curve derivation with the recognition-tick capacity-transfer law into a typed MasterTheorem Page-curve witness. Gravity auditors and the unconditional master-theorem assembly cite it as the tick-route certificate that Track 3.C is theorem-built rather than postulated. The body is a one-line structure packing of an already-proved conjunction.
Claim. There is a master-theorem witness asserting that the Page curve is derived: the recognition-tick capacity-transfer law holds and the dynamical Page-curve property holds (Schmidt-balanced radiation entropy equals $\min(\mathrm{bulk\,capacity},\mathrm{radiation\,capacity})$ along the evaporation parameter $t\in[0,1]$).
background
Module Gravity.PageCurveDynamical derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating a piecewise-linear ansatz. Evaporation is parameterized by $t\in[0,1]$: bulk capacity falls as $S_{BH}(1-t)$, radiation capacity grows as $S_{BH},t$. 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 balance the radiation entropy saturates that bound, yielding the triangle with forced peak at $t=1/2$.
Upstream, PageCurveDerived is the Track 3.C master-theorem slot: a proposition plus a proof that it holds. The strengthened proposition here is the conjunction of the recognition-tick capacity-transfer law with the dynamical Page-curve property; that conjunction is already proved as a pair of holds theorems.
proof idea
Definitional witness construction, not a tactic proof. The structure field page_curve_derived is set to the strengthened proposition (recognition-tick transfer $\land$ dynamical Page curve). The holds field is filled by the theorem that proves that conjunction by pairing recognition_tick_capacity_transfer_prop_holds with page_curve_derived_dynamical_prop_holds. No new algebra is done at this site.
why it matters
Closes the master-theorem interface for Track 3.C along the recognition-tick route: the Page curve is no longer a kinematic ansatz from PageCurveStructural but a derived min-of-capacities under Schmidt purity, bundled with the tick transfer law. Downstream, canonicalPageCurveDerivedWitness_tickRoute in MasterTheoremUnconditional aliases this witness and documents that the older recognition-tick route remains valid under audit. In the RS gravity stack this is the certificate that dynamical entropy evolution (bulk/radiation ledger) feeds the unconditional master theorem without leaving the Page-curve slot open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.