physicalReggeEHConcreteRefinementFamilyOneStatementProjectionCount_eq_three
plain-language theorem explainer
The one-statement projection count for the concrete physical Regge-to-Einstein-Hilbert refinement family equals three by definition. Gravity-track auditors cite it when the slice target, product-filter target, and audit certificate are packaged as a single residual statement. The proof is pure reflexivity on a numeric definition.
Claim. The one-statement projection count attached to the concrete physical Regge/Einstein-Hilbert refinement family equals $3$.
background
Module Track 1.B-PHY packages physical finite-probe Regge-to-EH residual theorems as a named structural upgrade beyond the flat-substrate witness. Closed content: normalized full nonlinear Regge finite aggregates converge to the canonical finite EH/Dirichlet action with residual tending to zero once edge-stencil local correspondence holds; the same correspondence feeds the finite-to-continuum bridge under a Riemann-sum identification.
What remains open 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 nearby session note frames a varying-cardinality product-filter route: a staged cross-cardinality quadrature package plus a global residual envelope supplies product-filter data for arbitrary cardinality index, after which the concrete physical Regge/EH slice target, product target, and audit certificate follow. The projection count simply records that three-way packaging.
proof idea
One-line term proof by rfl. The left-hand side is a numeric definition (or abbrev) whose body is the literal natural number 3, so definitional equality discharges the claim with no lemmas and no rewriting.
why it matters
Inside the physical Regge-to-EH residual track, this pins the cardinality of the one-statement projection bundle used by the concrete refinement-family packaging. The three projections match the staged route's outputs: concrete slice target, product-filter target, and audit certificate. No downstream consumers are recorded yet; the declaration is bookkeeping that keeps residual-envelope and product-filter statements aligned on a fixed projection arity.
It does not touch forcing-chain landmarks (T5 J-uniqueness, T6 phi, T7 eight-tick, T8 D=3) or the RCL directly. Its role is local to Gravity Track 1.B-PHY structural hygiene: fixing the projection count so later residual and continuum-bridge statements can quote a stable arity rather than an ad-hoc tuple length. The open manifold-integral remaining target is untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.