periodicTTNormalEquationCoeffInnerProduct5
plain-language theorem explainer
Defines the Euclidean inner product on real coefficient vectors indexed by the combined conformal-plus-longitudinal normal-equation set for the fixed five-cell periodic torus. Anyone proving self-adjointness, kernel annihilation, or Fredholm range criteria for the finite TT Gram operator cites this pairing. The body is the plain finite sum of pointwise products.
Claim. For coefficient maps $a,b$ from the combined normal-equation index set (conformal vertex generators plus longitudinal gauge generators on the fixed periodic torus) into $\mathbb{R}$, the coefficient-space inner product is $\langle a,b\rangle=\sum_i a_i b_i$.
background
Track 1.D isolates the tensor/shear sector of weak-field Regge gravity. Track 1.B's conformal ansatz only assigns a scalar potential per vertex and cannot represent 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 fixed periodic torus.
The index type is the disjoint sum of conformal vertex-delta generators (one per torus vertex) and fixed longitudinal vertex-vector generators. Coefficient vectors are real functions on that finite index set. The present definition equips that space with the standard $\ell^2$ pairing used throughout the Gram-operator analysis.
Downstream Hilbert wrappers identify Mathlib's inner product on the corresponding Euclidean space with this sum, so symmetry and kernel statements can be stated either in coefficient language or in the transported Hilbert language.
proof idea
Definitional one-liner: expand as the finite sum over the combined normal-equation index of the pointwise product $a(\mathrm{idx}),b(\mathrm{idx})$. No lemmas are applied; the body is the Euclidean dot product on $\mathbb{R}^N$ for $N=|\mathrm{idx}|$.
why it matters
This pairing is the metric against which the finite TT Gram operator is tested for self-adjointness and Fredholm solvability. The master handoff endpoint Track1DTTGramSelfAdjointEndpoint is literally the statement that Gram is symmetric for this inner product. Sibling theorems identify it with the Hilbert-wrapper inner product and prove the transported Gram map is symmetric.
Kernel and range criterion structures (kernel-orthogonal loads imply loads lie in the Gram image) quantify annihilation by this same pairing. That finite Fredholm surface is the algebraic gate for solving the combined conformal-plus-longitudinal normal equations that isolate pure shear/TT content beyond the conformal ansatz. It does not itself invoke the forcing chain (T5–T8) or RCL; it is pure finite-dimensional linear algebra inside the gravity track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.