periodicEdgeInnerProduct5_symm
plain-language theorem explainer
Symmetry of the finite edge-space pairing on real edge perturbations of the N=5 periodic Freudenthal triangulation: the sum of pointwise products is independent of argument order. Anyone building the transverse-traceless Gram matrix or residual identities in the tensor/shear sector cites it. The proof unfolds the sum definition and applies ring on each edge term.
Claim. Let $\varepsilon$ and $\eta$ be real-valued perturbations on the typed periodic Freudenthal edges of the $N=5$ triangulation. Then $\sum_e \varepsilon(e)\,\eta(e)=\sum_e \eta(e)\,\varepsilon(e)$, i.e. the finite edge-space inner product is symmetric.
background
Track 1.D opens the tensor/shear sector of weak-field gravity on a discrete triangulation. Track 1.B's conformal ansatz assigns one scalar potential per vertex and induces edge-length changes by averaging endpoints; that scalar slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module therefore treats independent edge perturbations separately from vertex-conformal ones and records the elementary rectangle obstruction for the conformal ansatz.
A periodic edge perturbation (for the N=5 typed Freudenthal edges) is simply a real function on those edges. The finite edge-space inner product used for the tensor/shear decomposition is the ordinary Euclidean pairing: sum over edges of the product of the two perturbation values. Symmetry of that pairing is the elementary algebraic fact recorded here.
proof idea
One short term-mode argument. Unfold the inner-product definition to an explicit Finset sum of pointwise products. Apply Finset.sum_congr with a reflexive index equality, then on each edge invoke ring to swap the two real factors. No external lemmas beyond the definition and standard sum congruence are required.
why it matters
The tensor/shear track needs a genuine inner product on edge space so that Gram matrices of generator families are well-defined and residual pairings reduce to load-minus-Gram identities. This symmetry lemma is the first algebraic property of that pairing.
It is used directly by the symmetric Gram-entry identity for the combined TT normal-equation generator family, by the residual-inner-product identity (pairing residual with a generator equals load minus Gram), and by the argument that a Gram-kernel coefficient vector produces the zero edge perturbation. Those results sit inside the discrete TT projection and normal-equation scaffolding that aims to isolate pure shear modes beyond the conformal ansatz. In the broader Recognition gravity program this is infrastructure for the weak-field tensor sector on the periodic Freudenthal torus, not yet a continuum or continuum-limit claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.