ExampleConstruction: AI-adaptedVerification: 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.

Finite checks of the cover: the half-turn rotations $ρ (\pm i), ρ (\pm j), ρ (\pm k)$ , the identity $ρ (i) ρ (j) = ρ (i j)$ , and the exact preimages of $ρ (k)$

Example

Let $e_{1}, e_{2}, e_{3}$ be the standard basis of $R^{3}$ and identify $R^{3}$ with $Im H$ through $φ$ as in The quaternion rotation map $ρ$ : conjugation on the imaginary quaternions, the unit sphere $S^{3}$ , and quaternion lifts; matrices of linear maps are taken in the ordered basis $(i, j, k)$ . Then:

$ρ (1)$ is the identity matrix and $ρ (- 1) = ρ (1)$ ; moreover, if $q \in S^{3}$ satisfies $ρ (q) = I_{3}$ , then $q = \pm 1$ .
$ρ (i), ρ (j), ρ (k)$ are the half-turns about the coordinate axes,

$ρ (i) = (\begin{array}{ccc} 1 & 0 & 0 \\ 0 & - 1 & 0 \\ 0 & 0 & - 1 \end{array}), ρ (j) = (\begin{array}{ccc} - 1 & 0 & 0 \\ 0 & 1 & 0 \\ 0 & 0 & - 1 \end{array}), ρ (k) = (\begin{array}{ccc} - 1 & 0 & 0 \\ 0 & - 1 & 0 \\ 0 & 0 & 1 \end{array}),$

and $ρ (i) ρ (j) = ρ (k) = ρ (i j)$ : the homomorphism identity is verified on the generating pair $i, j$ by finite matrix multiplication. 3. The exact preimages of $ρ (k)$ in $S^{3}$ are $\pm k$ : $ρ (\pm k) = ρ (k)$ , and every $q \in S^{3}$ with $ρ (q) = ρ (k)$ satisfies $q = \pm k$ .

Facts & Assumptions

Given: The basis $(i, j, k)$ of $Im H$ and the map $ρ$ of The quaternion rotation map $ρ$ : conjugation on the imaginary quaternions, the unit sphere $S^{3}$ , and quaternion lifts.

[L1]

For $N (q) = 1$ and $q = \cos (θ / 2) + φ (\hat{n}) \sin (θ / 2)$ with $∥ \hat{n} ∥_{2} = 1$ one has $ρ (q) (φ (z)) = φ (\cos θ z + (1 - \cos θ) ⟨ \hat{n}, z ⟩_{2} \hat{n} + \sin θ (\hat{n} \times z))$ (The product rule for quaternion and matrix curves, multiplicativity of the quaternion norm, and the conjugation formula $q φ (v) \overset{ˉ}{q} = φ ((a^{2} - ∥ u ∥^{2}) v + 2 ⟨ u, v ⟩ u + 2 a (u \times v))$ clause 4).

[L2]

The quaternion product table is $i^{2} = j^{2} = k^{2} = - 1$ , $i j = k$ , $j i = - k$ ; $N (s + φ (w)) = s^{2} + ∥ w ∥_{2}^{2}$ , so $N (i) = N (j) = N (k) = 1$ , $k^{- 1} = - k$ , and $N (k^{- 1}) = 1$ . Also $S^{3} = {q : N (q) = 1}$ , $q \overset{ˉ}{q} = \overset{ˉ}{q} q = \hat{N (q)}$ , and $N (p q) = N (p) N (q)$ (The quaternions $H$ : real quadruples with componentwise addition and an explicit multiplication formula matching the table on $1, i, j, k$ , $H$ is a division ring that is not commutative, hence not a field: $q^{- 1} = \overset{ˉ}{q} / N (q)$ for $q \neq 0$ , while $i j = k$ and $j i = - k$ , The product rule for quaternion and matrix curves, multiplicativity of the quaternion norm, and the conjugation formula $q φ (v) \overset{ˉ}{q} = φ ((a^{2} - ∥ u ∥^{2}) v + 2 ⟨ u, v ⟩ u + 2 a (u \times v))$ clause 2).

[L3]

$ρ (- p) = ρ (p)$ for $p \in S^{3}$ , $ρ (1)$ is the identity map, the map $p \mapsto ρ (p)$ is a homomorphism on $S^{3}$ , and its kernel is ${1, - 1}$ (The quaternion rotation map $ρ$ : conjugation on the imaginary quaternions, the unit sphere $S^{3}$ , and quaternion lifts Definition and Remark).

[L4]

