dotProduct_self_nonneg
plain-language theorem explainer
Any real 3-vector has nonnegative squared Euclidean length under the Mathlib dot product. Geometers working the tetrahedral dihedral cosine cite it to keep the geometric denominator square nonnegative. The proof unfolds the sum definition and applies nonnegativity of squares termwise.
Claim. For every real vector $v \in \mathbb{R}^3$, the Euclidean dot product satisfies $0 \le v \cdot v$.
background
The module builds the Euclidean side of the tetrahedral dihedral cosine: face normals via cross products of edge vectors, then the normalized inner product of two adjacent face normals. That cosine is the geometric counterpart of a Cayley-Menger cofactor ratio (Berger's formula), still to be identified in this file.
The Mathlib dot product on Fin 3 → ℝ is the sum of coordinatewise products. Squared length $v \cdot v$ therefore expands as $\sum_i v_i^2$. Nonnegativity of that sum is the elementary fact recorded here; it is used immediately for the product of two such squared lengths that appears as the geometric denominator square of the dihedral cosine.
proof idea
Term-mode proof. Unfold dotProduct to the finite sum $\sum_i v_i v_i$. Apply Finset.sum_nonneg with the pointwise witness mul_self_nonneg (v i), which is $v_i^2 \ge 0$ for each coordinate. No geometry-specific lemmas are needed.
why it matters
Feeds geometricDihedralDenomSq_nonneg, which states that the geometric denominator square of the dihedral cosine on a realized tetrahedron is nonnegative. That denominator is the product of the two face-normal squared lengths, so nonnegativity of $v \cdot v$ is applied twice.
In the broader Recognition geometry stack this keeps the geometric cosine well-defined as a real number before it is matched to the Cayley-Menger cofactor ratio (the Berger cofactor target of the module). It is pure Euclidean bookkeeping, not a forcing-chain step, but it closes a positivity obligation on the geometric side of that identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.