periodicEdgePerturbation5_eq_zero_of_inner_self_eq_zero
plain-language theorem explainer
On the finite-dimensional space of real edge perturbations of the 5×5×5 periodic Freudenthal torus, vanishing Euclidean self-inner-product forces the perturbation to be identically zero. Gravity and Regge analysts cite this when proving that Gram-kernel coefficient vectors generate only the zero edge mode. The argument is a short sum-of-squares positivity contradiction on a finite index set.
Claim. Let $\varepsilon$ be a real-valued function on the edges of the $5\times 5\times 5$ periodic Freudenthal torus. If the Euclidean edge inner product satisfies $\langle\varepsilon,\varepsilon\rangle=0$, then $\varepsilon\equiv 0$.
background
Track 1.D opens the tensor/shear sector of the weak-field Regge analysis. Track 1.B's 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 misses transverse-traceless gravitational-wave modes. This module therefore treats independent edge perturbations as primary data, separate from vertex-conformal log-strain.
An edge perturbation here is simply a real function on the typed edges of the periodic Freudenthal complex of side length 5 (the finite torus used throughout the stencil certificates). The associated inner product is the plain Euclidean pairing: sum over all edges of the product of the two values. The claim is the elementary positive-definiteness of that pairing on a finite real coordinate space.
proof idea
Apply function extensionality edgewise. Unfold the inner-product hypothesis to the statement that the sum of squares of the values of $\varepsilon$ vanishes. Suppose some edge value is nonzero; then that edge's square is strictly positive. The sum of squares is a sum of nonnegative terms with at least one strictly positive summand, hence is itself strictly positive (Finset.sum_pos'). Substituting the unfolded hypothesis yields $0<0$, which is impossible by irreflexivity of $<$ on the reals.
why it matters
This is the positive-definiteness lemma that closes the Gram-kernel argument in the same module: a coefficient vector in the periodic TT normal-equation kernel maps to the zero edge perturbation precisely because its generated mode has vanishing self-inner-product. Downstream, that zero-mode statement is the algebraic step that keeps the tensor/shear sector free of spurious kernel directions when independent edge strains are admitted beyond the conformal ansatz.
In the broader Recognition gravity track, the result is scaffolding for separating pure shear from vertex-conformal deformations on the discrete torus, a prerequisite for capturing TT wave content that the scalar conformal slice cannot see. It does not itself invoke the forcing chain (T5–T8) or the mass ladder; it is local linear algebra on the Regge edge space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.