periodicExternalEdgeOfEncodedIdx5
plain-language theorem explainer
Decodes a flat external edge index on the 5×5×5 periodic Freudenthal torus into a base vertex plus displacement under the Track 1.D order edge_index = vertex_index·7 + disp. Cited by anyone aligning Lean TT normal-equation generators with the Python payloads. The body is pure arithmetic: integer division and remainder by 7, then the matching external vertex decoder.
Claim. Given an external edge index $i$ ranging over the edges of the $5\times 5\times 5$ periodic Freudenthal torus, return the edge whose base vertex is the external decoding of $\lfloor i/7\rfloor$ and whose displacement label is $i \bmod 7$ (in $\{0,\ldots,6\}$).
background
Track 1.D opens the tensor/shear sector of the weak-field metric. The older Track 1.B conformal ansatz puts one scalar at each vertex and averages endpoints to get edge-length changes; that slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module therefore treats independent edge perturbations separately from vertex-conformal ones.
The ambient lattice is the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus. Edges are pairs (base vertex, displacement). The external numbering used by the numerical payloads is the product order edge_index = vertex_index · 7 + disp, with seven admissible displacements. The companion vertex decoder uses vertex_index = (x·5 + y)·5 + z.
The canonical torus edge equivalence goes through an opaque Fintype.equivFin order. This definition is the computable Lean-native twin that matches the payload generators exactly.
proof idea
Definitional construction, not a proof. Split the raw natural number of the finite edge index by integer division and remainder with modulus 7. Feed the quotient to the external vertex decoder to obtain the base; wrap the remainder as a displacement in Fin 7 (the bound is discharged by omega). Package base and displacement as a periodic edge on the 5×5×5 torus.
why it matters
Gives the edge-side coordinate chart that the external TT normal-equation generators read. Both the dense matrix-entry map and the sparse row dot product decode their edge index through this function, then pull base and head vertex indices for conformal averages and longitudinal component differences.
Without a Lean-native decoder locked to the Python payload order, the tensor/shear scaffold could not certify that the generator matrices used in numerics are the same objects formalized here. It sits downstream of the rectangle obstruction for the conformal ansatz and upstream of any claim that the TT sector is faithfully represented on the discrete torus.
Framework role is local to Gravity Track 1.D scaffolding: it does not itself invoke J-cost, the forcing chain, or the mass ladder, but it is infrastructure for discrete weak-field gravity on the recognition lattice (D = 3 spatial, eight-tick time structure elsewhere).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.