periodicEdge5EquivProd
plain-language theorem explainer
Canonical bijection: typed edges on the periodic 5×5×5 Freudenthal 3-torus are exactly pairs (base vertex, displacement in a 7-set). Downstream edge-count proofs cite it to get |E| = 125 × 7 = 875 without unfolding the encoded complex. The equivalence is definitional: project to (base, disp) and rebuild the structure, both inverses by rfl.
Claim. There is a canonical equivalence between the typed periodic edges of the $5\times 5\times 5$ torus and the product of its periodic vertices with a seven-element displacement index: each edge is uniquely a pair (base vertex, displacement).
background
Lane 3 of the Seven-Gaps gravity work studies the edge (tensor) sector on the actual periodic Freudenthal 3-torus beyond the vertex-conformal ansatz. That ansatz puts one scalar per vertex and induces the log-strain $(\xi_u + \xi_v)/2$ on each edge; the file measures how small that conformal image is inside the full edge-perturbation space.
PeriodicEdge5 is the abbreviation for typed edges of the $N=5$ periodic complex in each direction. By construction each such edge carries a base vertex and a displacement index in a 7-element set (the positive Freudenthal stencil directions). The companion vertex type is the $5^3$ lattice of periodic vertices.
The module already records the concrete counts $n_V = 125$ and $n_E = 875$, and the strict rank gap conformal image $\le 125 < 875$, so non-conformal shear modes exist. This equivalence is the bookkeeping step that turns the product structure of edges into a card computation.
proof idea
Pure structure equivalence. The forward map sends a typed edge to the pair of its base vertex and its displacement field. The inverse rebuilds the edge structure from that pair. Both left and right inverses hold by reflexivity of equality on the structure fields; no lemmas are invoked.
why it matters
Parent use is periodicTorus5_nE_eq, which proves the $5\times 5\times 5$ torus has $125 \cdot 7 = 875$ positive-displacement edges. That proof routes through the canonical edge equivalence and this product equivalence, then simp on the vertex type, avoiding deep unfolding of the encoded torus.
Those counts feed the dimension-gap theorems: conformal range has finrank at most $n_V = 125$, while the edge space has dimension 875, so the conformal slice is a proper subspace and explicit non-conformal witnesses (rectangle shear, uniform $x$-strain) live in the complement. In the Recognition gravity stack this is the concrete finite-complex evidence that the edge-tensor sector is strictly larger than the conformal ansatz on the eight-tick / $D=3$ Freudenthal lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.