Track1FiniteProductResidualEstimateEndpoint
plain-language theorem explainer
Agent B's Track-1 endpoint asserts that every global residual envelope on the six-tet periodic quadrature data yields the finite full-Regge-to-EH-quadrature residual bound. Gravity handoff integrators cite it as the Fork-B residual gate before product-filter continuum limits. The body is a pure Prop alias quantifying the existing residual-target predicate over envelope packages.
Claim. For every index types $\alpha,\rho$, filter $\ell$ on $\alpha$, cross-cardinality data $D$, and global residual envelope package $E$ on $D$ (envelope function tending to $0$ along $\ell$ together with a slice-uniform absolute residual bound), the finite full-Regge-to-quadrature residual estimate target holds for $E$: the bound comparing the full Regge–Einstein–Hilbert residual to the six-tet volume quadrature is available at every residual index and every filter index.
background
Track 7 is the integration-lane receipt for parallel gravity fork handoffs. Fork B covers the Track 1.B-PHY / 1.C physical residual and Bianchi interface. This definition is the Agent-B residual endpoint inside that fork: it does not prove a new estimate, it names the Prop that every admissible global envelope must satisfy before product-filter convergence is allowed to run.
The upstream package CanonicalPeriodicTetSixTetVolumeQuadratureGlobalResidualEnvelopeData bundles three fields future geometry must fill: an envelope on the within-slice refinement parameter, convergence of that envelope to zero along the filter, and a slice-uniform absolute residual bound. The target predicate PhysicalReggeEHFiniteProductResidualEstimateTarget is the Session-587 concrete full-Regge-to-quadrature bound required before the product-filter continuum argument.
Spatial dimension $D=3$ appears only through shared constants forced by the T8/T9 chain; the residual statement itself is filter-and-envelope local to the six-tet cubic Dirichlet instance.
proof idea
Definitional, not a proof. The Prop is the universal quantification of PhysicalReggeEHFiniteProductResidualEstimateTarget over every global residual envelope package $E$ built on six-tet cross-cardinality data. No tactics, no lemmas applied at this site. The companion theorem track1_finite_product_residual_estimate_endpoint_holds discharges the endpoint by feeding each $E$ to physicalReggeEHFiniteProductResidualEstimateTarget_holds.
why it matters
Fork B cannot hand off a usable residual interface until the finite product residual estimate is named as a single endpoint. Downstream, track1_finite_product_residual_estimate_endpoint_holds proves the endpoint, ForkHandoffIntegrationCert records it among the Track-1 reduction/interface fields, and fork_A_B_C_D_E_F_handoffs_integrated_one_statement consumes that certificate in the one-statement Track-7 receipt.
Per the module doc, this records exactly what the new endpoints prove and does not upgrade the discovery claim; remaining Track-1 displacement-class leaves stay open. In the broader RS gravity stack it sits after the six-tet volume quadrature geometry and before product-filter continuum limits that feed the structural master theorem. It is residual bookkeeping on the discrete gravity side, not a T0–T8 forcing step, not an $\alpha$ or mass-ladder claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.