def HyperplaneArrangement.reflections {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) : Set (E ≃ᵃⁱ[ℝ] E)

The set of all affine reflections through hyperplanes of arr, viewed as affine isometries $E \simeq^{ai}_\mathbb{R} E$. Each element is the orthogonal reflection $s_h$ across some $h \in arr.hyperplanes$.

noncomputable def HyperplaneArrangement.ReflectionGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) : Subgroup (E ≃ᵃⁱ[ℝ] E)

The reflection group of a hyperplane arrangement: the subgroup of affine isometries $E \simeq^{ai} E$ generated by all reflections through hyperplanes of arr.

def HyperplaneArrangement.walls {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (arr : HyperplaneArrangement E) (C : arr.Chamber) : Set (AffineHyperplane E)

The set of walls of a chamber $C$: those hyperplanes of arr whose carrier contains a relatively open piece of the closure of $C$ (i.e. $η$ satisfies η.IsWall C.set).

def HyperplaneArrangement.wallReflections {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) (C : arr.Chamber) : Set (E ≃ᵃⁱ[ℝ] E)

The set of reflections through the walls of a chamber $C$. These are the Coxeter generators $s_i$ for the Coxeter system attached to the arrangement.

noncomputable def HyperplaneArrangement.WallReflectionGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) (C : arr.Chamber) : Subgroup (E ≃ᵃⁱ[ℝ] E)

The subgroup of $E \simeq^{ai} E$ generated by the wall reflections of $C$. A central theorem (wallReflections_generate_theorem) shows this equals the full ReflectionGroup.

