periodicLongitudinalGaugeMap5_apply_endpoint
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus, the longitudinal gauge map at an edge equals the discrete gradient of the three-component vertex coefficients dotted with the edge displacement. Only base and head endpoint coefficients contribute. Tensor/shear-sector work and gauge-fixing of edge perturbations cite this. Proof unfolds the generator stack and collapses a finite product-sum by distributivity.
Claim. For any real coefficient assignment $c$ on pairs (periodic vertex, spatial index $j\in\{0,1,2\}$) and any edge $e$ of the $5\times5\times5$ periodic Freudenthal torus, the longitudinal gauge map satisfies $G_{\mathrm{long}}(c)(e)=\sum_{j=0}^{2}\bigl(c(v_{\mathrm{head}},j)-c(v_{\mathrm{base}},j)\bigr)\,d_j(e)$, where $d_j(e)\in\{0,1\}$ is the $j$-th coordinate of $e$'s Freudenthal displacement.
background
Track 1.D builds the tensor/shear sector of weak-field gravity on the periodic Freudenthal lattice. Track 1.B's conformal ansatz places one scalar potential per vertex and averages endpoints to vary edge lengths; that scalar slice cannot represent pure shear, hence cannot cover transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones.
Edges live on the canonical $5\times5\times5$ periodic torus (PeriodicEdge5). Longitudinal gauge indices are pairs (vertex, spatial component in $\mathrm{Fin},3$): one vector component at one periodic vertex. The displacement coordinate map extracts, for each of the seven positive Freudenthal edge directions, the $0/1$ bit of that displacement along each spatial axis. The longitudinal gauge map is, by definition, generated by this vertex-vector basis.
proof idea
Term-mode proof. Unfold the three nested definitions of the longitudinal gauge map, its generator map, and the longitudinal generator. Rewrite the sum over the product index type (vertex × component) as an iterated sum via Fintype.sum_prod_type. A single simp with Finset.sum_sub_distrib, mul_sub, and mul_comm then factors the difference of endpoint coefficients and retains only the three spatial components contracted against the edge displacement coordinates.
why it matters
Establishes pure endpoint support for the concrete longitudinal gauge map: the value on an edge is exactly the discrete gradient of the gauge vector field dotted with the edge displacement. That is the lattice analogue of $\xi\mapsto\partial_{(i}\xi_{j)}$ longitudinal contamination of a metric perturbation. In the tensor/shear track it is the elementary identity needed before one can quotient edge perturbations by longitudinal gauge and isolate pure shear (and eventually TT) modes on the Freudenthal complex. The module imports Regge first-variation and periodic-torus geometry; this lemma sits at the gauge-generator layer of that scaffold. No downstream consumers are wired yet; it is infrastructure for the shear-sector development rather than a closed forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.