periodicTTNormalEquationGramVector5
plain-language theorem explainer
Packages the finite TT Gram action on coefficient functions as a map from coefficients to coefficients. Anyone proving self-adjointness, linearity, or Fredholm range criteria for the Track 1.D normal equations cites this packaging. The body is a one-line eta-expansion of the pointwise Gram apply.
Claim. Given a real coefficient function $c$ on the combined index set of fixed conformal vertex-delta generators and fixed longitudinal vertex-vector generators on the period-5 torus, return the coefficient function whose value at each index $i$ is the Gram pairing of $c$ against the generator family at $i$.
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on a discrete complex. The conformal (Track 1.B) ansatz only moves edge lengths by averaging vertex potentials, so it cannot carry pure shear or transverse-traceless modes. This module therefore works with independent edge perturbations and a fixed finite family of conformal plus longitudinal generators on the period-5 periodic torus.
The combined generator index is the sum type of vertex indices and longitudinal gauge indices. The pointwise Gram apply sums, over that finite index set, the product of a coefficient with the periodic edge inner product of the corresponding generators. The present definition simply reinterprets that apply as a map sending a coefficient function to another coefficient function (the Gram image vector).
proof idea
Definitional one-liner: the output at index idx is exactly periodicTTNormalEquationGramApply5 coeff idx. No lemmas are invoked; it is the eta-form of the already-defined Gram apply, so downstream code can treat the Gram operator as a function coeff ↦ Gram(coeff) rather than a curried bilinear evaluation.
why it matters
This packaging is the toFun of the TT Gram linear map on raw coefficient space, and it is the operator appearing in the finite self-adjointness theorem for the coefficient inner product. The master-handoff endpoint Track1DTTGramSelfAdjointEndpoint is literally the statement that this Gram vector map is self-adjoint for that inner product. The proved finite range/Fredholm criterion also routes loads through the same map: a load orthogonal to the Gram kernel lies in its range. In the Recognition gravity scaffold this is the discrete stand-in for the TT projector/normal equations needed once conformal scalar modes are split off, feeding the tensor/shear track toward weak-field GW content beyond the eight-tick and $D=3$ forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.