abs_dot_div_sqrt_self_mul_self_le_one
plain-language theorem explainer
Normalized coordinate-vector dot products in R^3 have absolute value at most 1. Anyone bounding geometric dihedral cosines (face-normal inner products) cites this. The proof transports Fin 3 coordinate vectors into EuclideanSpace and applies the standard Cauchy–Schwarz form |⟨U,V⟩|/(‖U‖‖V‖) ≤ 1.
Claim. For any coordinate vectors $u,v:\{0,1,2\}\to\mathbb{R}$, $$\left|\frac{u\cdot v}{\sqrt{(u\cdot u)(v\cdot v)}}\right|\le 1.$$
background
This module builds the Euclidean geometric side of the tetrahedral dihedral cosine: face normals via cross products, then the normalized inner product of two adjacent face normals. The target is the Berger cofactor formula, equating that geometric cosine with a Cayley–Menger cofactor ratio.
Here $u$ and $v$ are plain Fin 3 → ℝ coordinate vectors (the ambient model for face normals and edge vectors). The expression is the usual cosine of the angle between them, written with the Mathlib dot product ⬝ᵥ. The only analytic input needed is that this normalized product stays in $[-1,1]$, including degenerate cases handled by the real square root and absolute value.
proof idea
Transport both coordinate vectors into EuclideanSpace ℝ (Fin 3) via the standard equivalence. Three short calculations identify the coordinate dot product with the Euclidean inner product and the self-dots with squared norms. The denominator square root then equals ‖U‖ * ‖V‖. After rewriting, the claim is exactly Mathlib’s abs_real_inner_div_norm_mul_norm_le_one.
why it matters
Feeds geometricDihedralCos_range, which states that geometric dihedral cosines of a realized tetrahedron lie in $[-1,1]$. That range fact is the sanity bound on the geometric side of the Berger cofactor identification: once the cofactor ratio equals this normalized face-normal product, it automatically inherits the cosine interval. Without this lemma the geometric cosine is only a formal quotient; with it, the quotient is a genuine cosine candidate for matching against the Cayley–Menger side in DihedralCayleyMenger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.