PeriodicLongitudinalGaugeIdx5
plain-language theorem explainer
Index type for the concrete longitudinal gauge basis on the fixed 5×5×5 periodic lattice: one spatial vector component at one periodic vertex. Downstream Track 1.D Gram/TT handoff endpoints cite it as the discrete domain for longitudinal generators. The body is a pure product abbreviation, not a proved claim.
Claim. The index set for the concrete periodic longitudinal gauge basis at lattice size $N=5$ is the Cartesian product of the periodic vertex set $V_{5,5,5}$ with the three spatial directions $\{0,1,2\}$. Each index therefore names one vector component at one vertex of the $5\times5\times5$ torus.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. Track 1.B already assigns a scalar potential at each vertex and induces edge-length changes by averaging endpoint potentials; that conformal slice cannot carry pure shear and therefore cannot represent transverse-traceless gravitational-wave modes.
This module separates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction: a nontrivial rectangle strain ($h \neq v$) has no vertex-conformal potential realization. The periodic geometry is the discrete $5\times5\times5$ torus; PeriodicVertex5 is exactly the vertex type of that torus (Vertex 5 5 5).
Longitudinal gauge modes are vectorial. Indexing them requires a vertex together with a spatial component, which is the product type defined here.
proof idea
Definitional abbreviation only: the type is the product of the periodic vertex type at $N=5$ with Fin 3 (three spatial directions). No lemmas, tactics, or proof obligations.
why it matters
Gives the discrete domain on which longitudinal gauge generators are enumerated in the finite TT Gram calculus at $N=5$. Master-theorem handoff endpoints in Track 1.D (Gram kernel criterion, kernel-generator map-to-zero, load image, load solver, range criterion, and the closed range endpoint that finishes the concrete TT projector split) all thread this index through their data packages.
Without a typed longitudinal basis index, the combined conformal-plus-longitudinal generator family cannot be stated, and the finite Fredholm/Gram criteria that close the TT decomposition stay ill-formed. The declaration is scaffolding infrastructure for the shear sector, not a physics theorem by itself; it sits downstream of the conformal obstruction and upstream of the TT projector closure at fixed $N=5$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.