PhysicalReggeEHManifoldIntegralRemainingTarget
plain-language theorem explainer
Names the remaining manifold-level Track 1.B-PHY obligation after local correspondence: on a periodic Freudenthal lattice (sizes at least 3), every finite vertex-potential probe, limit-weight vector, and supplied continuum EH value must satisfy Riemann-sum identification of the limiting finite EH/Dirichlet aggregate with that continuum integral. Residual and Bianchi-interface proofs cite it as the residual upgrade hypothesis. Definitional packaging of the upstream finite-to-integral target.
Claim. For integers $N_x,N_y,N_z\ge 3$, the remaining manifold integral target is the proposition that for every finite family of vertex conformal potentials on the canonical periodic Freudenthal triangulation of the $N_x\times N_y\times N_z$ torus, every real weight vector on that family, and every supplied continuum Einstein-Hilbert integral $I\in\mathbb{R}$, the limiting finite EH/Dirichlet weighted aggregate equals $I$ (Riemann-sum identification).
background
Track 1.B-PHY upgrades the flat-substrate Regge-to-Einstein-Hilbert residual of the structural track to the physical six-tet cubic Dirichlet instance on a periodic Freudenthal torus. The module closes normalized full nonlinear Regge finite aggregates converging to the canonical finite EH/Dirichlet action once edge-stencil local correspondence holds, and packages the finite-to-continuum bridge when a Riemann-sum identification is supplied.
Vertex conformal potentials are real assignments to the vertices of a finite 3D triangulation. The continuum integral here is intentionally just a real number: analytic content lives in the hypothesis that identifies refinement-indexed finite EH/Dirichlet aggregates with that value. The upstream finite-integral target states that after mesh weights converge, equality of the limiting finite aggregate with the supplied continuum value is enough to feed the finite-to-integral bridge.
This definition simply names that upstream target, universally quantified over probes, weights, and continuum values, on the canonical encoded periodic Freudenthal torus of given lattice sizes.
proof idea
Definitional, not a proved theorem. The body is the universal quantification, over finite probe families of vertex potentials on the canonical periodic Freudenthal torus, limit-weight vectors, and continuum EH integral values, of the upstream CanonicalPeriodicFiniteEHDirichletLimitWeightIntegralTarget. No tactics or lemmas; pure Prop alias for the remaining Riemann-sum obligation.
why it matters
Marks the exact gap between the structural Track 1.B residual (local correspondence plus finite-probe convergence) and an unconditional manifold Einstein-Hilbert theorem on the periodic Freudenthal family. Downstream, the physical upgrade reduction theorem states that beyond the flat witness the upgrade splits into local correspondence and this single Riemann-sum target. The Bianchi interface structure keeps this manifold integral target outside the packaged finite-probe residual plus contracted discrete Bianchi theorem; the corresponding constructor from local correspondence explicitly leaves this obligation as the remaining physical manifold upgrade. Concrete refinement-family slice targets and their holding theorems sit in the same residual module and eventually discharge instances of this Prop on six-tet volume quadrature families. In the broader RS gravity program this is the last named structural input before continuum EH on the discrete torus substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.