LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

A labeling containing two independent vectors has trivial $S O (3)$ -stabilizer

Statement

For $S \subseteq R^{3}$ , its pointwise $S O (3)$ stabilizer is

${Stab}_{S O (3)} (S) : = {R \in S O (3) : R s = s for every s \in S} .$

Let $u, v \in R^{3}$ be linearly independent and let $S \subseteq R^{3}$ be a nonempty set with $u, v \in S$ . If $R \in S O (3)$ satisfies $R s = s$ for every $s \in S$ , then $R = I_{3}$ .

Equivalently, ${Stab}_{S O (3)} (S) = {I_{3}}$ . The conclusion uses only the two indicated independent vectors; no assumption that $0 \in S$ is made.

Facts & Assumptions

Given: Linearly independent $u, v \in R^{3}$ , a nonempty $S \subseteq R^{3}$ containing $u$ and $v$ , and $R \in S O (3)$ with $R s = s$ for every $s \in S$ .

[L1]

For $R \in S O (3)$ one has $R^{T} R = I_{3}$ and $\det R = 1$ (The orthogonal group $O (3)$ and the rotation group $S O (3)$ ).

[L2]

The cross product is bilinear and alternating and satisfies $⟨ u \times v, w ⟩_{2} = \det [u v w]$ for all $u, v, w$ , where the bracket denotes the matrix whose columns are $u, v, w$ ; and $u \times v$ is orthogonal to $u$ and to $v$ (The cross product is bilinear, alternating, and orthogonal to both factors, The cross product in $R^{3}$ ).

[L3]

Transpose reverses products, $(R a)^{T} = a^{T} R^{T}$ , the determinant is multiplicative, and the matrix $R [u v w] = [R u R v R w]$ has the three image vectors as columns (Transpose is linear and involutive, and $(A B)^{T} = B^{T} A^{T}$ , For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ , Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes).

[L4]

Every vector of a real finite-dimensional vector space has unique coordinates in an ordered basis (A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i < n} λ_{i} v_{i}$ for exactly one $λ : n \to F$ ; those scalars are the coordinates of $x$ in that ordered basis).

[L5]

The Euclidean inner product is positive definite: if $⟨ x, z ⟩_{2} = 0$ for every $z \in R^{3}$ , then $x = 0$ (Real and complex inner product spaces, with the inner product linear in the first argument, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[L6]

For $u, v \in R^{3}$ , $∥ u \times v ∥_{2}^{2} = \det G (u, v)$ is positive exactly when $u, v$ are linearly independent (The squared cross-product norm is the Gram determinant of two vectors).

[L7]

The standard basis of $R^{3}$ spans $R^{3}$ and has three elements (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$ with $F = R$ and $n = 3$ ); by the Steinitz exchange theorem, any linearly independent three-element subset of $R^{3}$ spans it (The Steinitz exchange lemma: if $L \subseteq V$ is linearly independent and $S \subseteq V$ spans $V$ with $S$ finite of size $n$ , then $L$ is finite with $∣ L ∣ = m \leq n$ , and there is $T \subseteq S$ of size $n - m$ such that $L \cup T$ spans $V$ ).

[L8]

For $R \in S O (3)$ , $\det R = 1$ , so $R$ is invertible by the square-matrix determinant criterion (The orthogonal group $O (3)$ and the rotation group $S O (3)$ , A finite square real matrix is invertible if and only if its determinant is nonzero).

Proof

technique · direct

1.1L2L5L6L7givenalgebra

Put $w : = u \times v$ . It is nonzero by [L6]. If $w \in span {u, v}$ , then $w$ is orthogonal to every vector in that span by [L2], hence to itself; positive definiteness [L5] would give $w = 0$ , a contradiction. Thus $w \notin span {u, v}$ . If $α u + β v + γ w = 0$ and $γ \neq 0$ , then $w \in span {u, v}$ ; hence $γ = 0$ , and independence of $u, v$ gives $α = β = 0$ . So $u, v, w$ are linearly independent. By [L7] their three-element set spans $R^{3}$ , hence $(u, v, w)$ is an ordered basis.

2.1step 1.1L1L2L3L5L8algebra

For all $a, b \in R^{3}$ , $⟨ R a, R b ⟩_{2} = (R a)^{T} (R b) = a^{T} R^{T} R b = a^{T} b = ⟨ a, b ⟩_{2}$ , by [L1] and [L3]. Hence for every $z \in R^{3}$ , $⟨ R (u \times v), R z ⟩_{2} = ⟨ u \times v, z ⟩_{2} = \det [u v z]$ by [L2], while $⟨ (R u) \times (R v), R z ⟩_{2} = \det [R u R v R z] = \det ⁣ (R [u v z]) = \det R \det [u v z] = \det [u v z]$ by [L2] and [L3]. Subtracting gives $⟨ R (u \times v) - (R u) \times (R v), R z ⟩_{2} = 0$ for every $z$ . Since $R$ is invertible by [L8], $R z$ ranges over all of $R^{3}$ , so [L5] gives $R (u \times v) = (R u) \times (R v)$ .

3.1step 2.1given

By the defining property of $R$ , $R u = u$ and $R v = v$ ; substituting into step 2.1 gives $R (u \times v) = u \times v$ . Thus $R$ fixes each vector of the basis $(u, v, u \times v)$ of step 1.1.

4.1step 1.1step 3.1L4givenalgebra∎

Let $x \in R^{3}$ ; by [L4] write $x = c_{1} u + c_{2} v + c_{3} (u \times v)$ with unique real coefficients. By linearity of $R$ and step 3.1, $R x = c_{1} R u + c_{2} R v + c_{3} R (u \times v) = c_{1} u + c_{2} v + c_{3} (u \times v) = x$ . Since $x$ was arbitrary, $R = I_{3}$ .

A labeling containing two independent vectors has trivial $S O (3)$ -stabilizer

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

A labeling containing two independent vectors has trivial SO(3)SO(3)-stabilizer

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

A labeling containing two independent vectors has trivial $S O (3)$ -stabilizer