canonicalRegEHContinuumAndBianchiWitness_endpointRoute
plain-language theorem explainer
Packages the endpoint-receipt D2 witness for classical recovery: Track 1 handoff endpoints for Regge-to-Einstein-Hilbert continuum convergence, plus the contracted discrete Bianchi identity on Schläfli-satisfying data. Gravity auditors cite it when checking the audit route through the unconditional master theorem rather than the primary physical residual route. It is a structure instance wiring four already-proved propositions into the Regge/EH-plus-Bianchi bundle.
Claim. The endpoint-route D2 witness is the structure whose continuum clause is the conjunction of the single-slice, varying-cardinality, and physical-D2 Track 1 product-filter endpoints; whose continuum certificate is the corresponding triple of endpoint theorems; whose Bianchi clause asserts that for any vertex and bond types every Schläfli-satisfying Regge datum obeys the contracted discrete Bianchi identity at every vertex; and whose Bianchi certificate is the corresponding master residual theorem.
background
The module closes the five inputs of the older conditional quantum-gravity master theorem by installing zero-argument, theorem-built witnesses. D2 is the classical-recovery load: discrete Regge calculus must recover the Einstein-Hilbert continuum action, and the discrete geometry must obey a contracted Bianchi identity.
The structure being inhabited packages two propositions with their proofs: a Regge-to-EH continuum statement (with an explicit residual bound in the abstract interface) and a discrete contracted Bianchi statement. The primary D2 witness in this file names physical residual content directly (product-filter refinement on the canonical periodic six-tet cubic torus, plus universal Schläfli Bianchi). The declaration here is the retained audit route that instead packages three proved Track 1 handoff endpoints: single-slice product-filter data, varying-cardinality product-filter data, and the physical-D2 master-witness endpoint.
Upstream, the continuum clause is the conjunction of those three endpoint propositions, proved by the corresponding handoff theorems. The Bianchi clause is the universal quantification over vertex and bond types of the physical Schläfli Bianchi master proposition, discharged by its residual theorem.
proof idea
Definitional structure instance, not a tactic proof. The four fields of the Regge/EH-plus-Bianchi bundle are filled by direct assignment: continuum proposition to the endpoint-route conjunction of the three Track 1 handoff endpoints; continuum certificate to the triple of handoff endpoint theorems; Bianchi proposition to the concrete physical Schläfli Bianchi master proposition; Bianchi certificate to that proposition's residual theorem. No new geometric estimate is proved here; the def only bundles already-closed receipts.
why it matters
Supplies the audit-route D2 input to the unconditional master theorem. Downstream, the theorem that both D2 routes produce valid master outputs applies this witness together with the amplitude-linear, page-curve, and PTA witnesses, documenting that the Track 1 integration path is not dead code.
In the Recognition gravity stack this is classical recovery on the discrete side of the continuum limit: Regge action to Einstein-Hilbert, plus discrete Bianchi so the continuum limit can carry diffeomorphism consistency. It does not itself force $D=3$ or the eight-tick octave (those sit earlier in the forcing chain); it closes the D2 slot the master theorem consumes when assembling the RS quantum-gravity master statement.
The module prefers the physical residual D2 witness for primary citation; this endpoint bundle remains so auditors can replay the Session 566 handoff path without reopening geometric residuals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.