theorem AffineCoxeter.cor_affine_coxeter_similitude {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (φ : SimplicialComplexIso A.complex A'.complex) (f : E →ᵃ[ℝ] E') (hf_compat : ∀ (v : A.V), f (A.vertexMap v) = A'.vertexMap (φ.toMorphism.toFun v)) : ∃ μ > 0, (∀ (x y : E), euclideanDist (f x) (f y) = μ * euclideanDist x y) ∧ A'.chamberDiameter = μ * A.chamberDiameter

Corollary: any simplicial isomorphism between affine Coxeter complexes that lifts to an affine map of the ambient Euclidean spaces is a similitude with scaling factor $\mu > 0$ matching the ratio of chamber diameters.

theorem AffineCoxeter.cor_affine_coxeter_isometry_normalized {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (φ : SimplicialComplexIso A.complex A'.complex) (f : E →ᵃ[ℝ] E') (hf_compat : ∀ (v : A.V), f (A.vertexMap v) = A'.vertexMap (φ.toMorphism.toFun v)) (x y : E) : normalizedDist A' (f x) (f y) = normalizedDist A x y

Corollary: after normalizing each Euclidean metric by the chamber diameter, the simplicial isomorphism becomes a true isometry: $d_{A'}(f x, f y) = d_A(x, y)$.