def AffineCoxeter.IsSimilitude {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E'] (f : E → E') (d₁ : E → E → ℝ) (d₂ : E' → E' → ℝ) : Prop

A map $f : E \to E'$ is a similitude with respect to distances $d_1, d_2$ if there exists a uniform scale factor $\mu$ with $d_2(f(x), f(y)) = \mu \cdot d_1(x, y)$.

def AffineCoxeter.euclideanDist {E : Type u_1} [NormedAddCommGroup E] (x y : E) : ℝ

The Euclidean distance on an inner-product space: $d(x, y) = \|x - y\|$.

def AffineCoxeter.IsWInvariant {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (d : E → E → ℝ) : Prop

A distance function is $W$-invariant if every element of the affine reflection group acts as an isometry.

theorem AffineCoxeter.euclideanDist_isWInvariant {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) : IsWInvariant W euclideanDist

The Euclidean distance is invariant under any affine reflection group, since each element is an affine isometry.

structure AffineCoxeter.SimplicialComplexIso {V : Type u_2} {W : Type u_3} [DecidableEq V] [DecidableEq W] (K : SimplicialComplex V) (L : SimplicialComplex W) : Type (max u_2 u_3)

An isomorphism of simplicial complexes: a pair of mutually inverse morphisms between $K$ and $L$.

• toMorphism : K.Morphism L
• invMorphism : L.Morphism K
• left_inv (v : V) : self.invMorphism.toFun (self.toMorphism.toFun v) = v
• right_inv (w : W) : self.toMorphism.toFun (self.invMorphism.toFun w) = w

structure AffineCoxeter.AffineCoxeterComplex (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Type (max u_2 (u_3 + 1))

The structure of an abstract affine Coxeter complex in $E$: an abstract simplicial complex on vertices $V$ with a labelling, an affine vertex map onto a spanning subset, a chosen chamber diameter, a Coxeter matrix and normal basis with Gram matrix encoding the local Coxeter data, and the bijection between chamber adjacencies and Coxeter exponents.

• V : Type u_3
• decEq : DecidableEq self.V
• W : AffineReflectionGroup E
• complex : SimplicialComplex self.V
• vertexMap : self.V → E
• affineSpan_vertexMap_eq_top : affineSpan ℝ (Set.range self.vertexMap) = ⊤
• chamberDiameter : ℝ
• chamberDiameter_pos : self.chamberDiameter > 0
• n : ℕ
• normalBasis : Module.Basis (Fin self.n) ℝ E
• coxeterMatrix : Fin self.n → Fin self.n → ℕ
• coxeterGram : Fin self.n → Fin self.n → ℝ
• coxeterGram_of_coxeterMatrix (i j : Fin self.n) : self.coxeterGram i j = -Real.cos (Real.pi / ↑(self.coxeterMatrix i j))
• normalBasis_inner (i j : Fin self.n) : inner ℝ (self.normalBasis i) (self.normalBasis j) = self.coxeterGram i j
• chamber_card (C : Finset self.V) : self.complex.IsMaximal C → C.card = self.n + 1
• exists_chamber : ∃ (C : Finset self.V), self.complex.IsMaximal C
• vertexType : self.V → Fin (self.n + 1)
• vertexType_chamber_bijective (C : Finset self.V) : self.complex.IsMaximal C → ∀ (t : Fin (self.n + 1)), ∃! v : self.V, v ∈ C ∧ self.vertexType v = t
• coxeterMatrix_eq_chamberCount (C : Finset self.V) : self.complex.IsMaximal C → ∀ (i j : Fin self.n), {D : Finset self.V | self.complex.IsMaximal D ∧ {v ∈ C | self.vertexType v ≠ i.castSucc ∧ self.vertexType v ≠ j.castSucc} ⊆ D}.ncard = 2 * self.coxeterMatrix i j
• chamberCount_finite (C : Finset self.V) : self.complex.IsMaximal C → ∀ (i j : Fin self.n), {D : Finset self.V | self.complex.IsMaximal D ∧ {v ∈ C | self.vertexType v ≠ i.castSucc ∧ self.vertexType v ≠ j.castSucc} ⊆ D}.Finite
• vertex_in_chamber (v : self.V) : ∃ (C : Finset self.V), self.complex.IsMaximal C ∧ v ∈ C

noncomputable def AffineCoxeter.normalizedDist {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : AffineCoxeterComplex E) (x y : E) : ℝ

The canonical normalised distance on an affine Coxeter complex: the Euclidean distance scaled so that every closed chamber has diameter $1$.

theorem AffineCoxeter.AffineCoxeterComplex.nonempty_V {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : AffineCoxeterComplex E) : Nonempty A.V

The vertex type $V$ of an affine Coxeter complex is nonempty, since otherwise the affine span condition forces $\mathbb{R}^0 = \top$, a contradiction.

theorem AffineCoxeter.inner_preservation_from_gram_matching {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} {E' : Type u_2} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (b : Module.Basis (Fin n) ℝ E) (b' : Module.Basis (Fin n) ℝ E') (hgram : ∀ (i j : Fin n), inner ℝ (b' i) (b' j) = inner ℝ (b i) (b j)) (Ψ : E →ₗ[ℝ] E') (hΨ : ∀ (i : Fin n), Ψ (b i) = b' i) (x y : E) : inner ℝ (Ψ x) (Ψ y) = inner ℝ x y

A linear map that sends one basis to another with matching Gram matrices preserves the inner product on all of $E$.

theorem AffineCoxeter.norm_of_inner_preserving_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (Ψ : E →ₗ[ℝ] E') (h : ∀ (x y : E), inner ℝ (Ψ x) (Ψ y) = inner ℝ x y) (v : E) : ‖Ψ v‖ = ‖v‖

A linear map that preserves the inner product also preserves the norm.

theorem AffineCoxeter.SimplicialComplexIso.injective {V' : Type u_2} {W' : Type u_3} [DecidableEq V'] [DecidableEq W'] {K : SimplicialComplex V'} {L : SimplicialComplex W'} (φ : SimplicialComplexIso K L) : Function.Injective φ.toMorphism.toFun

The forward morphism of a simplicial complex isomorphism is injective.

def AffineCoxeter.SimplicialComplexIso.symm {V' : Type u_2} {W' : Type u_3} [DecidableEq V'] [DecidableEq W'] {K : SimplicialComplex V'} {L : SimplicialComplex W'} (φ : SimplicialComplexIso K L) : SimplicialComplexIso L K

The inverse of a simplicial complex isomorphism, obtained by swapping forward and backward morphisms.

theorem AffineCoxeter.SimplicialComplexIso.maps_maximal {V' : Type u_2} {W' : Type u_3} [DecidableEq V'] [DecidableEq W'] {K : SimplicialComplex V'} {L : SimplicialComplex W'} (φ : SimplicialComplexIso K L) (C : Finset V') (hC : K.IsMaximal C) : L.IsMaximal (Finset.image φ.toMorphism.toFun C)

Simplicial isomorphisms preserve maximal faces (chambers).

theorem AffineCoxeter.coxeter_iso_dim_eq {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (φ : SimplicialComplexIso A.complex A'.complex) : A.n = A'.n

An isomorphism of affine Coxeter complexes implies their ranks (dimensions) are equal.

theorem AffineCoxeter.AffineCoxeterComplex.gallery_connected {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : AffineCoxeterComplex E) (C D : Finset A.V) (hC : A.complex.IsMaximal C) (hD : A.complex.IsMaximal D) : ∃ (k : ℕ) (gallery : Fin (k + 1) → Finset A.V), gallery ⟨0, ⋯⟩ = C ∧ gallery ⟨k, ⋯⟩ = D ∧ (∀ (i : Fin k), A.complex.IsMaximal (gallery i.castSucc)) ∧ A.complex.IsMaximal (gallery ⟨k, ⋯⟩) ∧ ∀ (i : Fin k), (gallery i.castSucc ∩ gallery i.succ).card = A.n

Gallery connectivity of an affine Coxeter complex: any two chambers are connected by a sequence of adjacent chambers (gallery) of common-face dimension $n$.

theorem AffineCoxeter.AffineCoxeterComplex.labeling_agrees_on_some_chamber {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : AffineCoxeterComplex E) (τ : A.V → Fin (A.n + 1)) (hτ : ∀ (C : Finset A.V), A.complex.IsMaximal C → ∀ (t : Fin (A.n + 1)), ∃! v : A.V, v ∈ C ∧ τ v = t) : ∃ (C₀ : Finset A.V), A.complex.IsMaximal C₀ ∧ ∀ v ∈ C₀, τ v = A.vertexType v

Existence of a chamber where two compatible labellings agree: a useful "seed" for spreading agreement of labellings across chambers via gallery connectivity.

theorem AffineCoxeter.vertex_type_unique {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : AffineCoxeterComplex E) (τ : A.V → Fin (A.n + 1)) (hτ : ∀ (C : Finset A.V), A.complex.IsMaximal C → ∀ (t : Fin (A.n + 1)), ∃! v : A.V, v ∈ C ∧ τ v = t) (v : A.V) : τ v = A.vertexType v

Uniqueness of the vertex type labelling: any labelling satisfying the chamber-bijection property must agree with $A.\text{vertexType}$ on every vertex.

theorem AffineCoxeter.iso_preserves_vertex_type {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (φ : SimplicialComplexIso A.complex A'.complex) (hn : A.n = A'.n) (v : A.V) : A'.vertexType (φ.toMorphism.toFun v) = Fin.cast ⋯ (A.vertexType v)

An isomorphism of affine Coxeter complexes preserves the vertex type labelling (up to the canonical reindexing $\text{Fin.cast}$).

theorem AffineCoxeter.iso_chamber_count_preserved {V' : Type u_2} {W' : Type u_3} [DecidableEq V'] [DecidableEq W'] {K : SimplicialComplex V'} {L : SimplicialComplex W'} (φ : SimplicialComplexIso K L) (F : Finset V') : {D : Finset W' | L.IsMaximal D ∧ Finset.image φ.toMorphism.toFun F ⊆ D}.ncard = {C : Finset V' | K.IsMaximal C ∧ F ⊆ C}.ncard

An isomorphism preserves the number of chambers containing a given face.

theorem AffineCoxeter.coxeter_matrix_iso_preserved {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (φ : SimplicialComplexIso A.complex A'.complex) (hn : A.n = A'.n) (i j : Fin A.n) : A.coxeterMatrix i j = A'.coxeterMatrix (Fin.cast hn i) (Fin.cast hn j)

An isomorphism of affine Coxeter complexes preserves the Coxeter matrix: $m_{ij}$ is the same combinatorial datum on either side.

theorem AffineCoxeter.coxeter_iso_gram_eq {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (φ : SimplicialComplexIso A.complex A'.complex) (hn : A.n = A'.n) (i j : Fin A.n) : A.coxeterGram i j = A'.coxeterGram (Fin.cast hn i) (Fin.cast hn j)

Since an isomorphism preserves the Coxeter matrix and the Gram matrix $G_{ij} = -\cos(\pi/m_{ij})$ is determined by $m_{ij}$, isomorphic affine Coxeter complexes have equal Gram matrices (up to the dimension reindexing).

theorem AffineCoxeter.psi_induces_vertex_compatible_iso {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (hn : A.n = A'.n) (Ψ : E →ₗ[ℝ] E') (hΨ : ∀ (i : Fin A.n), Ψ (A.normalBasis i) = A'.normalBasis (Fin.cast hn i)) : ∃ (Ψ_star : SimplicialComplexIso A.complex A'.complex), ∀ (u w : A.V), (A'.chamberDiameter / A.chamberDiameter) • Ψ (A.vertexMap u - A.vertexMap w) = A'.vertexMap (Ψ_star.toMorphism.toFun u) - A'.vertexMap (Ψ_star.toMorphism.toFun w)

Existence half: a linear map $\Psi$ sending the normal basis of $A$ to the normal basis of $A'$ induces some simplicial isomorphism $\Psi^*$ that, after rescaling by the diameter ratio, agrees with $\Psi$ on vertex differences.

theorem AffineCoxeter.uniqueness_lemma_psi_star_eq_phi {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (φ : SimplicialComplexIso A.complex A'.complex) (hn : A.n = A'.n) (Ψ : E →ₗ[ℝ] E') (hΨ : ∀ (i : Fin A.n), Ψ (A.normalBasis i) = A'.normalBasis (Fin.cast hn i)) (Ψ_star : SimplicialComplexIso A.complex A'.complex) (hcompat : ∀ (u w : A.V), (A'.chamberDiameter / A.chamberDiameter) • Ψ (A.vertexMap u - A.vertexMap w) = A'.vertexMap (Ψ_star.toMorphism.toFun u) - A'.vertexMap (Ψ_star.toMorphism.toFun w)) (v : A.V) : Ψ_star.toMorphism.toFun v = φ.toMorphism.toFun v

Uniqueness half: any simplicial isomorphism $\Psi^*$ inducing the diameter-scaled $\Psi$ on vertex differences must coincide with the given $\varphi$ on vertices.

theorem AffineCoxeter.psi_scaled_compatible_on_vertex_differences {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (φ : SimplicialComplexIso A.complex A'.complex) (hn : A.n = A'.n) (Ψ : E →ₗ[ℝ] E') (hΨ : ∀ (i : Fin A.n), Ψ (A.normalBasis i) = A'.normalBasis (Fin.cast hn i)) (u w : A.V) : (A'.chamberDiameter / A.chamberDiameter) • Ψ (A.vertexMap u - A.vertexMap w) = A'.vertexMap (φ.toMorphism.toFun u) - A'.vertexMap (φ.toMorphism.toFun w)

Combining existence and uniqueness: for any basis-matching $\Psi$, the diameter ratio $A'.\mathrm{chamberDiameter} / A.\mathrm{chamberDiameter}$ times $\Psi$ acts on vertex differences of $A$ as $\varphi$ acts on the corresponding vertices of $A'$.

theorem AffineCoxeter.psi_scaled_agrees_with_phi_on_vertices {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (φ : SimplicialComplexIso A.complex A'.complex) (hn : A.n = A'.n) (Ψ : E →ₗ[ℝ] E') (hΨ : ∀ (i : Fin A.n), Ψ (A.normalBasis i) = A'.normalBasis (Fin.cast hn i)) : ∃ (t : E'), ∀ (v : A.V), (A'.chamberDiameter / A.chamberDiameter) • Ψ (A.vertexMap v) = A'.vertexMap (φ.toMorphism.toFun v) + t

Translating from vertex differences to vertices: there is a translation vector $t \in E'$ such that the diameter-scaled $\Psi$ on vertices equals $\varphi$ on vertices plus $t$.

theorem AffineCoxeter.coxeter_iso_vertex_compat {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (φ : SimplicialComplexIso A.complex A'.complex) (hn : A.n = A'.n) (Ψ : E →ₗ[ℝ] E') (hΨ : ∀ (i : Fin A.n), Ψ (A.normalBasis i) = A'.normalBasis (Fin.cast hn i)) (u w : A.V) : Ψ (A.vertexMap u - A.vertexMap w) = (A.chamberDiameter / A'.chamberDiameter) • (A'.vertexMap (φ.toMorphism.toFun u) - A'.vertexMap (φ.toMorphism.toFun w))

Inverse form of the vertex-difference compatibility: the unscaled $\Psi$ on vertex differences equals $(A.\mathrm{chamberDiameter}/A'.\mathrm{chamberDiameter})$ times the image under $\varphi$.

theorem AffineCoxeter.coxeter_iso_basis_compatible {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (φ : SimplicialComplexIso A.complex A'.complex) : ∃ (hn : A.n = A'.n) (Ψ : E →ₗ[ℝ] E'), (∀ (i : Fin A.n), Ψ (A.normalBasis i) = A'.normalBasis (Fin.cast hn i)) ∧ (∀ (i j : Fin A.n), inner ℝ (A'.normalBasis (Fin.cast hn i)) (A'.normalBasis (Fin.cast hn j)) = inner ℝ (A.normalBasis i) (A.normalBasis j)) ∧ ∀ (u w : A.V), Ψ (A.vertexMap u - A.vertexMap w) = (A.chamberDiameter / A'.chamberDiameter) • (A'.vertexMap (φ.toMorphism.toFun u) - A'.vertexMap (φ.toMorphism.toFun w))

Existence of a basis-and-vertex-compatible linear map: given an iso $\varphi$ of affine Coxeter complexes, there is a linear map $\Psi : E \to E'$ that maps the normal basis of $A$ to the normal basis of $A'$, preserves the Gram matrix, and satisfies the diameter-scaled vertex compatibility.

theorem AffineCoxeter.coxeter_iso_scaled_linear_map {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (φ : SimplicialComplexIso A.complex A'.complex) : ∃ (Φ : E →ₗ[ℝ] E'), (∀ (v : E), ‖Φ v‖ = A'.chamberDiameter / A.chamberDiameter * ‖v‖) ∧ ∀ (u w : A.V), Φ (A.vertexMap u - A.vertexMap w) = A'.vertexMap (φ.toMorphism.toFun u) - A'.vertexMap (φ.toMorphism.toFun w)

From an iso $\varphi$ one produces a scaled linear map $\Phi : E \to E'$ that multiplies every norm by the diameter ratio $A'.\mathrm{chamberDiameter}/A.\mathrm{chamberDiameter}$ and sends vertex differences in $A$ to the corresponding vertex differences in $A'$.

theorem AffineCoxeter.coxeter_iso_induces_vertex_compatible_similitude {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (φ : SimplicialComplexIso A.complex A'.complex) : ∃ (g : E →ᵃ[ℝ] E'), (∀ (x y : E), euclideanDist (g x) (g y) = A'.chamberDiameter / A.chamberDiameter * euclideanDist x y) ∧ ∀ (v : A.V), g (A.vertexMap v) = A'.vertexMap (φ.toMorphism.toFun v)

Promoting the scaled linear map to an affine map: there exists an affine map $g : E \to E'$ that is a similitude with factor the diameter ratio, and that restricts to $\varphi$ on the vertices.

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

Stronger packaged form: from $\varphi$ we extract an affine similitude $g$ with explicit similitude factor $\mu > 0$ satisfying $A'.\mathrm{chamberDiameter} = \mu \cdot A.\mathrm{chamberDiameter}$ and $g \circ A.\mathrm{vertexMap} = A'.\mathrm{vertexMap} \circ \varphi$.

theorem AffineCoxeter.vertex_compatible_map_unique {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeterComplex E) (A' : AffineCoxeterComplex E') (φ : SimplicialComplexIso A.complex A'.complex) (f g : E →ᵃ[ℝ] E') (hf : ∀ (v : A.V), f (A.vertexMap v) = A'.vertexMap (φ.toMorphism.toFun v)) (hg : ∀ (v : A.V), g (A.vertexMap v) = A'.vertexMap (φ.toMorphism.toFun v)) : f = g

Uniqueness of the affine extension: two affine maps that agree with $\varphi$ on the vertex set $\mathrm{range}(A.\mathrm{vertexMap})$ agree everywhere, because the vertex set affinely spans $E$.

theorem AffineCoxeter.simplicial_iso_is_similitude_with_diameter {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

Main quantitative form: any affine map $f$ extending $\varphi$ on the vertex set is a similitude with factor $\mu$, where $A'.\mathrm{chamberDiameter} = \mu \cdot A.\mathrm{chamberDiameter}$.

theorem AffineCoxeter.simplicial_iso_is_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)) : IsSimilitude (⇑f) euclideanDist euclideanDist

Qualitative form: any affine extension $f$ of $\varphi$ is a similitude with respect to the Euclidean distances.

noncomputable def AffineCoxeter.canonicalDist {E : Type u_1} [NormedAddCommGroup E] (chamberDiam : ℝ) (_hD : chamberDiam > 0) (x y : E) : ℝ

The canonical distance: Euclidean distance divided by the chamber diameter, so that each chamber has diameter exactly $1$.

theorem AffineCoxeter.normalizedDist_isWInvariant {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : AffineCoxeterComplex E) : IsWInvariant A.W (normalizedDist A)

The Weyl-group-invariance of the Euclidean distance descends to its rescaling $d/\mathrm{chamberDiameter}$.

theorem AffineCoxeter.canonical_metric_isometry {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

The canonical (chamber-diameter-normalized) metric is an isometry invariant of the simplicial structure: any affine map $f$ extending an iso $\varphi$ preserves the normalized Euclidean distance. This is the main result of Section 13.7.