periodicEdgeInnerProduct5
plain-language theorem explainer
The standard Euclidean pairing on real edge perturbations of the finite 5×5×5 periodic Freudenthal torus: sum over edges of the pointwise product. Anyone proving the conformal/shear orthogonal split in Track 1.D cites it as the ambient inner product. The body is a one-line finite sum, not a derived identity.
Claim. For real-valued edge perturbations $\varepsilon,\eta$ on the typed edge set of the $5\times 5\times 5$ periodic Freudenthal torus, define $\langle\varepsilon,\eta\rangle_{E_5}:=\sum_{e}\varepsilon(e)\,\eta(e)\in\mathbb{R}$.
background
Track 1.D separates independent edge-length perturbations from the Track 1.B conformal ansatz. The conformal slice assigns one scalar potential per vertex and induces edge variations by averaging the two endpoint potentials; that scalar family cannot represent pure shear, so it misses transverse-traceless weak-field modes.
Edge data live on PeriodicEdge 5 5 5, the encoded edge set of the canonical $5\times 5\times 5$ periodic Freudenthal torus. A perturbation is simply a real function on that finite edge type. The ambient pairing used for the tensor/shear decomposition is the ordinary $\ell^2$ product of those functions.
Downstream work treats the conformal log-strain subspace as a linear slice inside this finite-dimensional edge space and asks for concrete vectors orthogonal to the whole slice.
proof idea
Pure definition: expand the pairing as the finite sum over all typed periodic edges of the pointwise product of the two edge functions. No lemmas, no tactics, no algebraic reduction.
why it matters
This pairing is the ambient form for the orthogonal split that shows the conformal ansatz is incomplete. Downstream, the face shear on a square collapses the 875-term sum to four supported edges, pairs to zero against every conformal log-strain (endpoint averages telescope), and has self-norm squared equal to 4, giving an explicit nonzero vector in the conformal orthogonal complement. The same pairing shows uniform $x$-strain has a nonzero component in that complement. Those facts are the witness form of Deliverable 5 in the SevenGaps edge-tensor sector: the orthogonal complement inside the finite edge space is nontrivial, so pure shear (and eventually TT gravitational-wave modes) sit outside the vertex-conformal slice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.