toEuclidean3_smul
plain-language theorem explainer
Scalar homogeneity for the coordinate-to-Euclidean embedding on $\mathbb{R}^3$: scaling a Fin-3 vector then embedding equals embedding then scaling. Cited wherever face normals or edge vectors are renormalized inside the affine-independence interior argument. Proof is definition unfold plus simp through the EuclideanSpace equivalence.
Claim. For every real scalar $r$ and every coordinate vector $u:\mathrm{Fin}\,3\to\mathbb{R}$, the Euclidean $\ell^2$ image of $r\cdot u$ equals $r$ times the Euclidean $\ell^2$ image of $u$.
background
The module supplies the strict-interior step for the Regge closure program: two linearly independent adjacent face normals have normalized dot product strictly in $(-1,1)$, so arccos endpoints drop out of downstream calculus. Coordinate vectors live as Fin 3 → ℝ; Mathlib's inner-product API wants EuclideanSpace ℝ (Fin 3).
The bridge is toEuclidean3, which views a coordinate vector as the Euclidean $\ell^2$ vector via the standard EuclideanSpace.equiv symmetry. Homogeneity of that bridge is the elementary algebraic fact needed before norms, normalized dots, and face-normal independence lemmas can move scalars freely.
proof idea
Term-mode proof by unfolding toEuclidean3 and running simp. The definition is the inverse of EuclideanSpace.equiv, which is linear, so scalar multiplication passes through automatically; no extra lemmas are named.
why it matters
Sits in the geometry layer that feeds Regge closure: once adjacent face normals are independent, normalized dots stay strictly inside $(-1,1)$ and the strict dihedral interior follows. Homogeneity lets later lemmas (norm squares, normalized dots, cross-product nonvanishing) pull real scales out of the embedding without re-proving linearity each time.
No recorded downstream users yet in the graph; siblings such as norm_toEuclidean3_sq, inner_toEuclidean3, and the adjacent-face-normal independence statements are the natural consumers. Framework role is local Euclidean bookkeeping for tetrahedral face geometry, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.