noncomputable def HyperplaneArrangement.coxeterOrder {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (sᵢ sⱼ : E ≃ᵃⁱ[ℝ] E) : ℕ

The Coxeter order $m_{ij}$ of a pair of reflections: the order of the product $s_i s_j$ inside the group of affine isometries. This is the entry of the Coxeter matrix.

def HyperplaneArrangement.CoxeterRelation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (sᵢ sⱼ : E ≃ᵃⁱ[ℝ] E) : Prop

The Coxeter relation $(s_i s_j)^{m_{ij}} = 1$ holds for the pair $(s_i, s_j)$.

def HyperplaneArrangement.separatingHyperplanes {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (arr : HyperplaneArrangement E) (x y : E) : Set (AffineHyperplane E)

The set of hyperplanes of arr that strictly separate two points $x, y$ (i.e. $x$ and $y$ lie in opposite open half-spaces of $η$).

noncomputable def HyperplaneArrangement.galleryDistance {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (arr : HyperplaneArrangement E) (x y : E) : ℕ

The gallery distance between two points $x$ and $y$ is the number of hyperplanes in arr separating them. In a Coxeter arrangement this coincides with the word length of the unique group element sending the chamber of $x$ to that of $y$.

noncomputable def HyperplaneArrangement.chamberGalleryDistance {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (arr : HyperplaneArrangement E) (C D : arr.Chamber) : ℕ

The gallery distance between two chambers $C$ and $D$: the minimum, over $x \in C$ and $y \in D$, of galleryDistance x y. Equivalently the minimum number of walls one must cross in a chamber-to-chamber path.

def HyperplaneArrangement.imageByIsometry {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (w : E ≃ᵃⁱ[ℝ] E) (S : Set E) : Set E

The image of a set $S \subseteq E$ under an affine isometry $w$. A convenience wrapper for w '' S used throughout the development to talk about the action of reflection-group elements on chambers.

def HyperplaneArrangement.ActsOnChambers {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) : Prop

The arrangement acts on its chambers: every element of the reflection group sends each chamber to another chamber.

def HyperplaneArrangement.SimplyTransitive {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) : Prop

The action of the reflection group on chambers is simply transitive: for any pair of chambers $C, D$ there is a unique $w$ with $w(C) = D$. This is the key Coxeter property ensuring chambers are in bijection with group elements.

def HyperplaneArrangement.FundamentalDomain {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) (C : arr.Chamber) : Prop

A chamber $C$ is a fundamental domain for the action of the reflection group on $E$: its translates by group elements cover $E$ (via closures) and distinct translates of the open chamber are disjoint.

def HyperplaneArrangement.IsWordFor {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) (C : arr.Chamber) (word : List (E ≃ᵃⁱ[ℝ] E)) (w : E ≃ᵃⁱ[ℝ] E) : Prop

A word (a list of wall reflections of $C$) expresses the element $w$ if all entries are wall reflections and the list product equals $w$.

noncomputable def HyperplaneArrangement.wordLength {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) (C : arr.Chamber) (w : E ≃ᵃⁱ[ℝ] E) : ℕ

The word length $\ell(w)$ of an element $w$ relative to the chamber $C$: the minimum length of a list of wall reflections of $C$ whose product is $w$. By convention $\ell(w) = 0$ when no such list exists (using $\inf \emptyset = 0$ on $\mathbb{N}$).

def HyperplaneArrangement.LengthEqualsGalleryDistance {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) (C : arr.Chamber) : Prop

Length equals gallery distance: for every element $w$ of the reflection group and every $x \in C$, $\ell(w)$ equals the number of hyperplanes separating $x$ from $w(x)$. This is the hallmark equivalence between algebraic length and geometric distance in a Coxeter system.

def HyperplaneArrangement.DeletionCondition {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) (C : arr.Chamber) : Prop

The Deletion condition (one of the equivalent axioms of a Coxeter system): if a word in wall reflections is non-reduced ($\ell(\prod\text{word}) < |\text{word}|$), then we can delete two of its letters without changing the product.

def HyperplaneArrangement.isotropyGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) (x : E) : Subgroup (E ≃ᵃⁱ[ℝ] E)

The isotropy subgroup of a point $x \in E$ inside the reflection group: those $w$ in $ReflectionGroup$ that fix $x$.

def HyperplaneArrangement.hyperplanesThrough {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (arr : HyperplaneArrangement E) (x : E) : Set (AffineHyperplane E)

The set of hyperplanes of arr containing the point $x$.

def HyperplaneArrangement.reflectionsThrough {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) (x : E) : Set (E ≃ᵃⁱ[ℝ] E)

The set of reflections through hyperplanes containing the point $x$ (i.e. those that fix $x$). Used to describe the isotropy group of $x$.

def HyperplaneArrangement.IsotropyGeneratedByReflections {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) (C : arr.Chamber) : Prop

Stabilizers are generated by reflections: for every point $x$ in the closure of the fundamental chamber, the isotropy subgroup of $x$ equals the subgroup generated by reflections through hyperplanes containing $x$. This is the parabolic-subgroup structure of a Coxeter group.

class HyperplaneArrangement.CoxeterArrangement {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) : Prop

A Coxeter arrangement is a hyperplane arrangement equipped with the package of axioms needed to identify the reflection group as a Coxeter group. The axioms include: reflections permute chambers, are involutions, act transitively (and via wall-reflections) on chambers, are faithful, the closure of one chamber tiles space, distinct translates of the open chamber are disjoint, an Exchange property holds, wall reflections in adjacent chambers are conjugate, length is bounded by gallery distance both above and below, walls of a reduced word fix the right points, a reflection through a wall of $C$ is a wall of any chamber it produces, wall reflections fix points of their carriers, and the dihedral subgroups are locally finite (Cartan integrality).

• reflection_maps_chambers (η : AffineHyperplane E) : η ∈ arr.hyperplanes → ∀ (C : arr.Chamber), ∃ (D : arr.Chamber), D.set = imageByIsometry η.reflectionMap C.set
• reflection_involutive (η : AffineHyperplane E) : η ∈ arr.hyperplanes → η.reflectionMap * η.reflectionMap = 1
• transitive_on_chambers (C D : arr.Chamber) : ∃ (w : ↥arr.ReflectionGroup), imageByIsometry (↑w) C.set = D.set
• transitive_via_wall_reflections (C D : arr.Chamber) : ∃ w ∈ arr.WallReflectionGroup C, imageByIsometry w C.set = D.set
• faithful_on_chambers (C : arr.Chamber) (w : ↥arr.ReflectionGroup) : imageByIsometry (↑w) C.set = C.set → w = ⟨1, ⋯⟩
• closure_covers (C : arr.Chamber) (x : E) : ∃ w ∈ arr.ReflectionGroup, x ∈ imageByIsometry w (closure C.set)
• open_chambers_disjoint (C : arr.Chamber) (w₁ w₂ : ↥arr.ReflectionGroup) : w₁ ≠ w₂ → imageByIsometry (↑w₁) C.set ∩ imageByIsometry (↑w₂) C.set = ∅
• exchange_property (C : arr.Chamber) (s : E ≃ᵃⁱ[ℝ] E) : s ∈ arr.wallReflections C → ∀ (word : List (E ≃ᵃⁱ[ℝ] E)), (∀ t ∈ word, t ∈ arr.wallReflections C) → arr.IsWordFor C word word.prod → arr.wordLength C (s * word.prod) ≤ arr.wordLength C word.prod → ∃ (i : Fin word.length), s * word.prod = (word.eraseIdx ↑i).prod
• wall_reflection_conjugate (C : arr.Chamber) (w : E ≃ᵃⁱ[ℝ] E) : w ∈ arr.WallReflectionGroup C → ∀ (D : arr.Chamber), imageByIsometry w C.set = D.set → ∀ t ∈ arr.wallReflections D, ∃ s ∈ arr.wallReflections C, t = w * s * w⁻¹
• gallery_upper_bound (C : arr.Chamber) (word : List (E ≃ᵃⁱ[ℝ] E)) : (∀ s ∈ word, s ∈ arr.wallReflections C) → ∀ x ∈ C.set, arr.galleryDistance x (word.prod x) ≤ word.length
• gallery_lower_bound (C : arr.Chamber) (w : E ≃ᵃⁱ[ℝ] E) : w ∈ arr.ReflectionGroup → ∀ x ∈ C.set, arr.wordLength C w ≤ arr.galleryDistance x (w x)
• closure_wall_membership (C : arr.Chamber) (s₁ : E ≃ᵃⁱ[ℝ] E) (rest : List (E ≃ᵃⁱ[ℝ] E)) : s₁ ∈ arr.wallReflections C → (∀ t ∈ rest, t ∈ arr.wallReflections C) → arr.wordLength C (s₁ :: rest).prod = (s₁ :: rest).length → ∀ x ∈ closure C.set, (s₁ :: rest).prod x = x → ∃ η ∈ arr.walls C, s₁ = η.reflectionMap ∧ x ∈ η.carrier
• reflection_creates_wall (η : AffineHyperplane E) : η ∈ arr.hyperplanes → ∀ (C D : arr.Chamber), D.set = imageByIsometry η.reflectionMap C.set → η.IsWall D.set
• wall_reflection_fixes_wall_point (η : AffineHyperplane E) : η ∈ arr.hyperplanes → ∀ x ∈ η.carrier, η.reflectionMap x = x
• locally_finite (C : arr.Chamber) (η ζ : AffineHyperplane E) : η ∈ arr.hyperplanes → ζ ∈ arr.hyperplanes → η.IsWall C.set → ζ.IsWall C.set → ∃ (n : ℤ), 2 * inner ℝ (‖η.normal‖⁻¹ • η.normal) (‖ζ.normal‖⁻¹ • ζ.normal) = ↑n

def HyperplaneArrangement.PreservesChambers {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (arr : HyperplaneArrangement E) (w : E ≃ᵃⁱ[ℝ] E) : Prop

An affine isometry $w$ preserves chambers if both $w$ and its inverse send every chamber to a chamber. This is satisfied by every element of the reflection group.

theorem HyperplaneArrangement.simplyTransitive_theorem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {arr : HyperplaneArrangement E} [arr.CoxeterArrangement] : arr.SimplyTransitive

The reflection group acts simply transitively on chambers in a Coxeter arrangement. Existence comes from CoxeterArrangement.transitive_on_chambers; uniqueness uses the faithful_on_chambers axiom to show that $w'^{-1} w$ fixes $C$ setwise, hence equals $1$.

theorem HyperplaneArrangement.fundamentalDomain_theorem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {arr : HyperplaneArrangement E} [arr.CoxeterArrangement] (C : arr.Chamber) : arr.FundamentalDomain C

Every chamber is a fundamental domain of the reflection group in a Coxeter arrangement. Covering follows from closure_covers, disjointness from open_chambers_disjoint.

theorem HyperplaneArrangement.wallReflection_involutive {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {arr : HyperplaneArrangement E} [arr.CoxeterArrangement] (C : arr.Chamber) (s : E ≃ᵃⁱ[ℝ] E) (hs : s ∈ arr.wallReflections C) : s * s = 1

Wall reflections are involutions: $s^2 = 1$ for every $s$ in wallReflections C. This follows immediately from CoxeterArrangement.reflection_involutive once we extract the underlying hyperplane $η$.

theorem HyperplaneArrangement.deletionCondition_theorem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {arr : HyperplaneArrangement E} [arr.CoxeterArrangement] (C : arr.Chamber) : arr.DeletionCondition C

The deletion condition holds: in a Coxeter arrangement, every non-reduced expression in the wall generators admits a deletion of two letters yielding the same product. Proof by induction on the word, applying the Exchange property to find an index $i$ such that $s \cdot \text{rest}.\text{prod} = (\text{rest}.\text{eraseIdx}\,i).\text{prod}$.

theorem HyperplaneArrangement.wallReflections_generate_theorem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {arr : HyperplaneArrangement E} [arr.CoxeterArrangement] (C : arr.Chamber) : arr.WallReflectionGroup C = arr.ReflectionGroup

Wall reflections of any chamber generate the full reflection group: $\langle s_i : s_i \text{ wall of } C\rangle = \text{ReflectionGroup}$. The inclusion $\subseteq$ is immediate; for $\supseteq$ one uses transitivity-via-wall-reflections and the conjugation axiom wall_reflection_conjugate to express each reflection through any hyperplane as a conjugate of some wall reflection by an element of $WallReflectionGroup\,C$.

theorem HyperplaneArrangement.reverse_prod_of_involutions {G : Type u_2} [Group G] (wa : List G) (hinv : ∀ s ∈ wa, s * s = 1) : wa.reverse.prod = wa.prod⁻¹

Reversing a list of involutions inverts its product: if every element $s$ of a list wa satisfies $s^2 = 1$ (so $s = s^{-1}$), then $(\text{wa.reverse}).\text{prod} = (\text{wa.prod}) ^{-1}$. This is the generic group-theoretic fact behind constructing inverse words from generators known to be involutive (such as Coxeter generators).

theorem HyperplaneArrangement.word_exists_for_closure_element {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {arr : HyperplaneArrangement E} [arr.CoxeterArrangement] (C : arr.Chamber) (w : E ≃ᵃⁱ[ℝ] E) (hw : w ∈ arr.WallReflectionGroup C) : ∃ (word : List (E ≃ᵃⁱ[ℝ] E)), (∀ s ∈ word, s ∈ arr.wallReflections C) ∧ word.prod = w

Every element of $WallReflectionGroup C$ is a product of wall reflections of $C$: by Subgroup.closure_induction over generators, identity, multiplication, and inverses. Inverses are handled by reversing the word (using reverse_prod_of_involutions), since each generator is an involution.

theorem HyperplaneArrangement.lengthEqualsGalleryDistance_theorem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {arr : HyperplaneArrangement E} [arr.CoxeterArrangement] (C : arr.Chamber) : arr.LengthEqualsGalleryDistance C

Word length equals gallery distance: for every $w$ in the reflection group and every $x \in C$, $\ell(w) = d_{\text{gallery}}(x, w(x))$. The lower bound comes from gallery_lower_bound; the upper bound from gallery_upper_bound applied to a minimal-length expression of $w$ in wall reflections of $C$.

theorem HyperplaneArrangement.isotropyGeneratedByReflections_theorem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {arr : HyperplaneArrangement E} [arr.CoxeterArrangement] (C : arr.Chamber) : arr.IsotropyGeneratedByReflections C

Isotropy groups are generated by reflections through containing walls (the parabolic subgroup theorem): for each $x$ in the closure of a fundamental chamber, the stabilizer of $x$ in the reflection group equals the subgroup generated by reflections through hyperplanes containing $x$. The forward direction is by strong induction on word length, peeling off a fixing initial wall reflection via closure_wall_membership. The reverse direction is immediate from wall_reflection_fixes_wall_point.

def HyperplaneArrangement.IsCoxeterSystem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (arr : HyperplaneArrangement E) (C : arr.Chamber) : Prop

A hyperplane arrangement $(arr, C)$ forms a Coxeter system (relative to a fundamental chamber $C$) if all five canonical properties hold: simple transitivity, fundamental-domain property, length = gallery distance, deletion condition, and isotropy generated by reflections. The theorems above show every CoxeterArrangement satisfies this conjunction.