periodicTTNormalEquationGram_selfAdjoint5
plain-language theorem explainer
The finite transverse-traceless Gram operator on the combined conformal-plus-longitudinal coefficient space is self-adjoint for the standard coefficient inner product. Gravity and discrete-geometry workers cite it when packaging the N=5 periodic TT normal equations as a symmetric operator. The proof is a four-step finite-sum calc: distribute, commute sums, apply Gram-entry symmetry, and reassemble.
Claim. For coefficient vectors $a,b$ on the combined normal-equation index (conformal vertex generators plus longitudinal gauge generators), $\langle G a,\, b\rangle = \langle a,\, G b\rangle$, where $G$ is the Gram operator of the fixed generator family under the edge-space inner product, and $\langle\cdot,\cdot\rangle$ is the coefficient-space $\ell^2$ product.
background
Track 1.D isolates the tensor/shear sector that the Track 1.B conformal ansatz cannot reach. Vertex-scalar potentials induce only averaged edge-length strains and miss pure shear, so they cannot alone represent transverse-traceless weak-field modes. This module works on the finite periodic torus with $N=5$ and treats independent edge perturbations separately from vertex-conformal ones.
The coefficient space is indexed by the sum type of conformal vertex indices and longitudinal gauge indices. Each index maps to an edge perturbation via the combined generator family (conformal generators on the left summand, longitudinal gauge generators on the right). The edge-space inner product is the plain sum of pointwise products over the finite edge set. The Gram operator applies that inner product against the generator family and returns a coefficient vector; the coefficient inner product is the matching $\ell^2$ sum on those coefficients.
Upstream, the Gram-entry symmetry lemma already records that the bilinear form on generators is symmetric in its two indices, which is the only geometric input needed for operator self-adjointness.
proof idea
Unfold the coefficient inner product, the Gram-as-vector map, and the Gram apply definition so both sides become double finite sums. First distribute the outer factor of $b_i$ through the inner sum and rearrange scalars by ring. Commute the two Finset sums. On each summand replace the generator inner product by its swapped form via the Gram-entry symmetry theorem. Finally factor $a_j$ back out of the inner sum (mul_sum plus ring) to match the expanded form of $\langle a, G b\rangle$. No analysis or continuum limit appears; the argument is pure finite-dimensional linear algebra over $\mathbb{R}$.
why it matters
Self-adjointness of the finite TT Gram operator is the algebraic prerequisite for treating the discrete normal equations as a symmetric problem on coefficient space and for transporting them into Mathlib's Hilbert-space linear-map API. Downstream, it is applied verbatim as the Track 1.D self-adjointness endpoint consumed by Track 7 handoff integration, and it feeds the theorem that the transported Gram map is LinearMap.IsSymmetric in the Hilbert wrapper.
In the broader Recognition gravity program this closes a concrete finite-model obligation on the shear/TT side: once the Gram form is symmetric, range and solvability criteria for the combined conformal-plus-longitudinal normal equations become standard linear-algebra statements rather than ad-hoc sum identities. It does not by itself force continuum GR or the eight-tick/D=3 landmarks; it is infrastructure inside the discrete tensor sector scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.