periodicTTNormalEquationGramApply5
plain-language theorem explainer
Defines the finite Gram operator for the combined conformal-plus-longitudinal generator family on the N=5 periodic torus: at each combined index it returns the edge-space inner product of that generator against the linear combination of all generators weighted by the coefficient vector. Anyone working the TT normal equations or Fredholm-alternative range criteria cites it. The body is a direct finite sum of generator inner products.
Claim. For a coefficient map $c$ on the combined conformal-vertex and longitudinal-gauge index set $I_5$, and for any index $i \in I_5$, define $(\mathrm{Gram}\, c)(i) := \sum_{j \in I_5} c(j)\, \langle G_i, G_j \rangle_E$, where $G_k$ is the edge perturbation generated by index $k$ (vertex-conformal if conformal, longitudinal gauge if gauge) and $\langle\cdot,\cdot\rangle_E$ is the standard $\ell^2$ inner product on $N=5$ edge perturbations.
background
Track 1.D opens the tensor/shear sector because the Track 1.B conformal ansatz (one scalar potential per vertex, edge strains by endpoint averaging) cannot represent pure shear and therefore cannot cover transverse-traceless gravitational-wave modes. The module separates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction for the conformal slice.
On the concrete $N=5$ periodic torus, the combined normal-equation index set is the disjoint union of vertex indices (conformal generators) and longitudinal gauge indices (vertex-vector generators). Each index maps to an edge perturbation via the combined generator family: conformal indices yield vertex-delta conformal strains; gauge indices yield longitudinal gauge edge fields.
The finite edge-space inner product is the plain sum $\sum_e \varepsilon(e)\eta(e)$ over periodic edges. The Gram operator is the matrix of that inner product in the combined generator basis, applied to a coefficient vector.
proof idea
Pure definitional expansion: evaluate the double pairing by summing, over every combined index $j$, the product of the coefficient at $j$ with the edge inner product of the generator at the query index against the generator at $j$. No lemmas are invoked; the sum is the standard Gram action $\langle G_i, \sum_j c_j G_j \rangle$.
why it matters
This is the concrete linear operator whose kernel, image, and range criterion organize the finite TT normal equations. Downstream, the Gram kernel is defined as the zero set of this apply map; the theorem that kernel coefficients produce the zero edge perturbation uses it; the TT Gram linear map packages the vectorized form; and the load-image, range-criterion, and kernel-criterion data structures all quantify over or evaluate this apply map.
In the Recognition gravity track it is the algebraic surface on which the Fredholm alternative for the fixed conformal-plus-longitudinal family is stated: loads lie in the Gram image once they annihilate the Gram kernel and the finite range criterion holds. It does not yet force $D=3$ or the eight-tick octave; those enter elsewhere in the forcing chain. It closes the definitional half of the shear-sector scaffold so that kernel and solvability statements can be written without re-expanding the double sum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.