physicalReggeEHConcreteSingleSliceProductFilterOneStatementProjectionCount
plain-language theorem explainer
Audit counter that fixes at two the number of single-slice product-filter one-statement projections (slice target and product target) in the Track 1.B-PHY physical Regge-to-EH residual package. Session 556 bookkeeping only; anyone checking the concrete residual upgrade inventory would cite it. Defined by literal assignment to the natural number 2.
Claim. The Session 556 audit count of single-slice product-filter one-statement projections equals $2$, namely the slice target and the product target.
background
The ambient module packages physical finite-probe Regge-to-Einstein-Hilbert residual theorems as a named Track 1.B-PHY structural upgrade beyond the flat-substrate witness. Status is a structural theorem block (zero sorry, no new RS-specific axioms). What is already closed: normalized full nonlinear Regge finite aggregates converge to the canonical finite EH/Dirichlet action, with an explicit residual tending to zero, once edge-stencil local correspondence holds; the same correspondence 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 (canonical periodic finite EH/Dirichlet limit-weight integral target on a concrete periodic Freudenthal refinement family). The present declaration is pure inventory metadata inside that residual track: it records how many one-statement projections sit under the concrete single-slice product-filter filter.
proof idea
One-line definitional assignment of the natural number literal 2. No lemmas, no tactics, no proof obligations.
why it matters
Exists solely as Session 556 audit bookkeeping for the two named one-statement projections (slice target and product target) inside the concrete single-slice product-filter layer of the physical residual upgrade. Its only downstream consumer is the trivial equality theorem that reconfirms the count equals 2 by rfl. It does not advance the forcing chain, the RCL, or the remaining manifold-integral target; it only keeps the residual-track inventory honest while the structural upgrade beyond the flat witness is audited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.