shiftVertex
plain-language theorem explainer
On the periodic N³ cubic lattice, shift a vertex x by one of the seven nonzero positive cube displacements d. Anyone writing the seven-class Freudenthal stencil energy or matching periodic-edge endpoints cites this. The body is a one-line composition of bit-addition with the fixed displacement table.
Claim. Given a vertex $x$ on the periodic $N\times N\times N$ cubic lattice and a displacement class $d\in\{0,\ldots,6\}$, return the vertex $x+d$ obtained by adding the corresponding triple of Boolean unit steps (axis, face-diagonal, or body-diagonal) componentwise modulo $N$.
background
This module is Stage 1 of panel-locked Test G in the QG full-theory campaign: the action-level continuum limit of the frozen quadratic energy on the canonical periodic Freudenthal triangulation, for every side length $N>2$. The target identity rewrites the canonical Regge-Hessian quadratic form as a seven-class nearest-displacement stencil $\sum_x\sum_d c_d(u(x+d)-u(x))^2$ with weights $\sqrt{\ell_d^2}\in{1,\sqrt{2},\sqrt{3}}$.
Vertices are triples in $\mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$. The seven nonzero positive cube steps are tabulated by dispBits as Boolean triples (three axis, three face-diagonal, one body-diagonal). Componentwise wrap-around addition of a Boolean step is addBits. The present definition packages those two primitives into the lattice translation $x\mapsto x+d$ used by every stencil sum in the module.
proof idea
Pure definitional wrapper: unpack the Boolean triple (dx,dy,dz) := dispBits d and return addBits x dx dy dz. No lemmas, no tactics; the equality with PeriodicEdge.endpoints is definitional (rfl downstream).
why it matters
This is the lattice translation that makes the seven-class stencil well-defined. Downstream, freudenthalStencilEnergy sums $c_d(u(\mathrm{shift},x,d)-u(x))^2$ over all bases and classes; periodicEdge_endpoints_eq records that a periodic edge with base $x$ and class $d$ has endpoints $(x,\mathrm{shift},x,d)$; and canonicalEdgeStencil_eq_freudenthalStencil plus freudenthal_stencil_identity promote that sum to the exact Regge-Hessian quadratic form and the panel-locked normalized continuum identity $\rho(N)Q_N(u)=h^3\sum c_d((u(x+d)-u(x))/h)^2$. Stage-2 energy-limit witnesses (stencil_inner_sum_witness, freudenthalStencilEnergy_witness) evaluate the same shift on a sinusoidal sample field. It is scaffolding for the tensor-first anisotropic continuum limit (candidate C8), not a physics claim by itself; the pillar-2 path-sum flag remains red.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.