LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

Quaternion conjugation and division

Statement

For $h = a + b i + c j + d k \in H$ , define $\overset{ˉ}{h} = a - b i - c j - d k$ and $N (h) = a^{2} + b^{2} + c^{2} + d^{2} \in R$ . Quaternion conjugation is an involution and reverses products, $\overline{h g} = \overset{ˉ}{g} \overset{ˉ}{h}$ . Moreover,

h \overset{ˉ}{h} = \overset{ˉ}{h} h = N (h) 1.

In particular, every nonzero $h$ is invertible, with $h^{- 1} = \overset{ˉ}{h} / N (h)$ , so $H$ is a real division algebra.

Facts & Assumptions

Given: The real quaternion algebra and its basis and multiplication rules from Real, complex, and quaternion coefficient algebras and matrix notation, and real coefficients $a, b, c, d$ .

[F1]

The basis satisfies $i^{2} = j^{2} = k^{2} = - 1$ , $i j = k$ , $j k = i$ , $k i = j$ , and reversed products have opposite sign (Real, complex, and quaternion coefficient algebras and matrix notation).

[F2]

$R$ is an ordered field, so every square is nonnegative and a sum of squares is positive when at least one summand is nonzero (The reals form a totally ordered field).

Proof

technique · direct expansion

1.1givenF1algebra

Conjugation fixes $1$ and negates $i, j, k$ . For an imaginary basis unit $u$ , $\overline{u^{2}} = - 1 = (- u) (- u)$ ; for distinct imaginary units $u, v$ , $u v$ is an imaginary basis unit up to sign and $\overset{ˉ}{v} \overset{ˉ}{u} = v u = - u v = \overline{u v}$ . Bilinearity proves $\overline{h g} = \overset{ˉ}{g} \overset{ˉ}{h}$ for all $h, g$ , and the coordinate formula gives $\overset{ˉ}{\overset{ˉ}{h}} = h$ .

1.2givenF1algebra

Write $h = a + u$ with $u = b i + c j + d k$ . The relations in [F1] give $u^{2} = - (b^{2} + c^{2} + d^{2})$ because each mixed term is a scalar multiple of $i j + j i$ , $i k + k i$ , or $j k + k j$ . Since $a$ is central, $(a + u) (a - u) = (a - u) (a + u) = a^{2} - u^{2} = N (h) 1$ . Thus $h \overset{ˉ}{h} = \overset{ˉ}{h} h = N (h) 1$ .

2.1givenF2step 1.2algebra∎

If $h \neq 0$ , at least one of $a, b, c, d$ is nonzero, so [F2] gives $N (h) > 0$ . Therefore $N (h)^{- 1}$ exists in $R$ , and step 1.2 shows both $h (\overset{ˉ}{h} / N (h)) = 1$ and $(\overset{ˉ}{h} / N (h)) h = 1$ . For $h = 0$ the norm is $0$ and no inverse is asserted.

Depends on

Used by

Dependency tree · two levels

12 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

Jean Gallier, Clifford Algebras, Clifford Groups, and a Generalization of the Quaternions: The Pin and Spin Groups, §1.1 (standard reference, not scraped)
Konstantin Wernli, Lecture Notes on Spin Geometry, §1.4.1 (standard reference, not scraped)