Track1PhysicalResidualBianchiEndpoint
plain-language theorem explainer
Packages Fork B as a single proposition: on any 3-torus grid with side lengths greater than 2, the canonical periodic edge-stencil local correspondence implies the physical finite-probe Regge/EH residual and contracted Bianchi interface. Track 7 handoff integration cites it as the Fork B receipt. The body is a pure Prop abbreviation; the companion theorem discharges it by one named lemma.
Claim. For all $N_x,N_y,N_z\in\mathbb{N}$ with each at least $3$, and all types $V,B$ with $B$ finite: if the canonical periodic edge-stencil local correspondence holds on the Freudenthal torus of those dimensions, then the physical Regge–Einstein–Hilbert residual Bianchi interface holds for those parameters (universe level $0$).
background
This module is the Track 7 integration-lane receipt for parallel fork handoffs. Fork B is the Track 1.B-PHY / 1.C lane: physical residual plus structural contracted Bianchi interface. The module records endpoints without upgrading the discovery claim.
The hypothesis is the canonical periodic edge-stencil local correspondence: on the encoded periodic Freudenthal torus of sizes $(N_x,N_y,N_z)$, there exist $r>0$ and $C\ge 0$ such that for every vertex potential $\xi$ with $|\xi|<r$, the local nonlinear Regge/J-cost matches a quadratic real edge-stencil Dirichlet operator (plus controlled remainder). That is the concrete six-tet cubic Dirichlet instance of the local stencil.
The conclusion is the physical Regge/EH Bianchi interface from Track1BCPhysicalResidual: finite-probe residual control together with the structural contracted Bianchi identity on the same torus data, parameterized by vertex and bond types $V,B$.
proof idea
This declaration is a Prop definition, not a proved theorem. It quantifies over grid sizes $N_x,N_y,N_z>2$ and types $V,B$ (with $B$ finite) and asserts the implication from canonical periodic edge-stencil local correspondence to the physical Regge/EH Bianchi interface.
The companion theorem track1_physical_residual_bianchi_endpoint_holds is a one-line wrapper applying physicalReggeEHBianchiInterface_of_localCorrespondence, which is exactly that implication specialized to universe level 0.
why it matters
Fork B endpoint consumed by the integration lane. It is one conjunct of fork_A_B_C_D_E_F_handoffs_integrated_one_statement, which packages Forks A–F plus the structural master certificate without asserting the fully unconditional discovery theorem. It also fills the corresponding field of ForkHandoffIntegrationCert.
In the Recognition gravity stack this is the handoff from local J-cost / edge-stencil Dirichlet geometry on the Freudenthal torus into residual and Bianchi structure used by Track 1 physical residual work. Doc-comment is explicit: interface result only; the manifold integral target and the concrete physical Schläfli identity remain open. Sibling endpoints cover Schläfli reduction and displacement-class stationarity leaves; those stay separate dependencies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.