dot
plain-language theorem explainer
Euclidean inner product on real 4-vectors: the sum of componentwise products over Fin 4. The algebraic TT layer cites it for transversality, squared norms, and projectors against a wave covector. The body is the plain finite sum; no lemmas.
Claim. For $a,b:\mathbb{R}^4$ (indexed by $\mathrm{Fin}\,4$), define the Euclidean pairing $a\cdot b:=\sum_{i} a_i b_i\in\mathbb{R}$.
background
The module is the algebraic layer of the QG campaign item edge_tt_decomposition: linear-algebra transverse-traceless structure for symmetric real $4\times 4$ matrices relative to a nonzero Euclidean wave covector on $\mathrm{Fin},4$. Conventions lift the 3D closer (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin; Minkowski/null specialization is deferred.
This dot is the unweighted Euclidean pairing on coordinate 4-vectors. Upstream, Cost.Ndim.Core defines a related weighted sum $\sum_i \alpha_i t_i$ used by logarithmic aggregates; here the weights are absent and the dimension is fixed at four, matching Mat4 and the TT predicates in the same file (IsTransverse, IsTT, transverseProjector, momentumSq).
proof idea
Definition only: expand as the Finset sum $\sum_{i:\mathrm{Fin},4} a_i b_i$. No tactics, no lemmas, no wrapper around the Ndim weighted form.
why it matters
Gives the inner product that makes Euclidean transversality and squared-norm bounds speak in coordinates for the 4D TT decomposition. Downstream cost/Ndim material reuses the same pairing pattern for Cauchy–Schwarz (dot_sq_le_sqNorm_mul), compensatory nonnegativity under $|\alpha|^2\le 1$, and block-reduction identities that collapse $n$-dimensional projectors on 2-sparse slices. In the gravity lane it underwrites IsTT / transverseProjector algebra without claiming Regge EDGE decomposition, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence, or gap-action recovery. Landmark contact is structural (D=3 spatial plus time as Fin 4 indices), not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.