PhysicalReggeEHConcreteRefinementFamilySliceTarget
plain-language theorem explainer
Names the cross-cardinality Riemann-sum obligation for a varying six-tet Freudenthal refinement family: every slice must carry the concrete finite EH/Dirichlet limit-weight identification. Gravity Track 1.B-PHY and MasterTheorem handoff endpoints cite it as the slice-level half of the continuum bridge. The body is a one-line universal quantification over the family's slice map.
Claim. For a filter $l$ on an index type and a varying-cardinality family $F$ of canonical periodic six-tet volume-quadrature slices, the refinement-family slice target holds when, for every refinement parameter $r$, the slice $F(r)$ satisfies the concrete per-slice EH/Dirichlet limit-weight target (finite limiting aggregate identified with the slice's canonical quadrature integral via the $V_{\mathrm{cell}}/6$ split).
background
Track 1.B-PHY packages physical finite-probe Regge-to-EH residual theorems as a structural upgrade beyond the flat-substrate witness. What is already closed: normalized full nonlinear Regge finite aggregates converge to the canonical finite EH/Dirichlet action once edge-stencil local correspondence holds, and that correspondence feeds a finite-to-continuum bridge when a Riemann-sum identification is supplied.
A varying-cardinality refinement family is a collection of finite six-tet quadrature slices indexed by a refinement parameter type $\rho$, each slice a canonical periodic Freudenthal six-tet volume quadrature. The per-slice target asserts that the finite EH/Dirichlet limiting aggregate on that slice is identified with the slice's canonical quadrature integral, with probes and weights fixed by the periodic tetrahedra and the canonical cell-volume$/6$ split. That per-slice Prop is the slice-level instance of the remaining manifold-integral target on a concrete periodic Freudenthal family.
proof idea
Definitional abbreviation, not a proved theorem. The Prop is literally $\forall r : \rho$, the concrete per-slice limit-weight target holds on $F.\mathrm{slice}, r$. No tactics or lemmas fire at the definition site; the companion theorem physicalReggeEHConcreteRefinementFamilySliceTarget_holds discharges it by applying the per-slice holder to each slice.
why it matters
This is the slice-level half of the Agent-B continuum package for Track 1.B-PHY. Downstream, PhysicalReggeEHConcreteRefinementFamilyTargetCert stores it as the slice_targets field beside product-filter data; the MasterTheorem handoff endpoints (Track1ConcreteRiemannSumEndpoint, single-slice and varying-cardinality product-filter endpoints) all require it so that every slice carries the finite EH/Dirichlet limit-weight identification before product-filter full-Regge aggregates are compared to the family's continuum EH integral.
In the module's residual ledger it sits under the still-open manifold Einstein-Hilbert obligation: once cross-cardinality quadrature convergence and product-filter uniform residual control are supplied, this family-wide slice target plus the product-filter target yield the physical Regge/EH continuum statement along admissible diagonal schedules. It does not itself invoke the forcing chain (T5–T8) or the RCL; it is pure discrete-to-continuum bookkeeping on the six-tet Freudenthal lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.