The cross product is bilinear, $e_{2} \times e_{1} = - e_{3}$ , and $⟨ e_{2}, e_{1} ⟩_{2} = 0$ ; the Euclidean inner product is the coordinate dot product (The cross product in $R^{3}$ , The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[L5]

Matrix multiplication is associative with identity $I_{3}$ , and the entries of a product are $(A B)_{s r} = \sum_{t} A_{s t} B_{t r}$ (Matrix multiplication is associative, unital, distributive, and compatible with scalar multiplication, Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes).

[L6]

The quarter-turn values are $\cos π = - 1$ and $\sin π = 0$ , while the shift formulas give $\cos (π / 2) = 0$ and $\sin (π / 2) = 1$ (Quarter-turn values and shifts by pi/2 and pi).

Verification

technique · direct; evaluate the axis-angle formula at $\theta=\pi$, then multiply two explicit matrices and compare preimages through the kernel

1.1L1L3L4L6algebra

For $a = 1, 2, 3$ , applying [L1] with $θ = π$ , $\hat{n} = e_{a}$ and $q = φ (e_{a}) = \cos (π / 2) + φ (e_{a}) \sin (π / 2)$ gives $ρ (φ (e_{a})) (φ (z)) = φ (- z + 2 ⟨ e_{a}, z ⟩_{2} e_{a})$ using [L6]; its cross-product term vanishes because $\sin π = 0$ . In the basis $(i, j, k)$ this is the diagonal matrix with entry $+ 1$ in position $a$ and $- 1$ elsewhere, which is the displayed $ρ (i), ρ (j), ρ (k)$ . Also $ρ (1)$ is the identity map by [L3], and $ρ (- 1) = ρ (1)$ by [L3], so both real unit quaternions act trivially.

2.1step 1.1L5algebra

Multiplying the two displayed matrices with the entry formula of [L5] gives $ρ (i) ρ (j) = diag (- 1, - 1, 1) = ρ (k)$ ; explicitly, the product of two diagonal matrices multiplies corresponding diagonal entries, $(1) (- 1) = - 1$ , $(- 1) (1) = - 1$ , $(- 1) (- 1) = 1$ .

2.2step 1.1L2L3algebra

If $q \in S^{3}$ satisfies $ρ (q) = ρ (k)$ , then by the homomorphism and kernel facts of [L3] the element $q k^{- 1} \in S^{3}$ (unit because $N (q k^{- 1}) = N (q) N (k^{- 1}) = 1$ by [L2]) satisfies $ρ (q k^{- 1}) = ρ (q) ρ (k)^{- 1} = I_{3}$ , hence $q k^{- 1} \in {1, - 1}$ and $q = \pm k$ ; conversely $ρ (\pm k) = ρ (k)$ by [L3] and step 1.1. In the special case $ρ (q) = I_{3}$ the same argument with $k$ replaced by $1$ gives $q = \pm 1$ .

3.1step 2.1step 2.2L2algebra∎

Finally $i j = k$ by [L2], so $ρ (i j) = ρ (k) = ρ (i) ρ (j)$ by [step 2.1]: the homomorphism identity holds on the pair generating the quaternion group. This proves clauses 2 and 3 and completes the finite checks.

Remarks

The matrices display the two-to-one cover concretely: the identity rotation has the two preimages $\pm 1$ , and the half-turn about $e_{3}$ has the two preimages $\pm k$ , in agreement with the general kernel statement. The example checks specific rotations only; it is not a proof that the covering is nontrivial along loops, which is the separate closed-loop counterexample on this page.
The computation verifies the homomorphism identity on the generators $i, j$ of the quaternion group; it does not reprove the homomorphism property for all pairs, which is supplied by the cited cover.

Finite checks of the cover: the half-turn rotations $ρ (\pm i), ρ (\pm j), ρ (\pm k)$ , the identity $ρ (i) ρ (j) = ρ (i j)$ , and the exact preimages of $ρ (k)$

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources

Finite checks of the cover: the half-turn rotations ρ(±i),ρ(±j),ρ(±k)ρ(±i),ρ(±j),ρ(±k), the identity ρ(i)ρ(j)=ρ(ij)ρ(i)ρ(j)=ρ(ij), and the exact preimages of ρ(k)ρ(k)

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources

Finite checks of the cover: the half-turn rotations $ρ (\pm i), ρ (\pm j), ρ (\pm k)$ , the identity $ρ (i) ρ (j) = ρ (i j)$ , and the exact preimages of $ρ (k)$