PeriodicTTGramKernelGeneratorMapZeroData5
plain-language theorem explainer
Packages two finite-algebra hypotheses for the transverse-traceless Gram operator on the period-5 Freudenthal torus: loads orthogonal to the Gram kernel lie in the Gram image, and every Gram-kernel coefficient vector generates the zero edge perturbation. Downstream Track 1.D handoff and the longitudinal TT orthogonal-decomposition target consume this bundle. Pure structure definition; no proof content.
Claim. A data package for the TT Gram operator on the period-5 periodic torus asserting: (1) whenever a load $\ell$ on the combined normal-equation index set (conformal vertex generators plus longitudinal gauge generators) is orthogonal to every Gram-kernel coefficient vector, there exists a coefficient vector $c$ with $\mathrm{Gram}(c)=\ell$; (2) every Gram-kernel coefficient vector is sent by the generator map to the zero edge perturbation.
background
Track 1.D isolates the tensor/shear sector of weak-field Regge gravity. Track 1.B's conformal ansatz assigns one scalar per vertex and averages endpoints to get edge strains; that slice cannot carry 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 finite TT analysis works on the period-5 periodic Freudenthal torus. The combined normal-equation index set is the sum of conformal vertex-delta generators and fixed longitudinal vertex-vector generators. The Gram operator is the finite self-adjoint map on coefficient space induced by those generators; its kernel and range control solvability of the normal equation for a given load.
The companion kernel-criterion structure states the classical finite Fredholm surface: loads in the Gram image iff they annihilate the Gram kernel, plus a fixed range criterion. The present structure strengthens the packaging by also requiring that Gram-kernel coefficients generate the zero edge perturbation, so the geometric zero-mode side is already closed.
proof idea
Definitional structure with two Prop fields and no proof body. The first field is the range-of-kernel-orthogonal (finite Fredholm) criterion for the fixed Gram operator on the combined normal-equation index set. The second field asserts that the generator map sends every Gram-kernel coefficient vector to the zero function on edges. Inhabitants are supplied elsewhere; this declaration only names the interface.
why it matters
Closes the finite-algebra interface between Gram-kernel geometry and the concrete longitudinal TT decomposition on the N=5 torus. The theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramKernelGeneratorMapZeroData converts an inhabitant of this structure into the orthogonal-decomposition target by first building kernel-criterion data and then applying the criterion-to-target bridge.
The master-theorem handoff endpoint Track1DTTGramKernelGeneratorMapZeroReductionEndpoint treats this package as the reduction hypothesis: once Gram-kernel coefficients generate zero edge perturbations, the load-annihilates-kernel half of the finite criterion is automatic, and the remaining nonempty witnesses (criterion data, load-image data, projector data) become the Track 1.D discharge surface.
In the broader Recognition scaffold this is pure gravity-side linear algebra supporting the shear/TT sector that the conformal Track 1.B ansatz cannot reach; it does not itself invoke T5–T8 or the RCL, but it is required before TT modes can sit inside the forced D=3, eight-tick geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.