periodicGaugeSubspace5_spanned_by_longitudinalGeneratorMap
plain-language theorem explainer
Any edge perturbation in the concrete longitudinal gauge image on the period-5 Freudenthal torus is a finite linear combination of the vertex-vector delta generators. Gravity workers isolating the TT/shear slice cite this to replace an abstract gauge-membership hypothesis by explicit coefficients. The proof is a one-line specialization of the generic gauge-subspace spanning lemma to the longitudinal generator family.
Claim. Let $g$ be a real-valued perturbation of the typed period-5 Freudenthal edges. If $g$ lies in the longitudinal gauge subspace (i.e., $g$ is the image of some coefficient assignment on $\mathrm{PeriodicVertex}_5\times\{1,2,3\}$ under the concrete longitudinal gauge map), then there exist coefficients $c_i$ such that for every edge $e$, $g(e)=\sum_i c_i\,G_i(e)$, where $G_i$ are the vertex-vector delta generators.
background
Track 1.D separates pure shear (tensor) edge perturbations from the Track 1.B conformal ansatz, which assigns one scalar potential per vertex and cannot represent transverse-traceless gravitational-wave modes. The ambient space is real functions on the typed edges of the period-5 Freudenthal torus (PeriodicEdgePerturbation5).
A gauge subspace is defined existentially: an edge field $\varepsilon$ lies in the subspace for a chosen gauge map if $\varepsilon$ equals that map applied to some gauge potential. Here the potential type is assignments on PeriodicVertex5 × Fin 3 (one spatial vector component at each periodic vertex), matching the forced spatial dimension $D=3$ from the T8/T9 chain.
The longitudinal generators are the concrete vertex-vector delta family: each basis index places a unit vector component at one vertex and induces the corresponding edge increments. The theorem asserts that this family spans the image of the longitudinal gauge map.
proof idea
One-line wrapper. Apply the generic lemma periodicGaugeSubspace5_spanned_by_generatorMap to the concrete family periodicLongitudinalGaugeGenerator5, the given edge field $g$, and the membership hypothesis $hg$. That lemma already converts existential gauge-map membership into an explicit finite sum against the supplied generator map; no further algebra is needed.
why it matters
Inside the Track 1.D tensor/shear scaffold this discharges the longitudinal half of the gauge-image description: after the conformal slice is handled by the encoded vertex-delta family, the remaining diffeomorphism-like directions are spanned by the vertex-vector generators. Downstream projector data (the gauge-generator projector block immediately below in the file) can therefore treat longitudinal gauge as an explicit finite-dimensional span rather than an opaque operator image.
That is the sharper Track 1.D target once the conformal half is closed: TT modes are defined by orthogonality, in the finite periodic-edge inner product, to both the conformal slice and this longitudinal span. The result sits in the gravity domain and uses $D=3$ from the forcing chain, but does not itself prove existence of TT zero modes or close the full Regge shear analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.