periodicTranslateTTNormalEquationIdxEquiv5
plain-language theorem explainer
Packages translation of combined TT normal-equation indices by a fixed row-base vertex as a type-level equivalence on the 5-torus. Anyone proving row-frame generator closure or reindexing relative TT maps cites it. The inverse splits on the Sum of conformal vertex indices and longitudinal gauge indices, and both sides invert by the already-built vertex and gauge translation equivalences.
Claim. For any base vertex $b$ on the periodic $5\times5\times5$ torus, index translation by $b$ is an equivalence of the combined normal-equation index set with itself. That index set is the disjoint union of encoded conformal vertex indices and longitudinal gauge indices; translation acts by the corresponding vertex and gauge translations on each summand.
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on a periodic Regge complex. The conformal (vertex-scalar) ansatz cannot realize pure shear, so it misses transverse-traceless modes; this module therefore treats independent edge perturbations and longitudinal gauge generators separately from vertex-conformal ones.
The combined normal-equation index is the sum type of fixed conformal vertex-delta generators and fixed longitudinal vertex-vector generators on the $5$-torus. A typed row base is a vertex of that torus. Sibling equivalences already translate encoded vertices and longitudinal gauge indices by such a base; the present definition lifts those component maps to a single equivalence on the combined index.
The surrounding geometry imports the periodic Freudenthal torus and first-variation Regge action infrastructure used to set up TT hinge-aware analysis.
proof idea
Definitional packaging of an equivalence, not a deep theorem. Forward map is the existing combined index translation by the base. Inverse cases on the Sum: left summands invert via the encoded-vertex translation equivalence, right summands via the longitudinal-gauge translation equivalence. Left and right inverse proofs are case splits with simp unfolding the forward map, then congrArg on Sum.inl/Sum.inr applied to the component left_inv/right_inv lemmas.
why it matters
Needed so relative (row-frame) TT generator maps can be rewritten as global generator maps with coefficients pulled back along the base translation. Downstream, the equality of relative and shifted global maps uses this equivalence to reindex coefficients, and the generator-closure theorem builds a shifted coefficient vector by applying the inverse equivalence, then argues the translated combined generator space stays inside the fixed conformal-plus-longitudinal image.
In the Recognition gravity track this is scaffolding for the shear/TT sector that the conformal ansatz alone cannot cover: pure shear on rectangles is already shown not to be vertex-conformal. It does not itself force $D=3$ or the eight-tick structure; it is local linear-algebra bookkeeping on the $5$-torus normal equations that those later TT claims rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.