decomposition_hypothesis_fails_at_zero
plain-language theorem explainer
The zero covector on Fin 4 is never a non-null Minkowski wave: its self-pairing vanishes, so the non-null TT projector hypothesis fails at m = 0. Gravity analysts working the Lorentzian edge-TT layer cite this to fence off the null/zero cases from the non-null projector. The proof is a one-line simp of the zero-wave pairing identity.
Claim. It is not the case that the Minkowski pairing of the zero covector $m \equiv 0$ on $\mathrm{Fin}\,4$ with itself is nonzero: $\neg\bigl(\eta^{ij} m_i m_j \neq 0\bigr)$ when $m = 0$.
background
This module is the Lorentzian algebraic layer of the edge transverse-traceless (TT) decomposition campaign (Wave 4 / W4-1). Symmetric $4\times 4$ real matrices are decomposed against a Minkowski wave covector on $\mathrm{Fin},4$, signature $(-+++)$. Covectors are lowered by default; index raising negates the time component.
The Minkowski pairing is $\mathrm{minkowskiDot}(a,b) = -(a_0)(b_0) + (a_1)(b_1) + (a_2)(b_2) + (a_3)(b_3)$, equal to $\sum_j a_j (\mathrm{raise}, b)_j$. Non-null projectors require $\mathrm{minkowskiDot}(m,m)\neq 0$; the null case needs an auxiliary null $l$ with $m\cdot l\neq 0$. The zero covector sits outside both regimes.
Upstream, zero_wave_minkowskiDot records that the zero covector has vanishing self-pairing. The Euclidean sibling in EdgeTTDecomposition4D states the same fence for Euclidean momentum-squared.
proof idea
One-line tactic proof: simp rewrites the goal with zero_wave_minkowskiDot, which unfolds the Minkowski pairing on the constant-zero covector and simplifies to $0=0$. The double negation $\neg(0\neq 0)$ is then immediate. No case splits or classical choice beyond the ambient axiom footprint.
why it matters
Closes a boundary case in the Lorentzian TT linear-algebra layer: the non-null projector $P_{ij}=\eta_{ij}-m_i m_j/(m\cdot m)$ is undefined at $m=0$, and this theorem makes that failure explicit as a proved fact rather than an informal side condition.
It mirrors the Euclidean decomposition_hypothesis_fails_at_zero in EdgeTTDecomposition4D (which is both an upstream template and a downstream consumer of the same pattern). Within the QG campaign it supports the ledger name edge_tt_decomposition without claiming Regge-edge perturbation decomposition, Einstein-Hilbert recovery, or polarization normalizations. No forcing-chain landmark (T0-T8) is touched; this is pure Lorentzian linear algebra scaffolding for later gravity analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.