endpointRouteRegEHContinuumProp
plain-language theorem explainer
Packages three Track-1 endpoint receipts (single-slice product-filter data, varying-cardinality product-filter data, and the physical D2 master-witness endpoint) into one proposition for the Regge-to-Einstein-Hilbert continuum clause. Gravity auditors cite it when reconstructing the older endpoint-receipt D2 route into the unconditional master theorem. The body is a pure conjunction of those three Props; no new mathematics is proved here.
Claim. The endpoint-route Regge/Einstein-Hilbert continuum proposition is the conjunction of three claims: (1) every concrete six-tet quadrature slice on a filter supplies single-slice product-filter refinement data meeting the physical Regge/EH slice target; (2) staged cross-cardinality data plus a global residual envelope supply genuine varying-cardinality product-filter data meeting that target; (3) for any such product-filter refinement data and any finite bond type, a nonempty physical Regge/EH D2 master-witness certificate exists (so the master theorem's D2 input may use the physical $\mathrm{Tendsto}$ continuum target).
background
The module Gravity.MasterTheoremUnconditional installs zero-argument, theorem-built witnesses for the five inputs that the older conditional quantum-gravity master theorem took as hypotheses. The conditional theorem stays the audit surface; this file supplies the canonical route through it.
For the D2 (Regge continuum plus discrete Bianchi) input, an earlier construction routed the continuum clause through three endpoint-receipt propositions from Track 1 handoff integration. Those receipts are: every six-tet quadrature slice yields single-slice product-filter data (closing the unit-cardinality case); cross-cardinality data with a global residual envelope yield genuine varying-cardinality product-filter data (the manifold-scale route); and, given such data, a physical Regge/EH D2 master-witness certificate is nonempty, so the continuum target is the physical $\mathrm{Tendsto}$ to the Einstein-Hilbert integral rather than a flat-substrate identity.
The module now prefers a primary D2 witness that names the physical Regge/EH and Bianchi content directly. The present definition retains the older three-endpoint packaging as an explicit audit route.
proof idea
Definition only: the proposition is the three-way conjunction of the single-slice product-filter endpoint, the varying-cardinality product-filter endpoint, and the physical D2 master-witness endpoint (all imported from the Track-1 handoff integration module). No tactics or lemmas are applied at this site; inhabitation is deferred to the companion theorem that pairs the three corresponding endpoint-holds results.
why it matters
This is the continuum half of the retained endpoint-receipt D2 witness. Downstream, canonicalRegEHContinuumAndBianchiWitness_endpointRoute installs it as the regge_to_einstein_hilbert_continuum field of a RegEHContinuumAndBianchi structure (paired with the concrete physical Bianchi proposition), and endpointRouteRegEHContinuumProp_holds discharges the package by quoting the three Track-1 endpoint theorems.
In the Recognition gravity stack this sits on the path that turns discrete Regge calculus on the canonical periodic six-tet cubic torus into continuum Einstein-Hilbert behavior under product-filter refinement, which is one of the five inputs needed to close the unconditional master theorem. The module doc marks the primary physical-content route as preferred; this definition exists so auditors can still replay the Session-566 endpoint-receipt construction without touching the preferred witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.