raise
plain-language theorem explainer
Index raising on four-vectors for the mostly-plus Minkowski metric: the time component flips sign and the three spatial components are left alone. Anyone writing Lorentz-transverse or TT conditions on symmetric 4×4 matrices cites it as the sharp map m ↦ m♯. The body is a one-line piecewise definition on Fin 4.
Claim. For a covector $v \in \mathbb{R}^{4}$ (indices on $\mathrm{Fin}\,4$), the raised vector $v^{\sharp}$ is defined by $(v^{\sharp})^{0} = -v_{0}$ and $(v^{\sharp})^{i} = v_{i}$ for spatial $i \in \{1,2,3\}$, i.e. index raising with respect to $\eta = \mathrm{diag}(-1,+1,+1,+1)$.
background
The module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1). It specializes the Euclidean TT layer to symmetric real $4\times 4$ matrices against a Minkowski wave covector, including the null case. Signature is $(-,+,+,+)$; covectors are lowered by default.
Index raising is the only place the metric signature enters the linear algebra: it converts a lowered wave covector $m$ into the raised object used in contractions. The Minkowski pairing of covectors is then $\sum_{j} a_{j},(m^{\sharp})^{j}$, and the Lorentz load of a matrix $H$ is $(H\cdot m^{\sharp}){i} = \sum{j} H_{ij},(m^{\sharp})^{j}$. Lorentz transversality is the vanishing of that load.
Sibling primitives in the same file (Minkowski dot, Minkowski trace, gauge part, outer square) all route through this raise map so that every subsequent TT identity is written once in raised form.
proof idea
Pure definition: on $\mathrm{Fin},4$, return $-v_{0}$ when the index is $0$ and $v_{i}$ otherwise. No lemmas, no tactics.
why it matters
This is the metric-signature hook for the whole Lorentzian TT stack. Downstream, lorentzLoad is defined as the contraction of $H$ against raise m; the expansion identity lorentzLoad_eq, the gauge-part load formula, and the identity-matrix load all unfold through it. The counterexample that the Euclidean projector fails Lorentz transversality on the null axis also evaluates the load via raise.
In the Recognition gravity program this sits inside the ledger name edge_tt_decomposition: the algebraic TT split of symmetric edge perturbations before any continuum or Regge limit. It does not itself close gap-action recovery or EH convergence; it only supplies the correct $(-,+,+,+)$ raising so those later steps can quote a Lorentz-transverse remainder. Outside gravity it is reused in cosmology rung-descent bookkeeping that needs the same four-vector raise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.