addVertexBits_add_right
plain-language theorem explainer
On the periodic cubic lattice of side N, offsetting a vertex by a cube-corner bit-pattern and then translating equals translating first and then offsetting. Anyone building translation automorphisms of the embedded Freudenthal torus cites this commutation. The proof unfolds the bit-offset definition and applies the componentwise Bool-offset commutation lemma.
Claim. Let $N \ge 1$ and let $v,t$ be vertices of the periodic cube $(\mathbb{Z}/N\mathbb{Z})^3$. For any cube-corner index $a \in \{0,\ldots,7\}$, writing $\mathrm{addVertexBits}(v,a)$ for the vertex obtained by adding the three Boolean bit offsets encoded by $a$, one has $\mathrm{addVertexBits}(v+t,a)=\mathrm{addVertexBits}(v,a)+t$.
background
The ambient geometry is the periodic Freudenthal torus: vertices are the product of three cyclic groups $\mathrm{Fin},N \times \mathrm{Fin},N \times \mathrm{Fin},N$, with componentwise addition mod $N$. Cube-corner offsets are encoded by an element of $\mathrm{Fin},8$; the map that applies those three Boolean increments to a vertex is the local definition of the bit-offset operation (it factors through a lower-level three-Bool adder).
This module is a non-flag-bearing probe lane. It attaches the canonical periodic triangulation to the path-sum state space and checks that the translation group embeds into the relabeling automorphisms of that image. The present lemma is the vertex-level half of the translation-compatibility needed for those automorphisms.
Upstream, the three-Bool adder already commutes with lattice translation: adding Booleans after translating equals translating after adding Booleans. The cube-corner wrapper is only a packaging of that adder via a fixed bit decoding of $\mathrm{Fin},8$.
proof idea
Term-mode one-liner. Unfold the cube-corner offset to expose the underlying three-Bool adder applied to the decoded bits of $a$. The goal becomes exactly the statement of the Bool-offset commutation lemma on the same vertices $v,t$, which is applied directly (the three Boolean components are supplied by the bit decoding).
why it matters
PROBE C6 asks whether translations of the periodic torus embed into the automorphism group of its image in the path-sum complex. The construction of that embedding builds a relabeling automorphism for each lattice vector $t$ by conjugating typed translation through the canonical $\mathrm{Fin}$-indexings of vertices and edges. Both commutation fields of that automorphism are proved from bit-offset/translation compatibility; this lemma is the vertex half.
Downstream it is consumed by the translation-automorphism constructor. That constructor in turn yields injectivity of the embedding, the identity-at-zero law, and the homomorphism law, hence the cardinality lower bound $|\mathrm{Aut}(T_N)| \ge N^3$ and the path-sum measure upper bound $\mu(T_N) \le 1/N^3$. No continuum, measure-limit, or simpliciality claim is made here; the lemma only closes an algebraic landmine check on the discrete torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.