periodicEdgeInnerProduct5_zero_right
plain-language theorem explainer
The edge-space inner product on the N=5 periodic Freudenthal triangulation vanishes when the second argument is the zero perturbation. Anyone assembling the finite TT Gram operator or checking kernel orthogonality will cite this bilinearity fact. The proof is a one-line simp unfolding of the sum definition.
Claim. For every edge perturbation $\varepsilon$ on the typed periodic Freudenthal edges of the $N=5$ triangulation, the finite edge-space inner product of $\varepsilon$ with the zero map is zero: $\langle \varepsilon,\, 0\rangle_5 = 0$.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. The conformal ansatz of Track 1.B assigns one scalar potential per vertex and induces edge-length changes by averaging endpoints; that slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module therefore treats independent edge perturbations as primary data.
A PeriodicEdgePerturbation5 is simply a real-valued function on the typed edges of the periodic Freudenthal triangulation at resolution $N=5$. The companion inner product is the plain Euclidean sum
$$\langle\varepsilon,\eta\rangle_5=\sum_e \varepsilon(e),\eta(e).$$
It is the finite edge-space pairing later used to build the TT Gram operator and its kernel criterion.
proof idea
One-line wrapper: simp unfolds periodicEdgeInnerProduct5 to the finite sum $\sum_e \varepsilon(e)\cdot 0$, which reduces termwise to zero.
why it matters
Bilinearity and non-degeneracy of the edge inner product are the elementary linear-algebra surface on which the finite TT Gram operator sits. Downstream, PeriodicTTGramKernelCriterionData5 packages the Fredholm-alternative criterion: a load lies in the Gram image once it annihilates the Gram kernel (together with a fixed finite-range check). The zero-right identity is the first half of that pairing's linearity, needed whenever kernel coefficients or loads are tested against the zero section.
In the broader Recognition scaffold this is pure Track 1.D bookkeeping: it does not yet force $D=3$ or the eight-tick octave, but it supplies the discrete $L^2$ structure required before shear modes can be separated from the conformal vertex slice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.