physicalReggeEHUpgrade_beyond_flatStructuralWitness
plain-language theorem explainer
Under edge-stencil local correspondence on a periodic Freudenthal torus, the continuum Regge–EH structural property holds and weighted normalized finite Regge aggregates converge to the canonical finite EH/Dirichlet limit action (residual → 0). Gravity workers on the discrete-to-continuum Einstein–Hilbert bridge cite this as the physical Track 1.B upgrade past the flat zero identity. The proof is a two-component term pairing the structural witness with the finite-probe residual theorem.
Claim. Fix lattice sizes $N_x,N_y,N_z>2$ and assume canonical periodic edge-stencil local correspondence. Then the continuum Regge–EH structural property holds, and there exist $r>0$ and $C\ge 0$ such that: for any finite family of vertex potentials on the canonical encoded periodic Freudenthal torus, any weights along a filter $\ell$ tending to limit weights, and any mesh spacing tending to $0$ (eventually nonzero), the difference between the weighted sum of normalized Regge actions (Regge action of spacing-scaled probes, divided by $\|\mathrm{spacing}\|^2$) and the weighted sum of canonical finite EH/Dirichlet limit actions tends to $0$ along $\ell$.
background
Track 1.B-PHY packages physical finite-probe Regge-to-Einstein–Hilbert residual theorems as a named upgrade beyond the flat-substrate witness in the structural Track 1.B module. Status is a structural theorem: zero sorry and no new RS-specific axioms.
The geometry is the canonical encoded periodic Freudenthal torus on an $N_x\times N_y\times N_z$ lattice (each side $>2$). Vertex potentials live on that triangulation. The concrete 3D Regge action under the vertex-conformal ansatz is the sum over edges of hinge measure times deficit angle. The continuum side uses the canonical finite EH/Dirichlet limit action on the same probes.
The decisive hypothesis is canonical periodic edge-stencil local correspondence: it is what turns the flat zero–zero identity into a genuine residual that vanishes as mesh spacing tends to zero. The module also notes that the same correspondence feeds a finite-to-continuum bridge once a Riemann-sum identification is supplied.
proof idea
Term-mode proof by pairing. The first conjunct is discharged by the structural continuum witness regge_eh_continuum_canonical_witness from the flat Track 1.B structural module. The second conjunct is exactly the finite-probe residual theorem physicalReggeEHFiniteProbeResidualTarget applied to the given lattice sizes and the local-correspondence hypothesis. No further tactic work: the upgrade is the named conjunction of those two results.
why it matters
This declaration is the named physical upgrade that replaces the flat zero–zero identity of regge_eh_continuum_canonical_witness with a genuine finite-probe residual under local correspondence. It closes the Track 1.B-PHY claim that normalized full nonlinear Regge finite aggregates converge to the canonical finite EH/Dirichlet action with residual tending to zero once edge-stencil local correspondence holds.
What remains open for the unconditional manifold Einstein–Hilbert theorem is PhysicalReggeEHManifoldIntegralRemainingTarget: the canonical periodic finite EH/Dirichlet limit-weight integral target on a concrete periodic Freudenthal refinement family. Sibling interfaces (Bianchi, slice-limit weights, refinement families) sit next to this upgrade; none are discharged here. In the broader RS gravity track this is structural scaffolding toward continuum EH, not yet a derivation of $G$ or the $\varphi$-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.