physicalReggeEHContinuumNormalizationFromResidualProjectionCount
plain-language theorem explainer
Names the continuum normalization factor extracted from residual projection counting in the physical Regge-to-Einstein-Hilbert upgrade; the value is the natural number 2. Gravity workers citing Track 1.B-PHY residual theorems use it as the fixed scale that converts finite-probe residuals into continuum-normalized EH/Dirichlet aggregates. The definition is a literal constant assignment.
Claim. The continuum normalization constant obtained from residual projection counting in the physical Regge-to-Einstein-Hilbert residual package is the natural number $2$.
background
Track 1.B-PHY packages physical finite-probe Regge-to-EH residual theorems beyond the flat-substrate structural witness. Once edge-stencil local correspondence holds, normalized full nonlinear Regge finite aggregates converge to the canonical finite EH/Dirichlet action, with an explicit residual tending to zero; the same correspondence feeds a 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: a canonical periodic finite EH/Dirichlet limit-weight integral on a concrete periodic Freudenthal refinement family. In that residual bookkeeping, a discrete projection count supplies a continuum normalization scale; this definition records that scale as a named natural number.
proof idea
Pure definitional assignment: the constant is set equal to the natural number 2. No lemmas or tactics are involved. The companion equality theorem is reflexivity on that definition.
why it matters
Gives a stable named handle for the continuum normalization factor used when residual projection counts are turned into continuum-normalized Regge/EH statements in Track 1.B-PHY. The immediate consumer is the reflexivity theorem that records the equality to 2, which sits next to the physical D2 master-hypothesis witness replacing the flat structural $0=0$ clause. The module status is structural theorem (zero sorry, no new RS-specific axiom); this constant is part of the audit surface (Session 588: one normalization function and one applied continuum theorem). It does not itself close the manifold-integral remaining target on a Freudenthal refinement family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.