canonicalPageCurveDerivedWitness_tickRoute
plain-language theorem explainer
Canonical audit alias for the page-curve input to the unconditional gravity master theorem, routed through the older recognition-tick dynamical construction. Gravity auditors cite it to confirm that the tick-based page-curve witness still typechecks as a derived page-curve certificate. The body is a one-line alias onto the dynamical recognition-tick witness.
Claim. There is a canonical derived page-curve witness for the gravity master theorem obtained by the recognition-tick dynamical route: it inhabits the master-theorem page-curve-derived type and equals the existing recognition-tick page-curve certificate from the dynamical page-curve development.
background
The module Gravity.MasterTheoremUnconditional closes the older conditional quantum-gravity master theorem by installing zero-argument, theorem-built witnesses for each of its five inputs. The conditional statement remains the audit surface; this file supplies the canonical routes through it.
One of those inputs is a derived page-curve certificate (the master-theorem page-curve-derived type). Dynamical page-curve work already produces such a certificate along a recognition-tick route: entropy and island bookkeeping organized by discrete recognition ticks rather than a continuum-only construction.
This declaration is the audit-facing name for that older tick route. The module doc retains parallel endpoint and physical routes elsewhere (for Regge/EH continuum and Bianchi clauses); here the point is simply that the recognition-tick page-curve witness remains valid and is still exposable as a canonical master-theorem input.
proof idea
One-line definitional wrapper. The body is exactly the existing dynamical recognition-tick page-curve derived witness; no new tactics, lemmas, or algebraic work occur at this site. Type equality is by construction of that upstream witness inhabiting the master-theorem page-curve-derived type.
why it matters
In the Recognition gravity stack, the master theorem packages structural inputs (continuum Regge/EH limits, Bianchi identities, amplitude linearity, page-curve derived data, and related PTA/signal models) into an unconditional closure surface. Keeping the recognition-tick page-curve route as a named canonical witness preserves audit continuity with the dynamical page-curve development and with discrete recognition timing (eight-tick octave structure in the broader forcing chain).
Sibling canonical page-curve and PTA witnesses in the same module form the parallel zero-argument package. This particular name exists so reviewers can still discharge the page-curve slot via the older tick construction without forcing a single preferred dynamical model. No new physics claim is added beyond re-exporting that certificate under the unconditional master-theorem namespace.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.