periodicLongitudinalGaugeMap5_eq_generatorMap
plain-language theorem explainer
On the five-periodic torus, the concrete longitudinal gauge map equals the linear combination map built from the vertex-vector longitudinal generators. Anyone working the tensor/shear sector or TT residual gauge freedom would cite this. The proof is pure definitional equality (rfl).
Claim. The concrete longitudinal gauge map on the five-periodic edge strains equals the gauge-generator map applied to the finite family of vertex-vector longitudinal generators: for coefficient vectors $c$ on the longitudinal index set, the induced edge perturbation is $\sum_i c_i\, g_i$, where each $g_i$ is the signed edge-direction component of a unit vector field at one vertex.
background
Track 1.D builds the tensor/shear sector that the conformal (vertex-scalar) ansatz cannot reach. The conformal slice averages endpoint potentials into edge-length variations and therefore misses pure shear, including transverse-traceless weak-field modes. This module separates independent edge perturbations from vertex-conformal ones and records elementary rectangle obstructions.
A periodic edge perturbation assigns a real strain to each edge of the five-periodic torus. The gauge-generator map takes a finite family of such generators and a coefficient vector and returns the corresponding linear combination of edge strains. The concrete longitudinal generators are signed edge-direction components of unit vector fields at single vertices: positive at the head endpoint, negative at the base. The concrete longitudinal gauge map is defined to be exactly that generator map applied to this family.
proof idea
One-line definitional equality. The concrete longitudinal gauge map is introduced as the application of the generic gauge-generator map to the longitudinal generator family, so the stated equality holds by rfl.
why it matters
This pins the longitudinal residual gauge action in the fixed tensor sector to an explicit finite linear map on vertex-vector coefficients. Downstream TT predicates and zero-mode analyses can therefore treat longitudinal gauge as a concrete image of a generator map rather than an abstract subspace. In the broader Recognition gravity track it supports the separation of shear from conformal strain needed before claiming coverage of transverse-traceless modes on the periodic Freudenthal geometry. No parent theorems yet list this declaration; it is infrastructure for the shear-sector scaffold rather than a forcing-chain landmark (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.