PhysicalReggeEHContinuumNormalizationFromResidualTarget
plain-language theorem explainer
Continuum-normalization target for physical Regge-to-Einstein-Hilbert: if the finite product residual estimate holds on a global residual envelope, the product-indexed full-Regge aggregate converges to the continuum integral along the cross-cardinality product filter. Track 1.B-PHY gravity cites this as the raw Tendsto packaging after residual control plus staged quadrature. The body is a Prop definition (implication), not a proved theorem.
Claim. Fix cross-cardinality six-tet volume-quadrature data $D$ (with refinement filter and continuum integral) and a global residual envelope $E$ on $D$. The continuum-normalization-from-residual target asserts: if the finite product residual estimate holds for $E$, then the product-indexed full-Regge aggregate tends to $D$'s continuum integral along the product of the refinement filter with the within-slice filter.
background
Track 1.B-PHY upgrades the flat-substrate structural witness to physical finite-probe Regge-to-EH residual theorems from the six-tet cubic Dirichlet instance. Closed material includes normalized full nonlinear Regge finite aggregates converging to the canonical finite EH/Dirichlet action (residual to zero) once edge-stencil local correspondence holds, plus a finite-to-continuum bridge when a Riemann-sum identification is supplied.
The upstream global residual envelope packages three fields geometry must fill: an envelope on the within-slice refinement parameter, convergence of that envelope to zero, and a slice-uniform absolute residual bound. The product-indexed full-Regge aggregate evaluates, at a pair (cardinality slice, within-slice parameter), the full-Regge aggregate of that slice. Cross-cardinality data supply the refinement family, product filter, and named continuum integral target.
This definition is the Session 588 continuum-normalization target: the raw cross-cardinality Tendsto statement obtained after the finite product residual estimate is combined with the staged quadrature limit.
proof idea
Definitional packaging only. The Prop is the implication from the finite product residual estimate target on the envelope $E$ to a single Filter.Tendsto of the product-indexed full-Regge aggregate along the product filter (refinement filter $\times$ within-slice filter) into the neighborhood filter of $D$'s continuum integral. No tactics or lemmas are invoked in the body; the companion theorem physicalReggeEHContinuumNormalizationFromResidualTarget_holds is the place that discharges the implication.
why it matters
Sits in the Track 1.B-PHY residual structural upgrade that packages physical six-tet Regge-to-EH residual control beyond the flat structural witness. Downstream, the master-theorem handoff endpoint Track1ContinuumNormalizationFromResidualEndpoint is exactly the universal quantification of this target over all envelopes $E$, described as "the finite product residual estimate normalizes to the raw product-filter continuum Tendsto statement." The sibling holds theorem asserts the target for every such $E$.
In the broader Recognition gravity track this is the continuum-normalization step on the path from discrete Regge aggregates toward the Einstein-Hilbert continuum action. What remains for the unconditional manifold EH theorem is the manifold-integral remaining target (canonical periodic finite EH/Dirichlet limit-weight integral on a concrete periodic Freudenthal refinement family). Spatial dimension $D=3$ (T8) is ambient in the lattice and gap infrastructure this track imports, but is not re-proved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.