ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 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.

Reflection matrices in a positive plane, a Lorentzian plane, and a plane with radical

Example

Let $B$ be a symmetric bilinear form on a real vector space $V$ and let $a \in V$ with $B (a, a) \neq 0$ . Define $r_{a} (v) : = v - 2 B (v, a) a / B (a, a)$ , using the same formula as The real Coxeter form, its radical, reflections, and form-preserving maps. Step 1.1 below proves directly that this is a linear involution preserving $B$ and fixing $\ker B (-, a)$ pointwise for this general $B$ . In the three cases take $V = R^{2}$ , whose functions have domain ${0, 1}$ (The vector space $F^{X}$ of all functions $X \to F$ with pointwise operations, and $F^{n}$ as the case $X = n = {0, 1, \dots, n - 1}$ ), and relabel coordinates by $x_{1} : = x (0)$ , $x_{2} : = x (1)$ and standard unit vectors by $e_{1}, e_{2}$ , respectively (The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ ). Each matrix is taken in the ordered basis $(e_{1}, e_{2})$ ; inertia is as in Positive and negative definiteness, the inertia $(p, q, r)$ , rank $p + q$ , and signature $p - q$ of a real symmetric bilinear or quadratic form.

(i) Positive plane. $B$ the dot product, $a = \frac{3}{5} e_{1} + \frac{4}{5} e_{2}$ , so $B (a, a) = 1$ . Then $r_{a} (e_{1}) = \frac{7}{25} e_{1} - \frac{24}{25} e_{2}$ , $r_{a} (e_{2}) = - \frac{24}{25} e_{1} - \frac{7}{25} e_{2}$ , i.e. $[r_{a}] = \frac{1}{25} (\begin{array}{cc} 7 & - 24 \\ - 24 & - 7 \end{array}), [r_{a}]^{2} = I_{2}, \det [r_{a}] = - 1,$ and $B$ has inertia $(2, 0, 0)$ : a Euclidean reflection across the line $R (- 4 e_{1} + 3 e_{2})$ .

(ii) Lorentzian plane. $B (x, y) = x_{1} y_{1} - x_{2} y_{2}$ , of inertia $(1, 1, 0)$ , and $a = 2 e_{1} + e_{2}$ , so $B (a, a) = 3$ . Then $r_{a} (e_{1}) = - \frac{5}{3} e_{1} - \frac{4}{3} e_{2}$ , $r_{a} (e_{2}) = \frac{4}{3} e_{1} + \frac{5}{3} e_{2}$ , i.e. $[r_{a}] = \frac{1}{3} (\begin{array}{cc} - 5 & 4 \\ - 4 & 5 \end{array}), [r_{a}]^{2} = I_{2}, \det [r_{a}] = - 1,$ and $[r_{a}]$ preserves $B$ : $B (r_{a} e_{1}, r_{a} e_{1}) = 1$ , $B (r_{a} e_{2}, r_{a} e_{2}) = - 1$ , $B (r_{a} e_{1}, r_{a} e_{2}) = 0$ .

(iii) Plane with radical. $B (x, y) = x_{1} y_{1}$ , of inertia $(1, 0, 1)$ and radical $rad (B) = R e_{2}$ (The matrix, left and right radicals, rank, and nondegeneracy of a bilinear form on a finite-dimensional space), and $a = e_{1}$ : then $r_{a} = d i a g (- 1, 1)$ , i.e. $r_{a} (e_{1}) = - e_{1}$ and $r_{a} (e_{2}) = e_{2}$ , with fixed hyperplane $\ker B (-, e_{1}) = R e_{2} = rad (B)$ . The vector $e_{2}$ is $B$ -null, so the displayed formula does not define a reflection with normal $e_{2}$ .

Facts & Assumptions

