Track1MixedAxisSelectedCellTranslationEndpoint
plain-language theorem explainer
On the 5×5×5 torus, the selected periodic cube cell of the Freudenthal explicit-fiber model is equivariant under lattice translation: translating an edge then selecting its cell equals selecting then translating the vertex. Track 1.B / Session 210 cites this as the mixed-axis local translation endpoint. The declaration is a Prop packaging that commuting square; the companion theorem discharges it by selectedCell5_translate.
Claim. For every vertex $a$ on the $5\times 5\times 5$ torus, every periodic edge $e$, and every local Freudenthal pair $(\mathrm{tet},\mathrm{slot})\in\mathrm{Fin}\,6\times\mathrm{Fin}\,6$, the selected base cell of the $a$-translate of $e$ equals the $a$-translate of the selected base cell of $e$.
background
Track 7 (this module) is the fork-handoff integration lane for Gravity: it records what parallel endpoints prove without upgrading the discovery claim. Fork A covers Track 1.B stationarity reduction at $N=5$; the remaining displacement-class leaves stay open.
Vertices and edges live on the periodic cube lattice of side 5: a vertex is a triple in $(\mathbb{Z}/5)^3$, and a periodic edge pairs a base vertex with a displacement. Translation by $a$ adds $a$ componentwise (mod 5) to the base, leaving the displacement fixed. A Freudenthal local pair is a finite $(\mathrm{tet},\mathrm{edge\text{-}slot})$ index in $\mathrm{Fin},6\times\mathrm{Fin},6$, the table left after isolating the periodic-cell base-offset equation.
The selected cell of an edge relative to such a pair is the matching base cell of the cube-edge base of the local edge against the edge's base vertex. The endpoint asserts that this selection map intertwines edge translation with vertex translation.
proof idea
Definition only: the body is the universal quantification stating the commuting square, not a proof. The companion theorem track1_mixed_axis_selected_cell_translation_endpoint_holds is a one-line wrapper that applies the existing lemma selectedCell5_translate to inhabit this Prop.
why it matters
Session 210 Track 1.B local translation endpoint for the mixed-axis explicit-fiber coefficient model. It is consumed by Track 7's fork handoff package: the companion holds theorem feeds the integration certificate that bundles Forks A–F. Downstream, ForkHandoffIntegrationCert treats Track 1 material as a reduction/interface package, not a closure of the open Schläfli leaves. The commuting property is the geometric sanity check that selected cells transform correctly under the $N=5$ torus action before stationarity and residual interfaces are assembled. It does not finish the master theorem; it locks one translation-equivariance leaf so later displacement-class work can cite a named endpoint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.