nullPMixed
plain-language theorem explainer
Mixed-index null projector entry P_i^a = δ_i^a − S_i^a for a pair of covectors m, l on Minkowski 4-space (signature −+++). Gravity analysts cite it when assembling the double projection PHP in the Lorentzian edge TT layer. The body is a one-line difference of the Kronecker delta and the mixed null shear term.
Claim. For covectors $m,l:\{0,1,2,3\}\to\mathbb{R}$ and indices $i,a$, the mixed null projector is $P_i{}^{a}=\delta_i^{a}-\dfrac{m_i(\uparrow l)^{a}+l_i(\uparrow m)^{a}}{m\cdot l}$, where $\uparrow$ raises an index with the Minkowski metric of signature $(-+++)$ and $m\cdot l$ is the Minkowski pairing.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (QG Wave 4 / lane W4-1). It specializes the Euclidean TT layer to signature $(-+++)$: covectors are lowered by default, and raising negates the time component so that (raise v) 0 = -v 0 and (raise v) i = v i spatially. The Minkowski pairing is minkowskiDot a b = -(a 0)(b 0)+∑_{k=1}^3 (a k)(b k).
In the null sector one takes minkowskiDot m m = 0 with m ≠ 0 and an auxiliary null covector l with m·l ≠ 0. The covariant null projector is then P_{ij} = η_{ij} − (m_i l_j + l_i m_j)/(m·l). The mixed version raises the second index of the shear. That shear is exactly nullSMixed: (m i · raise l a + l i · raise m a)/(m·l). The local Kronecker symbol kron i a supplies the identity piece of the mixed projector.
(The cost-functional symbol H from CostAlgebra is unrelated; here H always means a symmetric 4×4 matrix being projected.)
proof idea
Pure definitional arithmetic: subtract the mixed null shear nullSMixed m l i a from the Kronecker entry kron i a. No lemmas, no tactics; the body is the difference of two already-defined real-valued terms.
why it matters
This entry is the atomic factor in the double mixed projection nullPhp, which implements (P H P)_{ij} = P_i{}^a H_{ab} P_j{}^b. Downstream results built on it include: the entrywise gap expansion nullPhp_entry (identity minus two single shears plus the bilinear remainder); symmetry preservation nullPhp_symmetric when H is symmetric; Lorentz transversality of nullPhp to both null legs (nullPhp_lorentzLoad_m, nullPhp_lorentzLoad_l); and the contraction identities sum_nullPMixed_raise_l / sum_nullPMixed_raise_m that make those load vanishings work.
Those facts close the algebraic TT gap expansion in the null sector of the ledger item edge_tt_decomposition. The module tier tags are explicit: this layer does not yet decompose Regge EDGE perturbations on a 4D lattice, does not prove S_RS_converges_EH_4d, and attaches no physical polarization normalization. It is the linear-algebra substrate for that future bridge under the Recognition gravity program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.