concretePhysicalRegEHContinuumProp
plain-language theorem explainer
Names the physical D2 Regge-to-Einstein-Hilbert claim: for every product-filter refinement package on the canonical periodic six-tet cubic torus, the normalized full nonlinear Regge aggregate tends to the supplied continuum EH/Dirichlet integral. Gravity auditors cite it as the concrete content of the master theorem Regge/EH clause. The body is a pure universal quantification over refinement data wrapping the product-filter target predicate; no proof work lives here.
Claim. For every index type $\alpha$, residual type $\rho$, filter $\ell$ on $\alpha$, and every product-filter refinement data package $D$ for the canonical periodic six-tet volume quadrature on the cubic torus, the full nonlinear Regge aggregate associated to $D$ converges along the product filter to the continuum Einstein-Hilbert/Dirichlet integral supplied by $D$.
background
The module closes the older conditional quantum-gravity master theorem by installing zero-argument witnesses for its five inputs. The D2 slot is continuum Regge-to-Einstein-Hilbert convergence plus a contracted discrete Bianchi identity; this definition is the Regge/EH half of that primary physical route (the endpoint-receipt route is retained only for audit).
The data package CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData bundles a six-tet volume-quadrature refinement family on the periodic cubic torus, a residual filter, a continuum integral value, and the quadrature limit. Unlike staged cross-cardinality packages, it carries a uniform product residual so one global limit is available.
The target predicate is the product-filter full-Regge-to-EH statement: after the family supplies cross-cardinality quadrature convergence and a uniform residual, the normalized nonlinear Regge aggregate tends to that continuum integral. Spatial dimension $D=3$ is the T8-forced value used throughout the gravity stack.
proof idea
Definition only, not a proved theorem. The body is a single universal quantifier: for arbitrary types $\alpha,\rho$, filter $\ell$, and any product-filter six-tet data package $D$, assert the concrete product-filter Regge-to-EH target on $D$. That target is itself a Filter.Tendsto of the full nonlinear Regge aggregate to $D$'s continuum integral. No tactics, no lemmas applied at this site; the actual convergence proof is discharged later by the companion _holds theorem via the Track-1 residual lemma.
why it matters
This is the named physical content of the master theorem's D2 Regge/EH field. The primary witness canonicalRegEHContinuumAndBianchiWitness plugs it directly into regge_to_einstein_hilbert_continuum (no endpoint-receipt indirection). The companion theorem concretePhysicalRegEHContinuumProp_holds proves the proposition by applying the Track-1 product-filter residual result. Non-circularity audit records the equality of the witness field with this definition, confirming the D2 slot is a genuine $\forall$-over-refinement-data claim rather than a tautology or the master conclusion itself. In the RS gravity program it is the continuum-limit half of the unconditional D2 closure surface that lets the older conditional master theorem run with zero free hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.