minkowskiDot
plain-language theorem explainer
Defines the Minkowski pairing of two covectors on Fin 4 with signature (−,+,+,+): η(a,b) = −a₀b₀ + a₁b₁ + a₂b₂ + a₃b₃. Anyone working the Lorentzian edge TT layer cites it as the basic inner product that decides null vs non-null wave covectors and feeds transversality and metric-trace. The body is a four-term arithmetic expression, not a derived lemma.
Claim. For covectors $a,b \in \mathbb{R}^4$ (indices on $\mathrm{Fin}\,4$), the Minkowski pairing is $\eta(a,b) := -a_0 b_0 + a_1 b_1 + a_2 b_2 + a_3 b_3$, i.e. $\eta^{ij} a_i b_j$ in signature $(-\!+,+,+)$.
background
This module is the Lorentzian algebraic layer of the QG campaign lane edge_tt_decomposition: transverse-traceless splitting of symmetric $4\times 4$ real matrices against a Minkowski wave covector, including the null case. Conventions fix signature $(-!+,+,+)$, covectors lowered by default, and index raising that negates the time component.
The pairing here is the basic bilinear form on covectors. Module text equates it to $\sum_j a_j,(\mathrm{raise},b)j$. Sibling notions built on the same metric include the metric-trace $\eta^{ij}H{ij}$ and Lorentz transversality (contraction of the second index of $H$ against the raised wave covector).
Upstream, Metric is only a re-export of the ILG metric-tensor type, and the Euclidean trace on 3D symmetric tensors is the spatial ancestor of the Lorentzian metric-trace; neither supplies the four-term formula, which is fixed by the signature convention of this file.
proof idea
Definitional, not a proof. The right-hand side is the expanded $\eta^{\mu\nu}a_\mu b_\nu$ in coordinates: one minus sign on the time–time product and plus signs on the three spatial products. No lemmas are applied; later results rewrite with this name via simp or direct unfolding.
why it matters
This is the primitive inner product for the whole Lorentzian TT stack. Non-null decomposition theorems (exists_lorentzTTDecomposition, primed variant) gate on $\eta(m,m)\neq 0$; the null theorem (exists_nullLorentzTTDecomposition) requires $\eta(m,m)=\eta(l,l)=0$ and $\eta(m,l)\neq 0$. Gauge constructions (gaugeVector, gaugeCorrected_transverse, load identities) divide by $\eta(m,m)$ or contract loads against $m$ through this pairing. The zero-wave sanity check decomposition_hypothesis_fails_at_zero is literally $\neg(\eta(0,0)\neq 0)$.
In the Recognition gravity program this is pure Lorentzian linear algebra supporting the ledger name edge_tt_decomposition. It does not itself recover Einstein–Hilbert action or close gap-action recovery; it only supplies the pairing those algebraic TT identities need. Framework landmarks T0–T8 and the J-cost RCL are not invoked here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.