physicalReggeEHContinuumNormalizationFromResidualTarget_apply
plain-language theorem explainer
Once a global residual envelope is fixed for a canonical periodic tet/six-tet volume quadrature family, the full product Regge aggregate converges in the product refinement filter to the continuum integral. Gravity workers citing the Track 1.B-PHY Regge-to-EH continuum bridge use this applied form. The proof is a two-line term application of the residual-target continuum theorem fed by the finite-product residual estimate.
Claim. Let $D$ package a canonical periodic tetrahedral/six-tet volume-quadrature family with cross-cardinality data over parameter type $\alpha$ and refinement type $\rho$, with filter $\ell$ on $\alpha$. Given a global residual envelope $E$ for $D$, the full product Regge aggregate of the family tends, along the product filter $D.\mathrm{refinementFilter}\times\ell$, to the neighborhood filter of the continuum integral $D.\mathrm{continuumIntegral}$.
background
Track 1.B-PHY packages physical finite-probe Regge-to-Einstein-Hilbert residual theorems as a structural upgrade beyond the flat-substrate witness. What is closed: normalized full nonlinear Regge finite aggregates converge to the canonical finite EH/Dirichlet action with an explicit residual tending to zero once edge-stencil local correspondence holds; the same local correspondence feeds the finite-to-continuum bridge when a Riemann-sum identification is supplied.
The data $D$ is a cross-cardinality package for a canonical periodic tet/six-tet volume quadrature family: it carries the refinement family, the refinement filter, and a named continuum integral target. The envelope $E$ is the global residual envelope over that package, bundling the finite-product residual control needed to pass from discrete aggregates to the continuum limit.
Still open for the unconditional manifold EH theorem is the remaining manifold-integral target: a concrete periodic Freudenthal refinement family must satisfy the canonical periodic finite EH/Dirichlet limit-weight integral identification.
proof idea
Term-mode one-shot application. The continuum-normalization-from-residual-target theorem is applied to the envelope $E$, with its residual hypothesis discharged by the finite-product residual estimate theorem specialized to the same $E$. No further filter or topology work is done here; both named lemmas already encode the Tendsto statement and the residual bound.
why it matters
This is the Session 588 projection that turns the residual-target interface into an applied continuum normalization theorem: finite residual control implies the full Regge aggregate converges to the continuum integral. It sits in the Track 1.B-PHY structural layer that upgrades the flat-substrate witness to physical six-tet cubic Dirichlet instances.
Downstream the module still points at the remaining manifold-integral target (canonical periodic finite EH/Dirichlet limit-weight integral on a concrete Freudenthal refinement family). No used-by edges are recorded yet; the declaration is the applied form of the continuum bridge rather than a leaf of a larger proved chain.
Framework context: the ambient geometry is three-dimensional (T8 forces $D=3$), and the discrete side is built from periodic tet/six-tet stencils compatible with the eight-tick octave structure. The result is pure analysis of Regge aggregates; it does not itself derive $G$ or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.