decomposition_hypothesis_fails_at_zero
plain-language theorem explainer
The Euclidean squared momentum of the zero 4-covector vanishes, so the nonzero-wave hypothesis required by the 4D transverse-traceless decomposition fails at the origin. Anyone delimiting the domain of the algebraic edge TT decomposition cites this boundary fact. The proof is a one-line simplification through the zero-wave momentum identity.
Claim. It is not the case that the Euclidean squared momentum of the zero covector on $\mathbb{R}^4$ is nonzero: $\neg\bigl(\sum_{i\in\mathrm{Fin}\,4} 0\cdot 0 \neq 0\bigr)$. Equivalently, that squared norm equals zero, so any hypothesis demanding a nonzero wave covector excludes the origin.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition (Wave 4 / W4-1): the linear-algebra transverse-traceless decomposition of symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. Conventions lift the 3D closer chain (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin; Minkowski/null specialization is deferred.
The squared momentum of a covector $m:\mathrm{Fin},4\to\mathbb{R}$ is the Euclidean sum of squares $\mathrm{momentumSq}(m)=\sum_i m_i^2$. The companion lemma zero_wave_momentumSq records that this quantity is identically zero on the zero covector. The TT decomposition is stated only for nonzero wave covectors, so the zero case must be excluded explicitly.
A parallel statement in the Lorentzian 4D module replaces Euclidean squared momentum by the Minkowski pairing and records the same failure at the origin.
proof idea
One-line term/tactic proof: simp rewrites the goal with zero_wave_momentumSq, which unfolds momentumSq on the constant-zero map and reduces the sum of products $0\cdot 0$ to $0$. The resulting $\neg(0\neq 0)$ is immediate. No case splits or external lemmas beyond that identity.
why it matters
Closes the zero-wave boundary of the algebraic TT kernel so that every named result in the Euclidean 4D edge decomposition can assume a nonzero covector without silent gaps. The module doc is explicit that this layer does not decompose Regge EDGE perturbations, does not prove $S_{\mathrm{RS}}$ converges to Einstein-Hilbert in 4D, and does not flip gap_action_recovery; it only supplies the linear-algebra substrate.
The Lorentzian twin (EdgeTTDecompositionLorentz4D.decomposition_hypothesis_fails_at_zero) mirrors the same exclusion for the Minkowski pairing, keeping the Euclidean and Lorentzian algebraic lanes aligned. Within the broader Recognition gravity stack this is scaffolding hygiene for the eight-tick / $D=3$ continuum limit work, not a dynamical claim about polarizations or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.