periodicEdgeProdEquiv
plain-language theorem explainer
Canonical bijection identifying each periodic edge on the N³ Freudenthal torus with a base vertex and one of seven displacement classes. Anyone reindexing edge sums into the seven-class stencil cites it. Both directions are the structure projections/constructors; inverses hold by reflexivity.
Claim. For every side length $N$, the set of periodic edges of the $N\times N\times N$ Freudenthal torus is in canonical bijection with pairs $(x,d)$ where $x$ is a lattice vertex and $d\in\{0,\ldots,6\}$ indexes the seven nearest-displacement classes (three axis, three face-diagonal, one body-diagonal). The map sends an edge to its base vertex and displacement class; the inverse rebuilds the edge from that pair.
background
This module is Stage 1 of panel-locked Test G in the QG full-theory campaign: prove that the frozen quadratic Regge Hessian on the canonical periodic Freudenthal triangulation equals a seven-class nearest-displacement stencil, for every side $N>2$.
A periodic edge carries a base vertex on the $N\times N\times N$ torus and a displacement class in Fin 7. The seven classes are the three axis steps, three face diagonals, and one body diagonal; their squared lengths are $1,1,1,2,2,2,3$, and stencil weights are the square roots of those lengths. The Dirichlet energy of the incidence graph is first rewritten as a sum over edges, then reindexed by this product structure so the sum becomes $\sum_x\sum_{d:0..6} c_d,(u(x+d)-u(x))^2$.
The equivalence is pure bookkeeping: it does not choose weights or impose dynamics. It only makes the (base, class) product available as a summation index.
proof idea
Definitional equivalence. Forward map sends an edge to the pair of its base vertex and displacement field. Inverse rebuilds the edge structure from that pair. Left and right inverses are both rfl because the structure fields are exactly those two components. No lemmas are invoked.
why it matters
Parent use is canonicalEdgeStencil_eq_freudenthalStencil: the canonical edge-stencil Dirichlet energy on the periodic Freudenthal triangulation equals the seven-class stencil energy for every $N$. That identity is the middle link in the Stage-1 chain (frozen Hessian quadratic form equals graph Dirichlet energy, then no-self-loop edge reindexing, then this product reindexing). Downstream the normalized stencil identity and the exact moment tensor $A_0=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$ sit on top of that equality. Without the product view, the seven-class sum cannot be written as a sum over vertices times displacement classes. Scope remains action-level continuum limit of the frozen quadratic energy; the pillar-2 path-sum flag stays red.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.