Given: $V = R^{2}$ with its ordered standard basis $e_{1}, e_{2}$ , a symmetric bilinear form $B$ on $V$ , and $a \in V$ with $B (a, a) \neq 0$ ; $r_{a} (v) : = v - \frac{2 B (v, a)}{B (a, a)} a$ , using the formula of The real Coxeter form, its radical, reflections, and form-preserving maps, and all matrices below are taken in the basis $(e_{1}, e_{2})$ .

[F1]

The reflection $r_{a}$ is defined only for $B (a, a) \neq 0$ ; the radical is the set of $u$ with $B (u, v) = 0$ for every $v$ , and the inertia of a form presented by a diagonal matrix with $p$ positive, $q$ negative and $r$ zero diagonal entries is $(p, q, r)$ (The real Coxeter form, its radical, reflections, and form-preserving maps, The matrix, left and right radicals, rank, and nondegeneracy of a bilinear form on a finite-dimensional space, Positive and negative definiteness, the inertia $(p, q, r)$ , rank $p + q$ , and signature $p - q$ of a real symmetric bilinear or quadratic form).

[F2]

A symmetric bilinear form is linear in each variable and satisfies $B (u, v) = B (v, u)$ (Bilinear forms, and symmetric, skew-symmetric, and alternating bilinear forms).

[F3]

$R^{2}$ is the function space on ${0, 1}$ ; with the relabelling $x_{1} = x (0)$ , $x_{2} = x (1)$ and standard unit vectors $e_{1}, e_{2}$ , one has $x = x_{1} e_{1} + x_{2} e_{2}$ (The vector space $F^{X}$ of all functions $X \to F$ with pointwise operations, and $F^{n}$ as the case $X = n = {0, 1, \dots, n - 1}$ , The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ ).

[F4]

$R$ is an ordered field, so the elementary arithmetic of the fractions below is the field arithmetic of $R$ ; in particular $2 \cdot \frac{1}{2} = 1$ and $\frac{2}{3} \cdot 3 = 2$ (The reals form a totally ordered field).

Verification

1.1givenF1F2F4algebra

General reflection identities. Put $d : = B (a, a) \neq 0$ . Bilinearity makes $r_{a}$ linear, gives $B (r_{a} (v), a) = - B (v, a)$ , and hence $r_{a}^{2} (v) = v$ . The formula gives $r_{a} (a) = - a$ and fixes every $v$ with $B (v, a) = 0$ ; conversely $r_{a} (v) = v$ forces $B (v, a) = 0$ , since $a \neq 0$ and $2 / d \neq 0$ . Finally, symmetry and bilinearity give $B (r_{a} (u), r_{a} (v)) = B (u, v) - 4 B (u, a) B (v, a) / d + 4 B (u, a) B (v, a) / d = B (u, v)$ . Thus the algebraic identities hold for every symmetric $B$ , without requiring it to be a Coxeter form.

2.1givenF1F2F3F4step 1.1algebra

Positive plane. Take $B$ the dot product, so $B (e_{1}, e_{1}) = B (e_{2}, e_{2}) = 1$ and $B (e_{1}, e_{2}) = 0$ , and take $a = \frac{3}{5} e_{1} + \frac{4}{5} e_{2}$ , for which $B (a, a) = \frac{9}{25} + \frac{16}{25} = 1$ . Here $B (e_{1}, a) = \frac{3}{5}$ and $B (e_{2}, a) = \frac{4}{5}$ , so $r_{a} (e_{1}) = e_{1} - \frac{6}{5} a = \frac{7}{25} e_{1} - \frac{24}{25} e_{2}, r_{a} (e_{2}) = e_{2} - \frac{8}{5} a = - \frac{24}{25} e_{1} - \frac{7}{25} e_{2},$ giving $[r_{a}] = \frac{1}{25} (\begin{array}{cc} 7 & - 24 \\ - 24 & - 7 \end{array})$ . Squaring, $[r_{a}]^{2} = \frac{1}{625} (\begin{array}{cc} 625 & 0 \\ 0 & 625 \end{array}) = I_{2}$ , and $\det [r_{a}] = \frac{- 49 - (- 24) (- 24)}{625} = \frac{- 625}{625} = - 1$ . The dot product has inertia $(2, 0, 0)$ and $r_{a}$ fixes $\ker B (-, a) = {x : \frac{3}{5} x_{1} + \frac{4}{5} x_{2} = 0} = R (- 4 e_{1} + 3 e_{2})$ pointwise, the Euclidean reflection across that line.

