LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Orthogonal-space preliminaries and anisotropic reflections

Statement

Let $V$ be a finite-dimensional real vector space of dimension $n$ , let $B$ be a nondegenerate symmetric bilinear form, and put $Q (v) = B (v, v)$ . A vector $u$ is anisotropic when $Q (u) \neq 0$ ; a subspace $U$ is totally isotropic when $B ∣_{U \times U} = 0$ . Define $O (V, B) = {A \in GL (V) : B (A v, A w) = B (v, w)}$ and $S O (V, B) = {A \in O (V, B) : \det A = 1}$ . For $U \leq V$ , put $U^{⊥} = {v : B (v, U) = 0}$ . Then:

$\dim U^{⊥} = n - \dim U$ , and every totally isotropic $U$ has $\dim U \leq n / 2$ .
Every such $(V, B)$ has a basis of pairwise orthogonal anisotropic vectors.
For $A \in O (V, B)$ , $im (A - I) = \ker (A - I)^{⊥}$ .
For anisotropic $u$ , the map $r_{u} (v) = v - 2 B (v, u) u / Q (u)$ is an orthogonal reflection: it fixes $u^{⊥}$ , sends $u$ to $- u$ , and has determinant $- 1$ .

Facts & Assumptions

Given: The finite-dimensional real quadratic space $(V, B)$ and the definitions in the Statement.

Proof

technique · direct

1.1givenchoosealgebra

If $n > 0$ , $Q$ is not the zero function: otherwise polarization gives $2 B (v, w) = Q (v + w) - Q (v) - Q (w) = 0$ for all $v, w$ , contradicting nondegeneracy. Choose anisotropic $u$ . Since $Q (u) \neq 0$ , $V = R u \oplus u^{⊥}$ ; the restriction of $B$ to $u^{⊥}$ is nondegenerate because a vector orthogonal to $u^{⊥}$ and to $u$ is orthogonal to all of $V$ . Induction on dimension gives an orthogonal anisotropic basis, with the empty basis when $n = 0$ .

1.2givenalgebra

The map $V \to V^{*}$ induced by $B$ is an isomorphism. Restriction $V^{*} \to U^{*}$ is onto because a linear functional on a subspace of a finite-dimensional vector space extends after extending a basis. Therefore $v \mapsto B (v, -) ∣_{U}$ is onto with kernel $U^{⊥}$ , so rank-nullity gives $\dim U^{⊥} = n - \dim U$ . If $U$ is totally isotropic then $U \subseteq U^{⊥}$ , hence $\dim U \leq n - \dim U$ .

2.1givenstep 1.2algebra

If $z \in \ker (A - I)$ and $y = (A - I) x$ , then $B (y, z) = B (A x, z) - B (x, z) = B (x, A^{- 1} z) - B (x, z) = 0$ . Thus $im (A - I) \subseteq \ker (A - I)^{⊥}$ . Both subspaces have dimension $n - \dim \ker (A - I)$ by rank-nullity and step 1.2, so they are equal.

3.1givenalgebra∎

The formula for $r_{u}$ is linear, fixes every vector in $u^{⊥}$ , and gives $r_{u} (u) = - u$ . The orthogonal direct sum $V = R u \oplus u^{⊥}$ therefore shows that $r_{u}$ preserves $B$ and has determinant $- 1$ . It is the reflection in the hyperplane $u^{⊥}$ .

Remarks

No choice axiom is used; the orthogonal basis is obtained by finite-dimensional induction. The moving-space identity in part 3 is valid for every signature.

Used by

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

Eckhard Meinrenken, Lie groups and Clifford algebras, Chapter 1 §4 (standard reference, not scraped)
Jean Gallier, Clifford Algebras, Clifford Groups, and a Generalization of the Quaternions: The Pin and Spin Groups, §1.3 (standard reference, not scraped)