periodicEdgeInnerProduct5_add_right
plain-language theorem explainer
Right-additivity of the finite N=5 periodic edge inner product: the pairing of any edge perturbation ε against η+ζ equals the sum of the pairings against η and against ζ. Anyone proving TT orthogonality or decomposing shear modes on the periodic Freudenthal edge space cites this. The proof unfolds the Euclidean sum, distributes addition over Finset.sum, and closes each summand by ring.
Claim. Let $\varepsilon,\eta,\zeta$ be real-valued perturbations on the finite $N=5$ periodic Freudenthal edge set. With the edge inner product $\langle\varepsilon,\eta\rangle_5:=\sum_e\varepsilon(e)\,\eta(e)$, one has $\langle\varepsilon,\,\eta+\zeta\rangle_5=\langle\varepsilon,\eta\rangle_5+\langle\varepsilon,\zeta\rangle_5$.
background
Track 1.D builds the tensor/shear sector that the Track 1.B conformal ansatz cannot reach. The conformal ansatz assigns one scalar potential per vertex and induces edge-length changes by averaging endpoints; that scalar slice cannot represent pure shear, so it cannot cover transverse-traceless weak-field modes.
Here an edge perturbation on the typed periodic Freudenthal complex is simply a real function on the finite edge type PeriodicEdge5. The working inner product is the standard Euclidean pairing
$\langle\varepsilon,\eta\rangle_5=\sum_{e}\varepsilon(e),\eta(e)$
on that finite real vector space. Right-additivity is the elementary bilinearity fact needed before any orthogonality statement against conformal or longitudinal generator maps can be stated.
proof idea
Unfold the definition of the edge inner product to an explicit Finset.sum of pointwise products. Rewrite the goal with Finset.sum_add_distrib so the sum of products becomes a sum of sums. Apply Finset.sum_congr with a reflexive index equality, and on each edge close $\varepsilon(e)\cdot(\eta(e)+\zeta(e))=\varepsilon(e)\eta(e)+\varepsilon(e)\zeta(e)$ by ring. No external lemmas beyond Mathlib finite-sum distributivity are required.
why it matters
This is infrastructure for the tensor/shear decomposition on the N=5 periodic edge space. Downstream, periodicLongitudinalTTSubspace5_inner_generatorMap_eq_zero uses the pairing to prove that every longitudinal TT perturbation is orthogonal to every combined conformal-plus-longitudinal normal-equation generator map. The relative-frame Prop PeriodicRelativeTTGeneratorOrthogonalOnTT5 likewise demands that every TT edge field is orthogonal to every row-frame translate of that generator map; both statements need linearity of the pairing in the second slot.
In the broader Recognition gravity track, the point is to separate independent edge shear from vertex-conformal strain so that transverse-traceless gravitational-wave content can sit outside the conformal ansatz. The lemma itself is pure finite-dimensional linear algebra; its place is as a named building block rather than a physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.