periodicExternalEdgeHeadIndex5
plain-language theorem explainer
Maps a typed edge on the 5×5×5 periodic Freudenthal torus to the external-order index of its head vertex (second endpoint). Downstream TT normal-equation generators use it to place conformal and longitudinal columns for each external edge. The body is a one-line projection through the existing external vertex indexer.
Claim. For an edge $e$ on the $5\times 5\times 5$ periodic Freudenthal torus, return the external-order natural-number index of the head vertex of $e$ (the second endpoint).
background
Track 1.D builds the tensor/shear sector beyond the Track 1.B conformal ansatz. The conformal slice assigns one scalar per vertex and averages endpoint potentials onto edges; that cannot represent pure shear or transverse-traceless gravitational-wave modes. This module therefore treats independent edge-length perturbations separately from vertex-conformal ones.
PeriodicEdge5 is the typed edge type on the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus. Edges carry ordered endpoints. An external vertex indexer already converts a torus vertex into a flat Nat index used by the external generator matrices that feed Python payloads. The head-index helper is the edge-level counterpart: it reads the second endpoint and reuses that vertex indexer.
proof idea
Definitional one-liner: apply the external vertex indexer to e.endpoints.2 (the head). No lemmas, no tactics; pure projection of the ordered endpoint pair.
why it matters
The external TT normal-equation generator matrix (rows = external edges; columns 0..124 conformal vertex deltas, 125..499 longitudinal vertex-component generators) and its sparse row dot product both need the head vertex index of each edge. Those defs call this helper so conformal averaging and longitudinal differences sit on the correct external columns. In the Recognition gravity track this is scaffolding for the shear/TT sector that the pure conformal ansatz cannot cover; it does not itself force $D=3$ or close a T0–T8 step, but it is the indexing glue for discrete TT generator assembly on the periodic torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.