periodicTTGramKernel5
plain-language theorem explainer
Defines kernel membership for the finite transverse-traceless Gram operator on the 5-periodic torus: a real coefficient vector on the combined conformal/longitudinal generator index lies in the kernel when Gram-apply vanishes at every index. Downstream Fredholm and range-criterion structures cite this predicate as the kernel side of the alternative. Pure definitional zero-set of the Gram map; no proof content.
Claim. A coefficient function $c$ on the combined conformal-vertex and longitudinal-gauge index set of the 5-periodic torus belongs to the kernel of the finite TT Gram operator when $(\mathrm{Gram}\, c)_i = 0$ for every combined index $i$.
background
Track 1.D opens the tensor/shear sector of weak-field gravity. The older conformal ansatz places one scalar 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 therefore treats independent edge perturbations separately from vertex-conformal ones.
The domain of the coefficient vector is the combined normal-equation index: a sum of the finite vertex set of PeriodicTorus5 (conformal vertex-delta generators) and the longitudinal vertex-vector gauge indices. The Gram map is the self-adjoint normal-equation operator that pairs generator coefficients against edge residuals on that fixed finite complex.
Kernel membership is the statement that this Gram map sends the coefficient vector to the zero function on the same index set.
proof idea
Definitional. The body is the single universal quantification that Gram-apply of the coefficient vector vanishes at every combined normal-equation index. No tactics, no lemmas, no reduction.
why it matters
This predicate is the kernel side of the finite Fredholm alternative for the TT Gram operator. Downstream structures package it into kernel-criterion data, generator-map-zero data, and range-criterion data: to place a load in the Gram image it is enough that the load annihilates every kernel coefficient vector, once the finite range criterion is known.
The companion theorem that every Gram-kernel coefficient generates the zero edge perturbation, and the proved range/Fredholm criterion for this fixed operator, both quantify over this predicate. The load-annihilation predicate for edge perturbations is likewise defined by universal quantification over it. Together they close the finite-algebra input needed before continuum or continuum-limit TT statements can be stated on the periodic complex.
Local to the shear track; not a forcing-chain (T0–T8) step, but infrastructure for representing TT modes that the conformal ansatz cannot reach.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.