periodicDispSqEdge
plain-language theorem explainer
Assigns to each of the seven positive lattice displacement classes its squared Euclidean edge length: three axis steps of length squared 1, three face diagonals of length squared 2, and one space diagonal of length squared 3. Gravity and Regge stencil code cites this as the sole source of edge metric data on the periodic Freudenthal torus. It is a pure pattern-match table on Fin 7.
Claim. The map $d \mapsto \ell^2(d)$ from the seven positive displacement classes $d \in \{0,\ldots,6\}$ to squared edge lengths in $\mathbb{R}$ is defined by $\ell^2 = 1$ on the three axis-aligned classes, $\ell^2 = 2$ on the three face-diagonal classes, and $\ell^2 = 3$ on the unique space-diagonal class.
background
The module builds a typed periodic Freudenthal torus: vertices on a rectangular lattice torus, edges labelled by positive displacement classes, and tetrahedra from the standard cube triangulation. It does not yet fix a concrete finite mesh size; it isolates the combinatorial model so any finite encoder into Triangulation3D inherits the incidence and edge-slot partition needed by nonlinear Regge calculus.
In three dimensions the nonzero 0/1 displacement vectors fall into exactly seven classes up to sign and lattice periodicity: three of Hamming weight 1 (axis steps), three of weight 2 (face diagonals), and one of weight 3 (space diagonal). Squared Euclidean length on the unit lattice equals Hamming weight, so the metric data on every edge is completely determined by its displacement class.
Sibling constructions (dispBits, localEdgeOf, edge equivalences) identify each concrete edge with one of these seven classes. The present table is the unique place those classes are turned into real squared lengths.
proof idea
Pure definition by exhaustive pattern match on Fin 7. No lemmas, no tactics: indices 0–2 map to 1, 3–5 to 2, and 6 to 3. Downstream equalities (e.g. freudenthal tetrahedron edge lengths versus this table) are proved by fin_cases on the local edge index.
why it matters
Every global edge-length assignment on the periodic model factors through this table. canonicalGlobalSqEdge is literally periodicDispSqEdge composed with the edge-to-displacement equivalence; the preflight theorem canonical_globalSqEdge_eq records that the incidence-consistent triangulation uses exactly these values.
The equality freudenthalTet_sqEdge_eq_periodicDispSqEdge_localEdgeOf ties the classical Freudenthal cube triangulation edge lengths to the same table, so local tet geometry and global periodic geometry agree. Gravity analysis then builds stencil weights and the moment tensor $A_0$ from these squared lengths: diagonal entries become $1+2\sqrt{2}+\sqrt{3}$ and off-diagonals $\sqrt{2}+\sqrt{3}$, the exact kernel-checked continuum limit of the seven-class stencil.
The four-dimensional analogue dispWeight4 copies the same Hamming-weight pattern. The definition therefore sits on the geometry-to-Regge interface that the module’s remaining finite-encoder work must preserve.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.