Track1MixedAxisAddVertexBitsTranslationEndpoint
plain-language theorem explainer
Commutation of 5³-torus translation with local eight-corner bit addition on Freudenthal vertices. Track 1.B and the Track 7 fork-handoff certificate cite it as the Session 210 mixed-axis translation endpoint. The declaration is a Prop packaging that equality; the companion holds-theorem discharges it by the existing addVertexBits_translate5 lemma.
Claim. For every translation offset $a$ and cell $c$ on the $5\times 5\times 5$ periodic vertex lattice, and every cube-corner index $b\in\{0,\ldots,7\}$, adding the bit-offset $b$ after translating $c$ by $a$ equals translating by $a$ after adding $b$ to $c$.
background
The ambient setting is Gravity Track 7 fork-handoff integration: a receipt module that records parallel endpoints from Tracks 1.B, 1.C, 2.C, 3.C, 4.C, and 6 without upgrading the discovery claim. Track 1.B concerns stationarity reduction on the N=5 Freudenthal lattice.
Vertex5 is the abbreviation for vertices of the periodic $5\times 5\times 5$ torus. Translation translateVertex5 a v adds the offset $a$ componentwise in each Fin 5 coordinate. addVertexBits v b takes a cube-corner index $b:\mathrm{Fin},8$, expands it to three bit offsets via vertexBits, and advances the vertex by those bits on the periodic lattice.
The endpoint asserts that these two operations commute: translating then adding a local cube corner equals adding the corner then translating. That is the natural mixed-axis compatibility needed when stencil coefficients and residual interfaces move between absolute and translated frames.
proof idea
No proof body: this is a bare Prop definition packaging a universal equality. The companion theorem track1_mixed_axis_add_vertex_bits_translation_endpoint_holds is a one-line wrapper that applies the existing lemma addVertexBits_translate5, which already establishes the commutation on Vertex5.
why it matters
Session 210 Track 1.B local vertex-translation endpoint consumed by Track 7. It feeds track1_mixed_axis_add_vertex_bits_translation_endpoint_holds and is part of the reduction/interface package recorded by ForkHandoffIntegrationCert.
Per the integration certificate, the Track 1 result is a reduction/interface package, not a closure of the open Schläfli leaves; displacement-class leaves remain the next dependency. In the broader RS gravity stack this is bookkeeping for stencil and residual handoffs on the eight-corner cube of the Freudenthal torus (the discrete geometry side of the eight-tick / D=3 forcing chain), not a new dynamical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.