PeriodicTTNormalEquationIdx5
plain-language theorem explainer
Combined discrete index for the normal equations of the periodic transverse-traceless (TT) sector on the fixed 5-torus: one slot per conformal vertex-delta generator plus one slot per longitudinal vertex-vector gauge generator. Anyone writing coefficient-space residual certificates or the Track 1.D Gram operator cites this type. It is a pure type abbreviation, the disjoint sum of the two generator families.
Claim. On the fixed periodic 5-torus, the combined normal-equation index set is the disjoint union $\mathrm{Fin}(n_V)\,\sqcup\,I_{\mathrm{long}}$, where $n_V$ is the number of vertices and $I_{\mathrm{long}}$ indexes the fixed longitudinal vertex-vector gauge generators. The left summand labels conformal vertex-delta generators; the right summand labels longitudinal gauge generators.
background
Track 1.D opens the tensor/shear sector of the weak-field Regge analysis. Track 1.B's conformal ansatz puts one scalar potential at each vertex and varies edge lengths by averaging endpoint potentials; that slice cannot represent pure shear, so it misses transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction for the conformal ansatz.
The normal equations for the TT residual (Regge Hessian minus lattice Lichnerowicz) are posed in a finite coefficient space whose basis is generated by two families: fixed conformal vertex-delta modes (one per vertex of the periodic torus) and fixed longitudinal vertex-vector gauge modes. PeriodicTorus5 is the concrete periodic geometry; its vertex count $n_V$ supplies the conformal half of the index. The longitudinal half is the already-defined gauge index type for that same torus.
Downstream certificates store residual dispersion coefficients as maps from this combined index into $\mathbb{R}$, and the Track 1.D Gram endpoint quantifies self-adjointness of the associated finite operator on coefficient space.
proof idea
Definitional abbreviation only: the type is the Lean Sum of Fin of the torus vertex count with the longitudinal gauge index type. No proof obligations; no lemmas applied.
why it matters
This index is the coefficient-space domain for essentially every Track 1.D residual certificate in the module. The encoded Hessian/Lichnerowicz structures (EncodedTTHessianLichnerowiczCoeffOriginColumnFormulaData5, the translated and relative variants, and the raw origin-column form) all store residual dispersion rows as maps Fin 7 → PeriodicTTNormalEquationIdx5 → ℝ and prove origin-column and translation formulas against that generator map.
It also feeds the master handoff: Track1DTTGramSelfAdjointEndpoint asserts that the fixed finite TT Gram operator is self-adjoint for the coefficient-space inner product on maps from this index into $\mathbb{R}$. Without a single combined index, conformal and gauge generators would not sit in one Gram matrix, and the self-adjointness endpoint could not be stated.
In the broader Recognition gravity track this is scaffolding infrastructure for the shear/TT sector that the conformal ansatz alone cannot reach; it does not itself invoke T0–T8 or the RCL, but it is the discrete index on which those continuum claims will eventually be checked in the weak-field lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.