Track1ConcreteRiemannSumEndpoint
plain-language theorem explainer
Agent B's Track-1 concrete Riemann-sum endpoint is the Prop that any six-tet product-filter refinement family yields slicewise finite Einstein-Hilbert/Dirichlet limit weights and a product-filter Regge aggregate converging to the family's continuum EH integral. Gravity handoff and master-theorem integration authors cite it as the receipt for the physical residual lane. It is a pure Prop definition packaging three conjuncts; the companion theorem discharges it.
Claim. For all types $\alpha,\rho$, every filter $\ell$ on $\alpha$, and every product-filter data package $D$ for a canonical periodic six-tetrahedron volume-quadrature refinement family along $\ell$: every refinement slice meets the concrete finite Einstein-Hilbert/Dirichlet limit-weight target; the product-filter full-Regge aggregate converges to $D$'s continuum EH integral; and a nonempty certificate of that refinement-family target exists.
background
Track 7 (this module) is the integration-lane receipt for parallel fork handoffs A-F in the gravity master plan. It records what each new endpoint proves without upgrading the unconditional discovery claim. Fork B supplies the physical residual and Bianchi interface that this endpoint packages.
The data package is the product-filter form of the six-tet volume-quadrature limit: a refinement family, a refinement filter on the secondary index, a continuum EH integral, and a uniform product residual that yields one global limit (unlike staged cross-cardinality packages). Upstream, spatial dimension is fixed at $D=3$ by the forcing chain (T8/T9).
The three conjuncts name the concrete finite EH/Dirichlet limit-weight target on each slice, the product-filter full-Regge aggregate target on the whole package, and nonemptiness of the corresponding refinement-family certificate.
proof idea
Pure Prop definition, no tactics. It universally quantifies over filter carrier types $\alpha,\rho$, a filter $\ell$, and a product-filter six-tet volume-quadrature data package $D$, then conjoins three propositions on $D$: the slicewise concrete EH/Dirichlet limit-weight target for $D$'s refinement family; the product-filter full-Regge convergence target for $D$; and nonemptiness of the refinement-family target certificate at $(\alpha,\rho,\ell)$. The companion theorem track1_concrete_riemann_sum_endpoint_holds is a one-line wrapper applying the physical Regge/EH concrete refinement-family one-statement.
why it matters
This is the Agent B endpoint Prop consumed by the integration lane. The companion theorem discharges it and feeds ForkHandoffIntegrationCert together with the one-statement fork A/B/C/D/E/F integration theorem, which states that Track 7 can consume Fork B's physical residual interface (among the other forks) without asserting the fully unconditional discovery theorem.
In the master plan this is the concrete Riemann-sum / product-filter handoff for Track 1.B-PHY / 1.C: once six-tet product-filter data are supplied, the master theorem's D2 input can be instantiated with the physical Regge/EH continuum limit. It does not close the remaining Track-1 displacement-class or open Schläfli leaves; those stay as the next dependency, consistent with the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.