periodicEdgeInnerProduct5_zero_left
plain-language theorem explainer
The zero edge perturbation is orthogonal to every finite edge perturbation under the N=5 edge-space inner product on the periodic Freudenthal torus. Tensor/shear-sector arguments cite this as the trivial left-zero identity for that product. The proof is a one-line simplification of the defining finite sum.
Claim. For every real-valued edge perturbation $\eta$ on the typed periodic Freudenthal edges at $N=5$, the edge-space inner product of the zero map against $\eta$ is zero: $\sum_e 0\cdot\eta(e)=0$.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. Track 1.B's conformal ansatz puts one scalar at each 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 separately from vertex-conformal ones.
An edge perturbation here is simply a real function on the typed periodic Freudenthal edges (the $N=5$ finite triangulation). The edge-space inner product used for the tensor/shear split is the plain finite sum $\sum_e \varepsilon(e),\eta(e)$. The present identity is the elementary left-zero property of that product.
proof idea
One-line wrapper: unfold the definition of the $N=5$ edge-space inner product and simplify. The sum of products against the zero map collapses immediately to zero; no further lemmas are required.
why it matters
Feeds the zero case of TT-orthogonality on the same finite edge space: the downstream result that the zero edge map is orthogonal to every gauge image is proved by applying this left-zero identity to each conformal (or gauge) competitor. In the Track 1.D scaffold that identity is the first algebraic check that the edge inner product behaves like a genuine pairing before one isolates pure shear from the conformal slice. It does not yet construct TT modes, but it clears the trivial kernel step those constructions rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.