physicalReggeEHConcreteRefinementFamilyTargetCertProjectionCount
plain-language theorem explainer
Audit constant fixing the number of concrete refinement-family certificate projections at three: data, slice targets, and product target. Gravity workers cite it when locking the Session 551 audit surface for the physical Regge-to-EH residual track. The body is the literal natural number 3.
Claim. The Session 551 audit count of concrete refinement-family certificate projections (data, slice targets, and product target) equals $3$.
background
Track 1.B-PHY packages physical finite-probe Regge-to-Einstein-Hilbert residual theorems as a structural upgrade beyond the flat-substrate witness. Normalized full nonlinear Regge finite aggregates converge to the canonical finite EH/Dirichlet action once edge-stencil local correspondence holds; the same correspondence feeds the finite-to-continuum bridge under a Riemann-sum identification.
What remains for the unconditional manifold EH theorem is the manifold-integral remaining target: the canonical periodic finite EH/Dirichlet limit-weight integral target on a concrete periodic Freudenthal refinement family. The present constant is the audit tally of the three certificate projections that package that remaining concrete refinement-family surface: data, slice targets, and product target.
proof idea
Definitional abbreviation: the natural number is set equal to 3 by a one-line definitional assignment. No lemmas or tactics are involved.
why it matters
Pins the Session 551 audit surface so downstream equality can fire by reflexivity. The immediate consumer is the theorem asserting this count equals three, which the module presents as the one-statement interface for the concrete refinement-family target: once the canonical periodic tet/six-tet volume-quadrature product filter data is supplied, the full-Regge residual path can proceed. It does not close the manifold integral remaining target itself; it only freezes the projection cardinality that the residual packaging expects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.