periodicTranslateTTNormalEquationIdx5
plain-language theorem explainer
Defines the translation action of a fixed torus vertex (row base) on the combined index set of TT normal-equation generators: conformal vertex-delta slots and longitudinal gauge slots. Anyone building the finite Regge TT system on the 5-period torus cites it to move generators with the lattice. The body is a two-branch pattern match sending left summands through the encoded-vertex translate and right summands through the longitudinal-gauge translate.
Claim. Fix a base vertex $b$ on the period-$5$ torus. The map $T_b$ sends a combined TT normal-equation index to another such index: on a conformal generator labeled by encoded vertex $v$ it returns the conformal index of the $b$-translate of $v$; on a longitudinal gauge index $i$ it returns the gauge index obtained by translating the underlying vertex by $b$ while keeping the vector component fixed.
background
Track 1.D opens the tensor/shear sector of the weak-field Regge model. The older conformal ansatz puts one scalar potential at each vertex and averages endpoints to get edge strains; that slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module isolates independent edge perturbations and builds a finite TT normal system on a concrete periodic geometry.
The ambient lattice is the period-$5$ torus (PeriodicVertex5 is the vertex type of the $5\times5\times5$ cell). Combined normal-equation indices are a disjoint sum: left summands are conformal vertex-delta generators (one per torus vertex), right summands are fixed longitudinal vertex-vector gauge generators. Translation of those two pieces is already defined separately (encoded-vertex equivalence on the conformal side; vertex shift with frozen vector component on the gauge side). The present map is their joint action on the sum type.
proof idea
Definition by cases on the sum type, not a proved theorem. On Sum.inl v apply the existing encoded-vertex translate by the base and rewrap as left. On Sum.inr i apply the existing longitudinal-gauge translate by the base and rewrap as right. No tactics or lemmas beyond those two sibling maps.
why it matters
Gives the lattice action needed so the finite TT normal matrix transforms covariantly under row-frame shifts on the period-$5$ torus. Downstream it is the toFun of the packaged equivalence periodicTranslateTTNormalEquationIdxEquiv5, and it is the index map in the identity periodicTTNormalEquationGenerator5_relativeColumn_eq_shift: a row-frame translate of any combined generator column equals the globally shifted generator column. That covariance is the bookkeeping step toward a well-posed discrete TT/shear sector beyond the conformal ansatz, on the gravity track that aims at weak-field modes the scalar slice cannot see. It does not itself close the shear obstruction or produce continuum TT waves; it only moves generator labels consistently.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.