PeriodicTTGramRangeCriterionData5
plain-language theorem explainer
Packages the finite-dimensional Fredholm range criterion for the fixed TT Gram operator on the N=5 periodic torus: any load orthogonal to the Gram kernel lies in the Gram image. Gravity Track 1.D cites it to close the longitudinal/TT split once kernel coefficients are known to give zero edge perturbation. It is a one-field structure holding that universal quantifier as data, not a proved theorem.
Claim. A datum asserting: for every real load on the combined conformal-plus-longitudinal normal-equation index set at $N=5$, if the load is orthogonal (under the normal-equation coefficient inner product) to every coefficient vector in the kernel of the finite TT Gram operator, then there exists a coefficient vector whose Gram image equals that load pointwise.
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on the fixed periodic Freudenthal torus at $N=5$. The conformal vertex ansatz only produces longitudinal edge strains; pure shear and transverse-traceless modes need independent edge perturbations and a projector that splits them from gauge.
The finite TT Gram operator is the self-adjoint map sending combined normal-equation coefficients (conformal vertex deltas plus longitudinal vertex-vector generators, indexed by PeriodicTTNormalEquationIdx5) to their Gram image. Its kernel is the set of coefficient vectors with vanishing Gram image. The coefficient inner product pairs loads against those vectors.
Upstream, kernel membership is already tied to zero edge perturbation. What remains as pure finite-linear-algebra input is the range half of the Fredholm alternative: orthogonality to the kernel implies membership in the range. This structure records exactly that criterion as reusable data.
proof idea
No proof body: this is a structure definition with a single field, the universal statement of the range criterion. Inhabitation is supplied elsewhere by periodicTTGramRangeCriterionData5_proved, which builds a Hilbert-space representative of the load, applies the finite-dimensional self-adjoint range fact, and transports back to coefficient space. Downstream wrappers such as PeriodicTTGramKernelCriterionData5.ofRangeCriterionData simply package an instance of this structure.
why it matters
Closes the last finite-algebra gate on Track 1.D. Master-theorem handoff treats nonempty instances of this structure as the range-closed endpoint and as the hypothesis of the reduction endpoint: once the range criterion is available, kernel criterion, load-image data, and the concrete TT projector at $N=5$ follow. The theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramRangeCriterionData turns any such datum into the full longitudinal/TT orthogonal decomposition target.
In the Recognition gravity program this is the discrete analogue of the continuum TT projector for gravitational waves: shear modes orthogonal to conformal and longitudinal gauge must be recoverable as Gram images. It does not itself force $D=3$ or the eight-tick octave; those sit upstream in the forcing chain. It only finishes the finite Gram step needed before continuum or continuum-limit claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.