nullAxisWave_dot
plain-language theorem explainer
The standard lightlike probe covector (1,1,0,0) is Minkowski-null under signature (−,+,+,+). Anyone locking the null-cone case of the Lorentzian edge TT decomposition cites this identity. The proof is a one-line unfold of the Minkowski pairing against the explicit components, followed by simplification.
Claim. Let $m=(1,1,0,0)\in\mathbb{R}^4$. With the Minkowski pairing $\eta^{ij}a_ib_j=-(a_0)(b_0)+(a_1)(b_1)+(a_2)(b_2)+(a_3)(b_3)$ of signature $(-,+,+,+)$, one has $m\cdot m=0$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1): transverse-traceless splitting of symmetric $4\times 4$ real matrices against a Minkowski wave covector on $\mathrm{Fin},4$, including the physically relevant null case. Signature is $(-,+,+,+)$; covectors are lowered by default.
The Minkowski pairing of two covectors is $\mathrm{minkowskiDot},a,b=-(a_0)(b_0)+\sum_{i=1}^3 a_i b_i$, equal to $\sum_j a_j(\mathrm{raise},b)_j$. The explicit null probe used throughout the residual identities is the four-vector $(1,1,0,0)$, built via the named-component constructor $\mathrm{vec4}$.
Null waves require a separate projector from the non-null case: when $m\cdot m=0$ and $m\neq 0$, one introduces an auxiliary null partner $\ell$ with $m\cdot\ell\neq 0$ and projects by $P_{ij}=\eta_{ij}-(m_i\ell_j+\ell_i m_j)/(m\cdot\ell)$. Establishing $m\cdot m=0$ for this probe is the first algebraic gate into that branch.
proof idea
One-line wrapper. Unfold the definitions of the Minkowski pairing and of the probe covector $(1,1,0,0)$, then simplify componentwise via the four-vector constructor. The arithmetic is $-(1)(1)+(1)(1)+0+0=0$; no external lemmas are required.
why it matters
This identity is the null-cone lock for the Lorentzian edge TT layer. Downstream it discharges the Minkowski-null predicate on the probe (nullAxis_MinkowskiNull), kills the naive non-null projector hypothesis on the null axis (naive_lorentz_projector_hypothesis_fails_on_nullAxis), and feeds the comparison showing that the Euclidean transverse projector, though defined, fails Lorentz transversality on the same null wave (euclideanProjector_not_lorentzTransverse_on_nullAxis).
Within the QG full-theory campaign it is pure linear algebra: it does not yet decompose Regge EDGE perturbations, prove $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or attach polarization normalizations. It simply certifies that the chosen residual probe sits on the light cone so the null-branch projector and residual identity are admissible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.