physicalReggeEHConcreteRefinementFamilyTargetCertProjectionCount_eq_three
plain-language theorem explainer
The concrete refinement-family target certificate for physical Regge→EH carries projection count exactly 3. Track 1.B-PHY residual bookkeeping cites this as the fixed size of the cert projection. The equality is definitional: the count is literally the numeral 3, discharged by rfl.
Claim. The projection count attached to the concrete refinement-family target certificate in the physical Regge-to-Einstein-Hilbert residual package equals $3$.
background
Track 1.B-PHY packages physical finite-probe Regge-to-EH residual theorems beyond the flat-substrate witness of Track 1.B-C structural work. Once edge-stencil local correspondence holds, normalized full nonlinear Regge finite aggregates converge to the canonical finite EH/Dirichlet action with residual tending to zero; the same correspondence feeds a finite-to-continuum bridge when a Riemann-sum identification is supplied.
What remains for an unconditional manifold Einstein-Hilbert theorem is the manifold-integral remaining target: a canonical periodic finite EH/Dirichlet limit-weight integral target on a concrete periodic Freudenthal refinement family. The nearby one-statement interface exposes exactly that residual path: supply the canonical periodic six-tet volume-quadrature product-filter data; full-Regge product-filter continuum limit and per-slice finite EH/Dirichlet limit-weight targets then follow.
The projection count is a small numeric invariant of that concrete refinement-family target certificate, used as a fixed checklist size rather than a derived geometric quantity.
proof idea
Pure definitional equality. The left-hand side is a constant definition that unfolds to the numeral 3; the proof is the single term rfl. No lemmas, no rewriting beyond reducible unfolding.
why it matters
Pins a trivial but named numeric gate in the Track 1.B-PHY residual upgrade: the concrete refinement-family target cert is declared to project in exactly three slots. Downstream residual packaging (finite-probe residual conclusions, Bianchi interface, slice limit-weight targets, and the manifold-integral remaining target) can treat that arity as closed rather than open-ended.
It does not advance the continuum Einstein-Hilbert identification itself. The module still flags the open structural obligation: provide canonical periodic six-tet volume-quadrature product-filter data so the full-Regge product-filter continuum limit and per-slice finite EH/Dirichlet limit-weight targets follow. No used-by edges are recorded yet; the theorem is local bookkeeping inside the physical residual module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.