concretePhysicalRegEHContinuumProp_holds
plain-language theorem explainer
In any spatial dimension, the physical Regge-to-Einstein-Hilbert continuum clause holds: on the canonical periodic six-tet cubic torus, every product-filter refinement sends the normalized full nonlinear Regge aggregate to the supplied continuum EH integral. Gravity auditors cite it as the zero-argument physical half of the D2 master-theorem witness. The proof is a one-line term that reexports the Track-1 physical residual product-filter target theorem.
Claim. The physical Regge/EH continuum proposition holds: for every spatial dimension $D$, and for any product-filter refinement data on the canonical periodic six-tetrahedra cubic torus, the normalized full nonlinear Regge aggregate converges to the supplied continuum Einstein-Hilbert integral along that product filter.
background
This module closes the five inputs of the older conditional quantum-gravity master theorem by installing theorem-built, zero-argument witnesses. The D2 slot is the Regge-to-continuum plus discrete Bianchi package. The primary route names physical content directly rather than endpoint receipts from the handoff integration layer.
The Regge/EH half asserts continuum recovery of the Einstein-Hilbert action from a discrete Regge calculus on a fixed combinatorial background: the canonical periodic six-tet cubic torus. Refinement is controlled by a product filter; the claim is that the normalized full nonlinear Regge aggregate converges to a supplied continuum EH integral on that filter.
Spatial dimension $D=3$ is forced upstream (T8/T9 in the forcing chain), but the proposition is stated for arbitrary $D$ and discharged uniformly. The companion Bianchi half (Schläfli-satisfying data obey the contracted discrete Bianchi identity at every vertex) is packaged beside this result in the same witness record.
proof idea
One-line term proof. The goal is the proposition concretePhysicalRegEHContinuumProp, which is a $\Pi$-type over dimension $D$. The body is the lambda fun D => ... that applies Track1BCPhysicalResidual.physicalReggeEHConcreteProductFilterTarget_holds at that $D$. No local rewriting, cases, or calculus; it is a pure reexport of the Track-1 physical residual product-filter convergence theorem into the master-theorem proposition shape.
why it matters
This is the proved half that fills regge_holds inside canonicalRegEHContinuumAndBianchiWitness, the primary D2 witness for the unconditional master theorem. Downstream doc-comment: the Regge/EH clause "carries the physical product-filter convergence theorem" with "no endpoint receipt indirection."
Together with the Bianchi holds lemma, it lets the older rs_quantum_gravity_master_conditional audit surface be invoked along a canonical zero-argument route. An alternate endpoint-receipt route is retained only for audit. In the broader RS gravity stack this is the discrete-to-continuum bridge that justifies treating Regge data as a controlled approximation to continuum EH gravity inside the master theorem, sitting beside page-curve and strong-field structural inputs rather than replacing them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.