dot_div_sqrt_ne_one_of_linearIndependent
plain-language theorem explainer
Two linearly independent vectors in R^3 cannot have normalized dot product equal to 1. Anyone proving that geometric dihedral cosines sit strictly inside (-1,1) from face-normal independence cites this. The proof maps to EuclideanSpace, applies the classical cosine-equals-one characterization, and recovers a scalar multiple that contradicts linear independence.
Claim. If $u,v\in\mathbb{R}^3$ are linearly independent over $\mathbb{R}$, then $\dfrac{u\cdot v}{\sqrt{(u\cdot u)(v\cdot v)}}\neq 1$.
background
The module supplies the strict-interior step for the Regge closure program: two linearly independent adjacent face normals have normalized dot product strictly between $-1$ and $1$. Once that holds, arccos endpoint inputs can be dropped from downstream calculus.
Coordinate vectors live as maps Fin 3 → ℝ. The map toEuclidean3 sends them into Mathlib's EuclideanSpace, where the standard inner product and norm are available. Sibling lemmas identify the coordinate dot product with that inner product (inner_toEuclidean3) and rewrite the geometric denominator as a product of Euclidean norms (sqrt_dot_self_mul_self_eq_norm_mul_norm). Scalar multiples transfer back by smul_of_toEuclidean3_smul.
The classical fact used upstream is that the normalized real inner product equals $1$ if and only if both vectors are nonzero and one is a positive real multiple of the other.
proof idea
Assume the normalized coordinate dot equals $1$. Transport via inner_toEuclidean3 and sqrt_dot_self_mul_self_eq_norm_mul_norm to obtain the same equality for toEuclidean3 u and toEuclidean3 v. Apply Mathlib's real_inner_div_norm_mul_norm_eq_one_iff to conclude both Euclidean images are nonzero and toEuclidean3 v = r • toEuclidean3 u for some $r>0$. Nonzeroness of $u$ follows by unfolding toEuclidean3. Pull the scalar relation back with smul_of_toEuclidean3_smul, then contradict LinearIndependent.pair_iff' on the pair $(u,v)$.
why it matters
This is one half of the analytic core of the module (the twin rules out normalized dot $-1$). The sole direct consumer is geometricDihedralCos_strict_interior_of_faceNormals_independent, which packages both endpoint exclusions into $-1 < \mathrm{geometricDihedralCos},T,e < 1$ whenever adjacent face normals are linearly independent.
That strict interior is the geometric input the Regge closure program needs so dihedral angles stay away from the flat and folded extremes once face-normal independence is known. The module keeps the remaining reduction (independence of adjacent face normals from the AffineIndependent field of a realized tetrahedron) explicit; this lemma removes the cosine-endpoint burden from that chain once independence is in hand. It is pure Euclidean 3-geometry and does not itself invoke the forcing chain, RCL, or $\varphi$-ladder landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.