track1_mixed_axis_edge_endpoints_translation_endpoint_holds
plain-language theorem explainer
Translating a periodic edge on the 5-vertex stencil moves both endpoints by the same vertex translation and leaves the edge displacement unchanged. Gravity Track 7 cites this as the Session 210 mixed-axis edge-endpoint handoff into the fork integration certificate. The proof is a one-line term application of the certified edge-translation lemma.
Claim. For every vertex translation $a$ on the $N=5$ stencil and every periodic edge $e$, the endpoints of the translated edge equal the pair of individually translated endpoints: $(\mathrm{translate\_edge}(a,e)).\mathrm{endpoints} = (\mathrm{translate\_vertex}(a,e_1),\,\mathrm{translate\_vertex}(a,e_2))$.
background
Track 7 is the Gravity fork-handoff integration lane. It records what parallel forks prove without upgrading the discovery claim: Fork A (Track 1.B Schläfli stationarity at $N=5$), Fork B (physical residual and Bianchi interface), and related tracks. Remaining displacement-class leaves stay open.
The proposition packages a Session 210 Track 1.B fact about the mixed-axis periodic edge stencil. A periodic edge on the five-vertex complex carries two endpoints; translating the edge by a vertex $a$ must act componentwise on those endpoints. The upstream certificate translateEdge5_endpoints (Freudenthal axis stencil coefficients) already proves that identity and that displacement is preserved under the translation.
Local setting is discrete Regge/EH residual geometry on the physical six-tet cubic Dirichlet instance: edge stencils feed finite-probe residuals and the contracted Bianchi interface, not yet a continuum manifold integral.
proof idea
One-line term proof. The goal is definitionally the proposition that translated-edge endpoints equal the pair of translated vertices. That statement is exactly the theorem translateEdge5_endpoints from the Freudenthal axis stencil coefficient certificate, so the proof is the bare application of that lemma with no extra tactics or rewriting.
why it matters
This is the Session 210 edge-endpoint translation endpoint consumed by Track 7. It feeds forkHandoffIntegrationCert, the integration-lane certificate that bundles fork handoffs (Track 2 many-body, Track 1 Schläfli reduction, displacement-class reductions, and siblings).
In the Fork B narrative, local edge-stencil correspondence underpins the physical finite-probe Regge/EH residual conclusion and the structural contracted Bianchi interface. The module doc is explicit that this remains an interface result: the manifold integral target and a concrete physical Schläfli identity stay open. The lemma does not close those leaves; it only locks the translation-covariance of edge endpoints so downstream residual and Bianchi wiring can cite a proved endpoint rather than a hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.