physicalReggeEHContinuumNormalizationFromResidualProjectionCount_eq_two
plain-language theorem explainer
In the physical Regge-to-Einstein-Hilbert residual package, the continuum normalization constant read off from the residual projection count equals 2. Gravity workers citing Track 1.B-PHY continuum weights or finite-probe residual upgrades use this fixed factor. The proof is pure definitional reflexivity: the constant is declared as 2.
Claim. The continuum normalization factor extracted from the residual projection count in the physical Regge–Einstein–Hilbert residual track equals $2$.
background
Track 1.B-PHY packages physical finite-probe Regge-to-EH residual theorems as a structural upgrade beyond the flat-substrate witness. The module closes normalized full nonlinear Regge finite aggregates converging to the canonical finite EH/Dirichlet action (residual to zero) once edge-stencil local correspondence holds, and feeds the finite-to-continuum bridge when a Riemann-sum identification is supplied.
What remains open for the unconditional manifold Einstein-Hilbert theorem is the manifold-integral remaining target: the canonical periodic finite EH/Dirichlet limit-weight integral on a concrete periodic Freudenthal refinement family. The continuum normalization constant named here is the scalar that rescales residual projection counts into that continuum weight bookkeeping; siblings treat finite-probe residual conclusions, Bianchi interfaces, and concrete slice-limit weight targets.
proof idea
One-line term proof by rfl. The named continuum-normalization constant is definitionally equal to the numeral 2, so no lemmas, rewrites, or arithmetic are required.
why it matters
Pins the continuum weight scale used throughout the physical residual upgrade: residual projection counts are normalized by the factor 2 when matching full nonlinear Regge aggregates to continuum EH/Dirichlet integrals. That scale sits beside the finite-probe residual conclusion, the Bianchi interface under local correspondence, and the concrete slice-limit weight target in the same Track 1.B-PHY module.
It does not itself close the manifold integral remaining target; it only fixes the bookkeeping constant those residual and continuum statements share. In the broader RS gravity track this is structural plumbing for the Regge→EH continuum limit, not a forcing-chain (T0–T8) step. No downstream consumers are recorded yet; the declaration is a named equality witness for the residual-projection normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.