canonicalPageCurveDerivedWitness
plain-language theorem explainer
Canonical D4 Page-curve witness for the unconditional RS quantum-gravity master assembly. It packages the nontrivial two-by-two Page process: capacity-curve entropy readout, interior peak at half the Bekenstein–Hawking value, and strict monotone rise then fall. Downstream non-circularity audits and the zero-argument master theorem cite it as the standalone D4 input. Proof shape is a one-line alias of the nontrivial derived witness.
Claim. There is a canonical inhabited D4 witness of type ``Page-curve derived'': the recognition-tick capacity-transfer law holds, and on the finite Hilbert space $\mathbb{C}^2\otimes\mathbb{C}^2$ there is a triangular Page curve (arbitrary tick budget) whose derived capacity-curve entropy has an interior peak equal to $S_{\mathrm{BH}}/2$, is monotone before and after that peak, and rises and falls strictly across it. This replaces the degenerate one-dimensional identity/zero-entropy witness.
background
The module Gravity.MasterTheoremUnconditional installs theorem-built witnesses for the five inputs that the older conditional RS quantum-gravity master theorem took as arguments. The conditional statement stays the audit surface; this file supplies the zero-argument route.
D4 is the Page-curve slot. In MasterTheorem, PageCurveDerived is a thin structure: a proposition page_curve_derived together with a proof that it holds. Historically Track 3.C treated dynamical Page evolution (unitary matter–radiation, replica/QES comparison) as heavy open work; the Page-time $M^3$ scaling was already closed. Peer-review finding F3 rejected a vacuous Fin 1 identity witness with zero entropy.
The nontrivial replacement lives in PageCurveNontrivial: a recognition-tick capacity-transfer law conjoined with a nondegenerate Page shape on Fin 2 ⊗ Fin 2 (triangular curve, interior peak $S_{BH}/2$, strict monotone limbs). The audit theorem d4_page_field_is records that equality by rfl.
proof idea
One-line definitional wrapper. The body is exactly PageCurveNontrivial.nontrivialPageCurveDerivedWitness, which already inhabits MasterTheorem.PageCurveDerived with the strengthened nontrivial content. No new tactics or lemmas are applied at this site; the declaration only names that witness as the canonical D4 input for the unconditional master route (and retains provenance against the older degenerate Fin 1 path).
why it matters
This is the D4 leg of the unconditional master assembly. rs_quantum_gravity_master_unconditional and endpointRoute_master_theorem_valid both pass it (with the other canonical witnesses) into MasterTheorem.RSQuantumGravityMaster. The non-circularity audit uses it three ways: all_witness_fields_hold discharges canonicalPageCurveDerivedWitness.page_curve_derived from the witness's own holds field; d4_page_field_is discloses that the field equals the capacity-transfer law conjoined with nontrivialPageCurveProp (not True); and master_theorem_non_circularity_certificate records that the D4 Page field is non-vacuous (strict rise to an interior peak).
In framework terms it closes the Page-curve input on the gravity master surface without assuming any master clause, addressing F3. It does not by itself finish every dynamical QES/replica comparison contemplated in the older Track 3.C note; it supplies the theorem-built nontrivial witness the unconditional route consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.