zero_wave_minkowskiDot
plain-language theorem explainer
The Minkowski pairing of the zero covector on Fin 4 with itself vanishes. Anyone checking the non-null or null TT projector hypotheses against the zero wave covector cites this. The proof is a one-line unfold of the pairing definition followed by simp.
Claim. For the zero covector $m \equiv 0$ on $\mathrm{Fin}\,4$, the Minkowski pairing satisfies $m \cdot m = 0$, i.e. $-(m_0)^2 + (m_1)^2 + (m_2)^2 + (m_3)^2 = 0$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1). It treats transverse-traceless decompositions of symmetric $4 \times 4$ real matrices against a Minkowski wave covector on $\mathrm{Fin},4$, including the null case, under signature $(-,+,+,+)$.
Covectors are lowered by default. The Minkowski pairing of two covectors 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 $m \cdot m \neq 0$; null projectors require $m \cdot m = 0$ with $m \neq 0$ and an auxiliary null $l$ with $m \cdot l \neq 0$.
The upstream definition is exactly that pairing: "Minkowski pairing of covectors: $\eta^{ij} a_i b_j$." The zero covector is the constant map $i \mapsto 0$.
proof idea
One-line wrapper. Unfold the definition of the Minkowski pairing, then simp evaluates each of the four products of zeros and sums them to zero. No lemmas beyond the definition are required.
why it matters
Feeds the immediate parent decomposition_hypothesis_fails_at_zero, which records that the non-null projector hypothesis $m \cdot m \neq 0$ fails at the zero wave covector. That negative fact is part of the Lorentzian linear-algebra hygiene for the ledger name edge_tt_decomposition: it marks the boundary between the non-null projector $P_{ij} = \eta_{ij} - m_i m_j/(m\cdot m)$ and the null/auxiliary construction.
Within the QG full-theory campaign this sits strictly in the algebraic layer. The module doc is explicit that the file does not decompose Regge EDGE perturbations, does not prove $S_{\mathrm{RS}}$ converges to EH in 4D, and does not flip gap_action_recovery. The result is a tiny but necessary sanity check so later TT statements can exclude the zero covector cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.