periodicExternalEdgeIndex5
plain-language theorem explainer
Encodes a directed edge on the fixed 5×5×5 periodic Freudenthal torus as a single natural number. The code is base-vertex external index times 7 plus the discrete displacement label. Track 1.D payload generators and shear-sector numerics cite it to keep edge arrays in a fixed external order. The body is a one-line arithmetic packing of the already-defined vertex encoder.
Claim. For an edge $e$ on the $5\times 5\times 5$ periodic Freudenthal torus, the external edge index is $I_V(e_{\mathrm{base}})\cdot 7 + d_1(e)$, where $I_V$ is the canonical external vertex index of the edge base and $d_1(e)$ is the first component of the discrete displacement of $e$.
background
Track 1.D opens the tensor/shear sector of weak-field gravity on discrete geometry. Track 1.B only varies edge lengths through a vertex scalar potential; that conformal slice cannot carry pure shear or transverse-traceless modes. This module therefore treats independent edge-length perturbations separately from vertex-conformal ones and records elementary rectangle obstructions for the conformal ansatz.
The ambient lattice is the concrete $N=5$ periodic Freudenthal torus: vertices and edges are the standard periodic types with periods $(5,5,5)$. Edges carry a base vertex and a discrete displacement. An upstream sibling already packs vertices into a single external natural index; the present definition extends that packing to edges so that numerical Track 1.D generators share one fixed ordering of edge slots.
proof idea
Pure definition, not a proof. The body multiplies the external index of the edge base vertex by 7 and adds the first component of the edge displacement. The factor 7 is the packing stride that matches the external edge order used by the Track 1.D payload generators. No lemmas are invoked.
why it matters
Gives the canonical external edge numbering for the $N=5$ torus used throughout the tensor/shear scaffold. Without a shared encoder, conformal-versus-shear comparisons and payload dumps would disagree on array layout. It sits beside the vertex encoder and the PeriodicEdge5 / PeriodicTorus5 abbreviations that fix the concrete geometry for Track 1.D. Downstream use is not yet wired in this graph snapshot; the intended consumers are shear-sector certificates and numerical generators that must address edges by a stable Nat key. Framework role is infrastructural rather than a forcing-chain step: it supports discrete Regge-style weak-field work that aims at TT modes beyond the conformal ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.