sameUnordered_translate
plain-language theorem explainer
Translation of all four arguments by the same lattice vector leaves the unordered-pair match predicate unchanged on the 5×5×5 torus. Anyone auditing translation invariance of Freudenthal axis-stencil monomial coefficients cites this. The proof is a two-line injectivity argument: translation is an equivalence, so equalities of vertices are preserved under simultaneous shift.
Claim. For any shift $a$ and vertices $x,y,u,v$ on the $5\times 5\times 5$ periodic lattice, the boolean that reports whether $\{x,y\}=\{u,v\}$ as an unordered pair equals the same boolean evaluated on the four translated vertices $x+a$, $y+a$, $u+a$, $v+a$.
background
The module certifies, with exact rationals only, every coefficient of an unordered monomial $\xi(u)\xi(v)$ in the corrected $N=5$ mixed explicit-fiber axis-stencil residual (mirroring the Python audit script named in the module doc).
Vertex5 is the product lattice $\mathrm{Fin},5\times\mathrm{Fin},5\times\mathrm{Fin},5$. Translation by $a$ adds $a$ componentwise via modular arithmetic on each factor. The companion equivalence shows this map is bijective, with inverse translation by $-a$.
The predicate sameUnordered is the boolean decision of whether two ordered pairs represent the same unordered pair: $(x,y)$ matches $(u,v)$ or $(v,u)$. It is the gate that identifies which residual terms contribute to a given monomial coefficient.
proof idea
Extract injectivity of translation from the already-constructed equivalence translateVertex5Equiv a. Unfold sameUnordered and rewrite equalities of translated vertices via Injective.eq_iff, so each atomic equality $x=u$ (resp. $x=v$, etc.) holds after translation if and only if it held before. The boolean therefore evaluates identically.
why it matters
Feeds directly into scaledPairLocalVertexCoeff_translate, which lifts the same translation invariance to the scaled local vertex coefficient of a Freudenthal pair along a periodic edge. That parent step is part of the exact rational certificate that every unordered monomial coefficient in the corrected axis-stencil residual is translation-invariant on the $N=5$ torus.
In the broader gravity stack this is bookkeeping, not a forcing-chain landmark: it ensures the stencil residual is well-defined on the periodic lattice rather than on a choice of origin. Without it, the coefficient audit would have to re-run at every basepoint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.