euclideanProjector_not_lorentzTransverse_on_nullAxis
plain-language theorem explainer
The Euclidean transverse projector on the null-axis wave covector is not Lorentz-transverse. Anyone assembling a Lorentzian TT split for null gravitational waves needs this negative control before trusting a Euclidean formula on the light cone. The proof evaluates the Lorentz load at the time index, reduces it to the raised null component, and obtains a nonzero contradiction.
Claim. Let $m$ be the fixed null-axis wave covector on $\mathbb{R}^{1,3}$. The Euclidean transverse projector $P^E(m)=I-m\otimes m/\|m\|_E^2$ (well-defined since $\|m\|_E^2=2\neq 0$) fails Lorentz transversality to $m$: the contractions $(P^E(m)\cdot m^\sharp)_i$ do not all vanish.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1). It treats symmetric $4\times 4$ real matrices against a Minkowski wave covector on $\mathrm{Fin},4$, signature $(-+++)$, including the physically relevant null case. Covectors are lowered by default; index raising flips the sign of the time component. Lorentz transversality means that every row of $H$ contracts to zero against the raised wave covector $m^\sharp$, equivalently that the Lorentz load $(H\cdot m^\sharp)_i$ vanishes for all $i$.
The Euclidean transverse projector is the naive non-null formula $I-m\otimes m/|m|_E^2$. It is defined on the null axis because the Euclidean norm squared is $2\neq 0$, but the ambient geometry is Minkowski. The companion non-null Lorentz projector uses the Minkowski pairing in the denominator; the null case needs an auxiliary null partner. This lemma records that the Euclidean formula does not secretly satisfy the Lorentz condition on the light cone.
proof idea
Assume for contradiction that the Euclidean projector is Lorentz-transverse to the null-axis wave. Pass through the equivalence IsLorentzTransverse_iff_lorentzLoad and evaluate the load at the time index $i=0$. Unfold the projector and apply the load lemmas for the identity, scalar multiples, and outer-square terms, together with the null-axis Euclidean-dot identity, to reduce the load at index $0$ exactly to $(\mathrm{raise},m)_0$. Simplifying the raised null-axis components yields a nonzero value, contradicting vanishing of the load.
why it matters
In the Lorentzian TT layer the correct null projector uses an auxiliary null partner $l$ with $m\cdot l\neq 0$, not the Euclidean formula. This negative result blocks the naive substitution of the Euclidean projector on the light cone and forces the genuine null construction. It sits inside the algebraic scaffolding for edge_tt_decomposition and does not yet feed a named parent theorem (no downstream uses). Framework-wise it is pure linear algebra on the Minkowski wave covector; it does not touch the forcing chain T0–T8, RCL, or the phi-ladder mass formula, but it is a necessary hygiene step before any claim that edge perturbations decompose into Lorentz TT modes on null characteristics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.