track1_mixed_axis_selected_cell_translation_endpoint_holds
plain-language theorem explainer
On the N=5 periodic torus, the selected cube cell of a translated edge equals the translate of the selected cell, for every Freudenthal local pair. Track 7 fork-handoff integration cites this as the Track 1.B mixed-axis translation endpoint. The proof is a one-line term wrapper of the already-proved selected-cell translation identity.
Claim. For every vertex $a$ on the $N=5$ torus, every periodic edge $e$, and every Freudenthal local pair $p$, the selected cell of the $a$-translate of $e$ at $p$ equals the $a$-translate of the selected cell of $e$ at $p$.
background
Track 7 is the integration-lane receipt for parallel fork handoffs in the gravity master theorem. It records endpoints without upgrading the discovery claim; remaining Track 1 displacement-class leaves stay open. Fork A covers Track 1.B stationarity reduction at $N=5$.
The endpoint concerns the explicit-fiber coefficient model on the $N=5$ torus. A selected cell assigns, to each periodic edge and Freudenthal local pair, the cube cell used by that coefficient stencil. Torus translation acts on vertices and edges; the claim is that selection commutes with that action.
Upstream, selectedCell5_translate already proves the identity by simplifying through the matching-base-cell translation lemma. The present declaration packages that fact as a named Track 1.B handoff Prop for the integration certificate.
proof idea
One-line term wrapper: the goal is definitionally the universal quantification proved by selectedCell5_translate in the Freudenthal axis stencil coefficient certificate. No extra tactics; the proof term is that theorem itself.
why it matters
Session 210 selected-cell translation endpoint consumed by Track 7. It feeds forkHandoffIntegrationCert, the integration-lane certificate that bundles Track 1, Track 2 many-body, and related fork receipts. The module doc places this under Fork A (Track 1.B 1B-SCH stationarity reduction at $N=5$): translation-normalization of the mixed explicit-fiber LHS, independent of the already-proved RHS stencil translation.
Without cell-selection commuting with torus translation, the mixed-axis coefficient model would not be translation-covariant on the periodic lattice, blocking clean reduction of the non-origin row probe at $(1,0,0)$. This closes that local covariance leaf so the handoff cert can record it as proved rather than scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.