2.2givenF1F2F3F4step 1.1algebra

Lorentzian plane. Take $B (x, y) = x_{1} y_{1} - x_{2} y_{2}$ , of inertia $(1, 1, 0)$ , and $a = 2 e_{1} + e_{2}$ , so $B (a, a) = 4 - 1 = 3$ , $B (e_{1}, a) = 2$ and $B (e_{2}, a) = - 1$ . Then $r_{a} (e_{1}) = e_{1} - \frac{4}{3} a = - \frac{5}{3} e_{1} - \frac{4}{3} e_{2}, r_{a} (e_{2}) = e_{2} + \frac{2}{3} a = \frac{4}{3} e_{1} + \frac{5}{3} e_{2},$ so $[r_{a}] = \frac{1}{3} (\begin{array}{cc} - 5 & 4 \\ - 4 & 5 \end{array})$ , whose square is $\frac{1}{9} (\begin{array}{cc} 9 & 0 \\ 0 & 9 \end{array}) = I_{2}$ and whose determinant is $\frac{- 25 + 16}{9} = - 1$ . The invariance identities hold on the basis: $B (r_{a} e_{1}, r_{a} e_{1}) = \frac{25}{9} - \frac{16}{9} = 1$ , $B (r_{a} e_{2}, r_{a} e_{2}) = \frac{16}{9} - \frac{25}{9} = - 1$ , and $B (r_{a} e_{1}, r_{a} e_{2}) = - \frac{20}{9} + \frac{20}{9} = 0$ , so $[r_{a}]$ preserves $B$ by bilinearity.

2.3givenF1F2F3F4step 1.1algebra

Plane with radical. Take $B (x, y) = x_{1} y_{1}$ , whose matrix $diag (1, 0)$ has inertia $(1, 0, 1)$ and whose radical is ${u : u_{1} v_{1} = 0 for all v} = R e_{2}$ , and take $a = e_{1}$ , so $B (a, a) = 1$ and $r_{a} (v) = v - 2 v_{1} e_{1}$ . Hence $r_{a} (e_{1}) = - e_{1}$ and $r_{a} (e_{2}) = e_{2}$ , that is $r_{a} = diag (- 1, 1)$ , and its fixed hyperplane is $\ker B (-, e_{1}) = {v : v_{1} = 0} = R e_{2} = rad (B)$ . The vector $e_{2}$ is $B$ -null, $B (e_{2}, e_{2}) = 0$ , so the displayed formula assigns it no reflection.

3.1givenF1F2step 1.1step 2.1step 2.2step 2.3∎

Conclusion. In each of the three cases $a$ satisfies $B (a, a) \neq 0$ and the displayed matrix is $[r_{a}]$ in the ordered basis $(e_{1}, e_{2})$ : an involution with determinant $- 1$ in the two nondegenerate cases, with the inertia readings $(2, 0, 0)$ and $(1, 1, 0)$ of the form and the fixed hyperplane $\ker B (-, a)$ computed above, and in the degenerate case the fixed hyperplane coincides with the radical $R e_{2}$ . These explicit numbers verify the general identities proved in step 1.1 and display why the hypothesis $B (a, a) \neq 0$ of [F1] is exactly what the definition of $r_{a}$ requires: the null vector $e_{2}$ of the last case is a normal for which no reflection is defined by the displayed formula.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

55 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

Michael W. Davis, The Geometry and Topology of Coxeter Groups (Princeton University Press; author's full institutional PDF) (standard reference, not scraped)
Anders Björner and Francesco Brenti, Combinatorics of Coxeter Groups (Graduate Texts in Mathematics 231, Springer 2005) (standard reference, not scraped)