nullLGaugeVector
plain-language theorem explainer
Defines the l-direction gauge covector for the null Lorentzian TT split of a symmetric 4×4 matrix H. Component j is the Lorentz load of H against the null wave covector m, divided by the Minkowski pairing m·l. Used by the null residual gap and by the existence theorem for the null edge TT decomposition. Pure definition: componentwise quotient, no proof obligations.
Claim. For covectors $m,l\in\mathbb{R}^{4}$ and a covariant matrix $H\in\mathrm{Mat}_{4}(\mathbb{R})$, the $l$-gauge vector $v^{L}$ is defined by $(v^{L})_{j}=(H\cdot m^{\sharp})_{j}/(m\cdot l)$, where $H\cdot m^{\sharp}$ is the Lorentz load (row contraction of $H$ against the raised covector $m$) and $m\cdot l$ is the Minkowski pairing $\eta^{ij}m_{i}l_{j}$.
background
This module is the Lorentzian algebraic layer of the QG campaign item edge_tt_decomposition (Wave 4 / W4-1). It specializes the Euclidean 4×4 TT layer to signature $(-+++)$, with covectors lowered by default and index raising flipping the sign of the time component.
The Minkowski pairing is $m\cdot l=-(m_{0})(l_{0})+\sum_{i=1}^{3}m_{i}l_{i}$. The Lorentz load of a matrix $H$ on a covector $m$ is the covector $(H\cdot m^{\sharp}){i}=\sum{j}H_{ij}(m^{\sharp})^{j}$. In the null case one takes $m\cdot m=0$, $m\neq 0$, and an auxiliary null partner $l$ with $m\cdot l\neq 0$; the transverse projector is then $P_{ij}=\eta_{ij}-(m_{i}l_{j}+l_{i}m_{j})/(m\cdot l)$.
The residual identity decomposes $H-PHP$ into an $m$-gauge piece, an $l$-gauge piece, and a bilinear correction. This definition supplies the coefficient covector of the $l$-gauge term.
proof idea
Definition only. Each component is the corresponding component of lorentzLoad H m divided by minkowskiDot m l. No tactics, no lemmas, no side conditions are discharged at the definition site; non-vanishing of the denominator is imposed by callers.
why it matters
Closes the coefficient side of the null residual. Downstream, nullGap builds the explicit gap $H-PHP$ as gauge$_m$ + gauge$_l$ − bilinear, feeding this vector into gaugePart l (·). The main existence theorem exists_nullLorentzTTDecomposition then writes the full null identity
$H=$ TT project $+$ $m$-gauge $+$ $l$-gauge $-$ bilinear $+$ screen-trace,
using this vector for the $l$-gauge summand. Entrywise control appears in nullGap_entry.
Within the Recognition gravity stack this is pure Lorentzian linear algebra for the ledger name edge_tt_decomposition. It does not yet touch Regge edge perturbations, Einstein–Hilbert recovery, or polarization normalizations; those sit further down the campaign chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.