periodicTTNormalEquationCoeffInnerProduct5_symm
plain-language theorem explainer
The coefficient-space bilinear form for the combined conformal-plus-longitudinal normal equations on the 5-periodic TT torus is symmetric in its two arguments. Anyone assembling the Gram matrix or invoking self-adjointness of that finite operator cites this. The proof unfolds the sum definition and applies ring termwise after Finset congruence.
Claim. Let $a,b$ be real coefficient vectors on the finite index set of the combined conformal-plus-longitudinal normal equations in the 5-periodic transverse-traceless setting. The associated coefficient-space inner product satisfies $\langle a,b\rangle=\langle b,a\rangle$.
background
Track 1.D isolates the tensor/shear sector of weak-field Regge gravity. The older conformal ansatz puts one scalar at each vertex and averages to edges; 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 builds finite normal equations on a periodic torus model.
The coefficient space here is the real function space on the finite index set of those combined normal equations (conformal generators plus longitudinal ones). The bilinear form in view is the Gram-type sum that pairs two coefficient vectors by summing products of their components against the fixed generator family. Symmetry of that form is the elementary algebraic step before treating the Gram operator as self-adjoint on the finite Hilbert wrapper.
proof idea
Term-mode proof. Unfold the definition of the coefficient-space inner product (a finite sum over the normal-equation index set). Apply Finset.sum_congr with reflexivity on the index set, then for each index use ring to equate the summand after swapping the two coefficient vectors. No external lemmas beyond the sum congruence and commutative ring arithmetic on $\mathbb{R}$.
why it matters
Self-adjointness of the finite Gram operator is the hinge for the range criterion: a load orthogonal to the kernel lies in the range. Downstream, periodicTTGramRangeCriterionData5_proved packages that finite-dimensional Fredholm fact for the fixed TT Gram data; it needs this symmetry identity on the combined generator family.
In the broader Recognition gravity track, this is scaffolding toward genuine TT/shear modes on the periodic geometry, beyond the conformal scalar slice of Track 1.B. It does not yet force continuum GR or the eight-tick/D=3 landmarks; it only clears the algebraic symmetry step inside the discrete normal-equation Gram matrix.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.