periodicTTLoadAnnihilatesGramKernel5
plain-language theorem explainer
Predicate stating that the normal-equation load of a periodic edge perturbation is orthogonal to every TT Gram-kernel coefficient vector. Cited when assembling the finite Fredholm alternative for the periodic TT Gram operator on the five-edge Freudenthal torus. Pure Prop packaging: no proof content, only the kernel-annihilation condition.
Claim. For a periodic edge perturbation $\varepsilon$, write $L(\varepsilon)$ for its normal-equation load. Then $L(\varepsilon)$ annihilates the Gram kernel: every coefficient vector $k$ with $\mathrm{Gram}\,k=0$ satisfies $\langle L(\varepsilon),k\rangle=0$.
background
Track 1.D isolates the tensor/shear sector of weak-field Regge gravity. The conformal (vertex-potential) ansatz only produces longitudinal edge strains; pure shear and transverse-traceless modes require independent edge perturbations. On the typed periodic Freudenthal torus the edge space is finite, so the TT normal equations reduce to a finite Gram operator on coefficient vectors.
An edge perturbation $\varepsilon$ (a real assignment to each periodic edge) induces a load vector $L(\varepsilon)$ in the normal-equation dual. The Gram kernel consists of those coefficient vectors that the discrete TT operator sends to zero. Orthogonality of $L(\varepsilon)$ to that kernel is the classical Fredholm side-condition for solvability.
The sibling abbreviation PeriodicEdgePerturbation5 is simply the function type from periodic edges to reals. The Gram-kernel predicate and the load/inner-product maps are the other ingredients packaged here.
proof idea
Definitional Prop, not a proved theorem. The body is the universal quantification: for every coefficient vector, membership in the periodic TT Gram kernel implies that the normal-equation coefficient inner product of the load of $\varepsilon$ against that vector vanishes. No tactics or lemmas are applied; the declaration only names the annihilation condition.
why it matters
Supplies the kernel-annihilation half of the finite Fredholm alternative used by PeriodicTTGramKernelCriterionData5. That structure's range-of-kernel-orthogonal field states that a load lies in the Gram image once it annihilates every kernel vector (plus a fixed finite-range criterion). Without this predicate the criterion data cannot even be stated.
In the broader Recognition gravity track this is scaffolding toward genuine TT gravitational-wave modes on the discrete torus, beyond the conformal slice that cannot represent pure shear. It does not yet close the existence of nontrivial TT solutions; it only names the linear-algebra side-condition those solutions must satisfy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.