PeriodicTTGramKernelCriterionData5
plain-language theorem explainer
Packages the finite Fredholm-alternative data for the transverse-traceless Gram operator on the period-5 Freudenthal torus: any load orthogonal to the Gram kernel lies in the Gram image, and every physical TT load annihilates that kernel. Track 1.D handoff endpoints cite it to close the TT projector split. Pure structure definition with two Prop fields; no proof body.
Claim. A data bundle asserting two facts for the finite TT Gram operator at period $N=5$: (i) if a load on the combined conformal-plus-longitudinal index set is orthogonal to every Gram-kernel coefficient vector, then that load lies in the image of the Gram map; (ii) every admissible TT load annihilates the Gram kernel.
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on the periodic Freudenthal torus. The conformal (vertex-scalar) ansatz of Track 1.B cannot carry pure shear, so independent edge perturbations and a transverse-traceless (TT) normal equation are needed for gravitational-wave modes.
The finite TT Gram operator maps coefficient vectors on the combined index set (conformal vertex-delta generators plus longitudinal vertex-vector generators, PeriodicTTNormalEquationIdx5) to loads. Its kernel is the space of coefficient vectors that produce zero under the Gram map. The classical finite-dimensional Fredholm alternative says a load is in the image iff it is orthogonal to that kernel.
This structure is exactly that surface for the fixed $N=5$ operator: the range-from-orthogonality implication, plus the claim that every physical TT load already annihilates the kernel. Spatial dimension $D=3$ (forced by the linking/T9 step) underlies the torus geometry.
proof idea
Definitional structure, not a theorem. The two fields are bare Props: range_of_kernel_orthogonal is the finite range criterion (orthogonality to periodicTTGramKernel5 implies existence of a preimage under periodicTTNormalEquationGramApply5), and loads_annihilate_kernel asserts periodicTTLoadAnnihilatesGramKernel5 for every admissible load. No tactics or lemmas; inhabitants are built downstream from proved range data or kernel-generator-map-zero data.
why it matters
This is the intermediate criterion surface that lets Track 1.D close the TT split without re-proving the full solver each time. Downstream, Track1DTTGramKernelCriterionReductionEndpoint states that an inhabitant yields nonempty load-image, load-solver, and projector data. Track1DTTGramRangeCriterionReductionEndpoint and Track1DTTGramKernelGeneratorMapZeroReductionEndpoint reduce into it from the proved range criterion or from kernel-generator-map-zero data; the corresponding _holds theorems build an inhabitant and hand it to Track 7.
In-module, periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramKernelCriterionData consumes it. Framework role: completes the shear/TT half of the weak-field metric sector beyond the conformal ansatz, on the $D=3$ eight-tick geometry. It does not itself settle continuum gravity; it packages the finite $N=5$ algebraic criterion the master handoff needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.