PeriodicTTGramLoadImageData5
plain-language theorem explainer
Packages the geometric range condition for the finite transverse-traceless Gram operator on the N=5 periodic torus: every load induced by an edge perturbation lies in the image of the fixed Gram map on the combined conformal-plus-longitudinal coefficient space. Gravity Track 1.D and the master-theorem handoff cite it as the load-image half of the TT split. It is a structure with a single universal-existential field, not a proved theorem.
Claim. Data asserting that for every edge perturbation $\varepsilon$, the associated normal-equation load vector lies in the image of the finite TT Gram operator: there exist real coefficients on the combined index set (conformal vertex generators plus longitudinal gauge generators) such that applying the Gram map recovers the load at every index.
background
Track 1.D opens the tensor/shear sector of weak-field gravity on the Recognition lattice. Track 1.B's conformal ansatz puts one scalar at each vertex and averages endpoints to 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 normal equation is posed on a combined index set: conformal vertex-delta generators together with fixed longitudinal vertex-vector generators. The Gram operator is the associated finite symmetric map on coefficient space; the load is the linear functional of an edge perturbation against those generators. Spatial dimension is the forced $D=3$ of the forcing chain (T8).
The structure is deliberately weaker than a solver: it only asks that physical loads sit in the Gram image, which is the geometric half of closing a TT projector split on the periodic $N=5$ torus.
proof idea
No proof body: this is a structure definition whose single field is a proposition. Inhabiting it means exhibiting, for each edge perturbation, a coefficient function on the combined normal-equation index set that the Gram apply map sends to the load. Downstream constructors (for example ofKernelCriterionData) build such inhabitants from kernel-criterion data rather than by solving the linear system in place.
why it matters
This is the load-image package consumed by the Track 1.D master-theorem handoff. Track1DTTGramLoadImageReductionEndpoint takes an inhabitant and produces a load solver, a system solution, and TT projector data. The stronger kernel-criterion endpoint reduces through it: kernel criterion implies nonempty load-image data, then solver and projector. The range-closed endpoint at $N=5$ lists nonempty load-image data among the conjuncts that close the concrete TT projector split.
In the Recognition gravity program this is the geometric gate between pure shear edge modes and a well-posed finite TT normal equation, complementary to the conformal scalar track. It does not by itself force the eight-tick or $\phi$-ladder mass formula; it only supplies the image half needed so Track 7 can treat the TT split as closed once the kernel and range criteria are filled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.