LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-10-08

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Moved space of a reversed reflection product with independent normals

Statement

Let $(V, ⟨ \cdot, \cdot ⟩)$ be a finite-dimensional real inner-product space, let $k \geq 0$ , and let $σ_{1}, \dots, σ_{k} \in V$ be linearly independent unit vectors (Real and complex inner-product spaces and their induced length, Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i < n} λ_{i} v_{i} = 0_{V}$ forces every $λ_{i} = 0_{F}$ , and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent, For a subspace $W$ of a finite-dimensional inner product space, $V = W \oplus W^{⊥}$ ). For a unit vector $v$ define the orthogonal reflection $R (v) x : = x - 2 ⟨ x, v ⟩ v .$ For a linear map $A : V \to V$ write $M (A) : = im (A - {i d}_{V})$ (Linear map between vector spaces over the same field, Kernel and image of a linear map). Then:

(1) The moved space. $M (R (σ_{k}) R (σ_{k - 1}) \dots R (σ_{1})) = span (σ_{1}, \dots, σ_{k}),$ and its dimension is $k$ . When $k = 0$ , the product is the identity, the span of the empty set is ${0}$ , and the moved space is ${0}$ .

(2) Reflection length. For a finite-type Coxeter system, specialize the inner-product space of (1) to $V = R^{S}$ with Coxeter form $B$ (The real Coxeter form, its radical, reflections, and form-preserving maps); this is positive definite by Finiteness criterion: W is finite exactly when the Coxeter form is positive definite. Let $ρ$ be the canonical reflection homomorphism and $T$ the reflection set (The canonical reflection homomorphism, roots, reflections, and the positive cone, Reflection length, the absolute order on a finite Coxeter group, and the moved and fixed spaces of an orthogonal operator). If $σ_{1}, \dots, σ_{k}$ are roots, choose any $r_{i} \in T$ with $ρ (r_{i}) = R (σ_{i})$ ; such reflections exist by Descent of the reflection representation, unit root norms, and conjugation of reflections (3),(4). Then $ℓ_{T} (r_{k} r_{k - 1} \dots r_{1}) = \dim M (R (σ_{k}) \dots R (σ_{1})) = k .$ The product order is the reverse of the root list, as in The Brady-Watt ordered root complex X(c), its subcomplexes X(sigma) and X(sigma,rho), and their positive-cone realizations (1),(2): the reflection with normal $σ_{1}$ acts first on vectors when applying the product.

(3) Limits. Clause (1) needs only linear independence and unit norms; the normals need not lie in a common open half-space and no Coxeter complex is needed. Clause (2) uses finite type so that the Coxeter form is a positive definite inner product. No crystallographic assumption or Choice is used.

Facts & Assumptions

Given: A finite-dimensional real inner-product space and a finite list of linearly independent unit vectors; for clause (2), a finite-type Coxeter system, its canonical reflection representation and roots.

[F1]

In a finite-dimensional inner-product space, $V = U \oplus U^{⊥}$ for every subspace $U$ (For a subspace $W$ of a finite-dimensional inner product space, $V = W \oplus W^{⊥}$ ). If a linear map sends $U$ into itself and is injective on finite-dimensional $U$ , it is onto $U$ by rank-nullity (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

[F2]

For a unit vector $v$ , the displayed formula gives $R (v) x - x = - 2 ⟨ x, v ⟩ v$ , so $R (v) - i d$ has image $span (v)$ (take $x = v$ ) and $R (v)$ fixes $v^{⊥}$ . Also $⟨ R (v) x, v ⟩ = - ⟨ x, v ⟩$ , whence $R (v)^{2} = i d$ , and expanding $⟨ R (v) x, R (v) y ⟩$ gives $⟨ x, y ⟩$ because $⟨ v, v ⟩ = 1$ . Thus it is an orthogonal reflection.

[F3]

For finite-type $W$ , the Coxeter form is positive definite and $ρ (W)$ preserves it. Every root has unit norm, and for every $t \in T$ its operator $ρ (t)$ is the reflection $R (α)$ for a root $α$ (Finiteness criterion: W is finite exactly when the Coxeter form is positive definite, Descent of the reflection representation, unit root norms, and conjugation of reflections (2)–(4)).

[F4]

The reflection length $ℓ_{T} (g)$ is the least number of factors from $T$ in a factorization of $g$ (Reflection length, the absolute order on a finite Coxeter group, and the moved and fixed spaces of an orthogonal operator (1)).

[F5]

The list of independent vectors $σ_{1}, \dots, σ_{k}$ is a basis of its span $U$ , so $\dim U = k$ by the definition of dimension (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis).

Proof

technique · show that the product fixes exactly the orthogonal complement of the span, then use a rank bound for products of reflections

Given: The data in the Statement. For clause (1), put $U = span (σ_{1}, \dots, σ_{k})$ and $A = R (σ_{k}) \dots R (σ_{1})$ .

1.1F1F2F5algebra

(Moved space of the product.) If $k = 0$ , then $A = {i d}_{V}$ and $M (A) = {0} = U$ . Otherwise each $R (σ_{i})$ sends $U$ into $U$ and fixes $U^{⊥}$ pointwise, so $A (U) \subseteq U$ , $A$ fixes $U^{⊥}$ , and $M (A) \subseteq U$ . To prove the reverse inclusion, let $x \in U$ satisfy $A x = x$ , set $x_{0} = x$ , and for $i = 1, \dots, k$ set $x_{i} = R (σ_{i}) x_{i - 1}$ . Then $x_{k} = A x = x_{0}$ , so $0 = x_{k} - x_{0} = \sum_{i = 1}^{k} (x_{i} - x_{i - 1}) = - 2 \sum_{i = 1}^{k} ⟨ x_{i - 1}, σ_{i} ⟩ σ_{i} .$ Linear independence forces every coefficient to vanish. Thus $x_{i} = x_{i - 1}$ for every $i$ , and each reflection fixes $x$ ; hence $x ⊥ σ_{i}$ for every $i$ . Since $x \in U$ , this gives $x \in U \cap U^{⊥} = {0}$ . Therefore $(A - i d) ∣_{U} : U \to U$ is injective, and rank-nullity makes it surjective. Thus $U \subseteq M (A)$ , so $M (A) = U$ and $\dim M (A) = k$ by [F5].

2.1F3F4step 1.1algebra∎

(Reflection-length rank bound.) Assume the finite-type hypotheses of clause (2) and let $g = r_{k} \dots r_{1}$ , so $ρ (g) = A$ by [F3]. For any two invertible linear maps $X, Y$ , $X Y - i d = (X - i d) + X (Y - i d),$ hence $M (X Y) \subseteq M (X) + X M (Y)$ and $\dim M (X Y) \leq \dim M (X) + \dim M (Y)$ because $X$ is invertible. Iterating this inequality, any factorization of $g$ into $m$ elements of $T$ gives $\dim M (ρ (g)) \leq m$ , since each image under $ρ$ is an orthogonal reflection with one-dimensional moved space by [F3]. Step 1.1 gives $\dim M (ρ (g)) = k$ , so every reflection factorization has at least $k$ factors. The displayed factorization $g = r_{k} \dots r_{1}$ has exactly $k$ , and therefore $ℓ_{T} (g) = k$ , including the empty-product case.

Depends on

Used by

Dependency tree · two levels

98 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

T. Brady and C. Watt, Lattices in Finite Real Reflection Groups, Transactions of the American Mathematical Society 360 (2008), 4809–4844, arXiv:math/0501502 (standard reference, not scraped)