canonicalPageCurveDerivedWitness_operatorRoute
plain-language theorem explainer
Canonical audit alias that packages the operator-route Page-curve witness as a zero-argument MasterTheorem.PageCurveDerived value. Gravity auditors cite it when checking that the Schmidt-saturated operator derivation still discharges the Track 3.C slot on the unconditional master-theorem surface. The body is a one-line alias of the operator entropy witness.
Claim. Define the canonical operator-route witness of type "Page curve derived" to be the operator-derived Schmidt-saturated witness: its proposition is the conjunction of the recognition-tick capacity transfer law and the operator-derived Page-curve proposition, and both conjuncts hold.
background
The unconditional master-theorem module supplies zero-argument witnesses for the five inputs that the older conditional RS quantum-gravity master theorem took as hypotheses. One of those slots is Track 3.C: a dynamical Page-curve derivation packaged as a Lean structure with a proposition field and a proof that the proposition holds.
Upstream, the operator entropy module builds that structure by routing through a Schmidt-saturated operator process rather than a readout-equals-page-curve field. Its proposition is the conjunction of a recognition-tick capacity transfer law (tied to the fundamental RS time quantum $\tau_0 = 1$ tick) and an operator-derived Page-curve statement; both halves are already proved there.
The present definition is the audit-facing name for that same operator witness on the unconditional closure surface. A sibling canonical witness exists for the older recognition-tick route; this operator route is retained for provenance, including a degenerate $\mathrm{Fin},1$ path.
proof idea
One-line definitional alias. The body is exactly operatorPageCurveDerivedWitness from the Page-curve operator-entropy module, which already constructs a PageCurveDerived record whose page_curve_derived field is the conjunction of the recognition-tick capacity transfer proposition and the operator-derived Page-curve proposition, with holds pairing the two corresponding proofs.
why it matters
On the unconditional master-theorem closure surface this name freezes the operator-derived Schmidt-saturated discharge of Track 3.C so auditors can still point at it after the primary canonical Page-curve witness may have moved. The parent structure is the MasterTheorem Page-curve hypothesis: dynamical entropy evolution for a unitary joint matter-radiation system, with Page time $M^3$ scaling already closed and the full replica-wormhole / quantum-extremal-surface comparison still heavy multi-session work. Retaining the operator route documents that the Schmidt-saturated derivation remains a valid zero-argument input even when the mainline witness prefers another path. No downstream consumers are wired yet; the declaration is provenance and audit surface, not a new physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.