Track1MixedAxisEdgeEndpointsTranslationEndpoint
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus, translating a periodic edge by a lattice vector translates both of its endpoints by that same vector. Gravity Track 1.B and the Track 7 fork-handoff certificate cite this as the edge-endpoint translation interface. The property is the Prop packaging of the already-proved translateEdge5_endpoints fact.
Claim. For every lattice vector $a$ on the $5\times 5\times 5$ periodic torus and every periodic edge $e$, the endpoints of the translated edge equal the pair of translated endpoints: $(\tau_a e)_\pm = \tau_a(e_\pm)$.
background
Track 7 (Fork Handoff Integration) records parallel gravity-track endpoints without upgrading the discovery claim. Fork A covers Track 1.B stationarity reduction at $N=5$ on the discrete Freudenthal torus.
Vertex5 is a point of the $5\times 5\times 5$ periodic lattice; PeriodicEdge5 is a periodic edge on that torus (base vertex plus displacement). Translation translateVertex5 a v adds $a$ componentwise in each $\mathbb{Z}/5\mathbb{Z}$ factor. Edge translation translateEdge5 a e moves the base by $a$ and keeps the displacement fixed, so the geometric edge is rigidly shifted.
The claimed identity says that this base-shift definition is compatible with the endpoint pair: translating then reading endpoints equals reading endpoints then translating each.
proof idea
This declaration is a bare Prop alias, not a proved theorem. Its body is the universal statement equating (translateEdge5 a edge).endpoints with the pair of translateVertex5 images of the two endpoints. The companion theorem track1_mixed_axis_edge_endpoints_translation_endpoint_holds discharges it in one line by applying the upstream lemma translateEdge5_endpoints.
why it matters
Session 210 packages this as a Track 1.B edge-endpoint translation endpoint consumed by Track 7. Downstream, track1_mixed_axis_edge_endpoints_translation_endpoint_holds asserts the Prop, and ForkHandoffIntegrationCert aggregates Fork A–F handoffs: Track 1 contributes reduction/interface facts (including Schläfli and displacement-class leaves), not full closure of open Schläfli leaves.
In the gravity stack this guarantees that mixed-axis stencil and residual constructions see translation-covariant edge geometry on the $N=5$ torus, so local edge-stencil correspondence can feed physical finite-probe Regge/EH residual and contracted Bianchi interfaces without endpoint bookkeeping drift. It does not finish the master theorem; remaining Track 1 displacement-class leaves stay open dependencies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.