PhysicalReggeEHConcreteDiagonalTarget
plain-language theorem explainer
Names the diagonal convergence target for full nonlinear Regge aggregates on a six-tet periodic family: along a schedule into the product of within-slice refinement and cardinality filters, the normalized aggregate tends to the continuum Einstein–Hilbert integral. Gravity workers citing Track 1.B-PHY residual upgrades use it as the concrete Prop discharged by the companion holds theorem. The body is a pure Prop abbreviation of a single Filter.Tendsto statement.
Claim. Given product-filter data $D$ for a canonical periodic six-tet volume-quadrature refinement family (with continuum EH integral $I_\infty$) and a diagonal schedule $\gamma:\delta\to\rho\times\alpha$, the predicate asserts $\mathrm{Tendsto}_{s\to m}\,\mathrm{FullReggeAgg}_D(\gamma(s))=I_\infty$ in the usual neighborhood filter on $\mathbb{R}$.
background
Track 1.B-PHY packages physical finite-probe Regge-to-EH residual theorems beyond the flat-substrate witness of Track 1.B-C structural. The closed content is that normalized full nonlinear Regge finite aggregates converge to the canonical finite EH/Dirichlet action (residual to zero) once edge-stencil local correspondence holds, and that the same correspondence feeds a finite-to-continuum bridge under a Riemann-sum identification.
The product-filter data package bundles a refinement family, a within-slice refinement filter, a continuum integral, and a uniform product residual so one global limit is available (unlike staged cross-cardinality packages). The full-Regge aggregate is product-indexed: the first coordinate selects the finite cardinality slice, the second is the within-slice refinement parameter.
The remaining open piece for an unconditional manifold Einstein–Hilbert theorem is the manifold-integral remaining target: the canonical periodic finite EH/Dirichlet limit-weight integral target on a concrete periodic Freudenthal refinement family.
proof idea
Definitional Prop, not a proved theorem. It expands to a single Filter.Tendsto of the product-indexed full-Regge aggregate composed with the supplied diagonal map, with codomain neighborhood filter of D.continuumIntegral. No tactics or lemmas are applied at this site; the companion theorem physicalReggeEHConcreteDiagonalTarget_holds discharges the Prop by feeding a tendsto hypothesis of the diagonal into the product filter (D.refinementFilter ×ˢ l).
why it matters
Gives the named diagonal form of the concrete product-filter full-Regge-to-EH target inside Track 1.B-PHY. Downstream, physicalReggeEHConcreteDiagonalTarget_holds states that any diagonal tending into the product filter proves this target, converting a schedule hypothesis into continuum convergence of the normalized full-Regge aggregate.
In the broader residual upgrade, this sits between finite-probe residual conclusions (local correspondence implies residual to zero against the finite EH/Dirichlet action) and the still-open manifold integral remaining target. It does not itself invoke the forcing chain landmarks (T5–T8, RCL, $\varphi$), but it is part of the gravity track that aims to recover continuum EH from discrete Regge data on the RS-native six-tet cubic Dirichlet instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.