periodicEdgeInnerProduct5_linear_combo_right
plain-language theorem explainer
The finite periodic-edge inner product is linear in its right argument on any finite linear combination of edge perturbations. Anyone building Gram matrices, normal equations, or TT projectors on the five-edge Freudenthal torus cites this. The proof is a short sum-interchange calc: distribute the product, commute the double sum, and factor each coefficient.
Claim. Let $\iota$ be a finite index type, $\varepsilon$ an edge perturbation on the typed periodic Freudenthal edges, $c:\iota\to\mathbb{R}$ coefficients, and $b_i$ edge perturbations. Writing $\langle\varepsilon,\delta\rangle=\sum_e\varepsilon(e)\,\delta(e)$, one has $\langle\varepsilon,\sum_i c_i b_i\rangle=\sum_i c_i\langle\varepsilon,b_i\rangle$.
background
Track 1.D isolates the tensor/shear sector of weak-field edge-length variations on the periodic Freudenthal torus. The conformal (Track 1.B) ansatz only assigns a scalar potential per vertex and cannot represent pure shear, so it misses transverse-traceless gravitational-wave modes. This module works with independent edge perturbations instead.
A periodic edge perturbation is simply a real function on the typed finite edge set PeriodicEdge5. The associated inner product is the plain $\ell^2$ pairing: sum over edges of the pointwise product. Finite spanning families of such perturbations later generate conformal and gauge slices; projectors are built so the TT residual is orthogonal to every generator.
The ambient geometry is the $D=3$ spatial setting forced by the Recognition chain (T8), realized here as the periodic Freudenthal complex rather than a continuum metric.
proof idea
Unfold the inner product definition to an explicit edge sum. The right-hand argument is $\sum_i c_i b_i(e)$ pointwise, so the product $\varepsilon(e)\cdot(\sum_i\cdots)$ becomes an inner sum by Finset.mul_sum. Commute the double sum with Finset.sum_comm to group by the generator index $i$. Factor each $c_i$ out of the edge sum again by mul_sum, using ring on the scalar product. The resulting edge sums are exactly the inner products against the individual basis elements.
why it matters
This is elementary linear algebra, but it is the workhorse identity for the finite-generator TT projector surface announced in the module. Downstream it lets the Gram operator equal the inner product against the combined generator map, identifies load-coefficient pairings with that same inner product, shows Gram-kernel coefficient vectors produce the zero edge mode, and upgrades orthogonality to a finite spanning set into full TT orthogonality of the projected residual.
In the Recognition gravity program this closes a concrete step of Track 1.D: once conformal and gauge slices have finite spanning families, the residual after projection is certified TT by finite checks rather than an infinite continuum argument. It does not itself force $D=3$ or the eight-tick structure; those enter only as the ambient discrete geometry on which the edge set is defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.