periodicTTLoadCoeffInnerProduct_eq_inner_generatorMap5
plain-language theorem explainer
On the finite N=5 periodic Freudenthal edge space, pairing the TT normal-equation load of an edge perturbation ε against coefficient vector c equals the edge inner product of ε with the combined conformal-plus-longitudinal generator mode built from c. Anyone assembling the finite TT Gram/Fredholm surface cites this adjoint identity. The proof unfolds the load and generator maps, applies right-linearity of the edge product, and finishes by ring.
Claim. For every edge perturbation $\varepsilon$ on the typed periodic Freudenthal edges of the $N=5$ torus and every coefficient vector $c$ on the combined conformal-vertex and longitudinal-gauge index set, the coefficient-space pairing of the TT normal-equation load of $\varepsilon$ with $c$ equals the edge inner product $\langle\varepsilon,\, G(c)\rangle$, where $G(c)$ is the combined generator map applied to $c$.
background
Track 1.D builds the tensor/shear sector missing from the Track 1.B conformal ansatz. Vertex-scalar potentials induce only averaged endpoint edge strains and cannot represent pure shear, so they miss transverse-traceless gravitational-wave modes. This module works with independent edge perturbations on the typed periodic Freudenthal edges of a finite $N=5$ torus.
The edge-space inner product is the plain finite sum $\sum_e \varepsilon(e),\eta(e)$. The combined normal-equation index set is the disjoint union of conformal vertex-delta generators and longitudinal vertex-vector generators. The generator map sends a coefficient vector to the corresponding linear combination of those fixed edge modes (via the gauge generator map). The load of an edge perturbation $\varepsilon$ is the dual coefficient vector obtained by pairing $\varepsilon$ against each generator.
The identity proved here is the elementary adjoint relation between that load pairing and the edge inner product against the generated mode.
proof idea
Unfold the four definitions that package the coefficient pairing, the load, the combined generator map, and the underlying gauge generator map. After unfolding, the right-hand side is an edge inner product against a finite linear combination of basis modes. Apply the right-linearity lemma periodicEdgeInnerProduct5_linear_combo_right to pull the sum and coefficients outside. The two sides become identical finite sums over the combined index set; finish each summand by ring.
why it matters
This adjoint identity is the bridge between coefficient-space pairings and edge-space geometry for the finite TT normal equation. Downstream it is consumed by PeriodicTTGramKernelCriterionData5, the kernel-criterion data structure for the finite TT Gram operator: that structure is the finite Fredholm-alternative surface on which one proves loads lie in the Gram image by showing they annihilate the Gram kernel.
In the broader Recognition gravity track, the tensor/shear sector is what lets the discrete geometry carry pure shear and hence TT wave content beyond the conformal scalar slice. The identity itself is pure finite-dimensional linear algebra on the $N=5$ periodic edge space; it does not yet force continuum GR or the eight-tick/D=3 landmarks, but it is a necessary bookkeeping step toward a discrete TT decomposition compatible with those constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.