periodicLongitudinalGaugeGenerator5
plain-language theorem explainer
Defines the elementary longitudinal gauge generator on the periodic Freudenthal edge lattice: one basis vector for each pair (vertex, spatial component). On an edge it returns the signed displacement coordinate of that component, positive when the vertex is the head and negative when it is the base. Downstream gauge maps and TT projectors cite this as the concrete span of pure-gauge edge strains. The body is a direct piecewise formula, not a derived identity.
Claim. For each index $(v,j)$ with $v$ a periodic vertex and $j\in\{0,1,2\}$, define an edge strain $\delta_{(v,j)}$ by $\delta_{(v,j)}(e)=d_j(e)$ if $v$ is the head of $e$, $\delta_{(v,j)}(e)=-d_j(e)$ if $v$ is the base of $e$, and $0$ otherwise, where $d_j(e)$ is the $j$-th coordinate of the Freudenthal displacement of $e$.
background
Track 1.D isolates the tensor/shear sector of weak-field edge strains on the periodic Freudenthal torus. Track 1.B's conformal ansatz puts one scalar at each vertex and averages endpoints; that slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module therefore treats independent edge perturbations $e\mapsto\mathbb{R}$ separately from vertex-conformal ones.
A longitudinal gauge index is a pair (periodic vertex, spatial component in $\mathrm{Fin},3$). An edge perturbation is any real function on the typed periodic edges. The displacement coordinate $d_j(e)$ extracts the $j$-th bit of the seven positive Freudenthal edge displacements (0 or 1). The generator below is the discrete analogue of $\partial_i\xi_j+\partial_j\xi_i$ restricted to a unit vector field supported at one vertex.
proof idea
Pure definition by cases. For index $(v,j)$ and edge $e$, read $d:=d_j(e)$ from the edge displacement; return $d$ if $v$ equals the head endpoint, $-d$ if $v$ equals the base, else $0$. No lemmas are invoked; the formula is the content.
why it matters
This generator is the atomic pure-gauge mode used throughout the tensor/shear scaffold. The finite longitudinal gauge map is the linear span of these generators; endpoint-support and generator-map identities are immediate corollaries. Downstream, the gauge subspace is proved spanned by them, and TT projector data packages them as the gauge generators so that transverse-traceless residual strains are well-defined without a separate span obligation. In the broader RS gravity track this is the discrete step that separates longitudinal gauge from shear, enabling a clean TT sector on the eight-tick / $D=3$ lattice rather than remaining stuck in the conformal scalar slice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.