Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16
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.

Q8 is a subgroup of H× with eight elements, and −1 is its only element of order 2

Statement

Let Q8={1,−1,i,−i,j,−j,k,−k}⊆H× be as in The quaternion group Q8={±1,±i,±j,±k} inside the nonzero quaternions. Then:

  1. Q8 is a subgroup of H× and ∣Q8∣=8;
  2. 1 is the only element of order 1, −1 is the only element of order 2, and each of ±i,±j,±k has order 4;
  3. ⟨i⟩={1,i,−1,−i} is a subgroup of order 4 containing −1, and the same holds for ⟨j⟩ and ⟨k⟩.

Facts & Assumptions

Given: The quaternions H, the basis quaternions 1,i,j,k, the real embedding λ↦λ^, the element n=−1^ and the abbreviation −x=nx of The quaternion group Q8={±1,±i,±j,±k} inside the nonzero quaternions and The quaternions H: real quadruples with componentwise addition and an explicit multiplication formula matching the table on 1,i,j,k.

[F1]

Evaluating the multiplication formula of H on the basis quaternions gives i2=j2=k2=−1, ij=k, jk=i, ki=j, ji=−k, kj=−i, ik=−j, together with 1x=x1=x for x∈{1,i,j,k}; and λ^x=xλ^=(λx0,λx1,λx2,λx3) for every real λ (The quaternions H: real quadruples with componentwise addition and an explicit multiplication formula matching the table on 1,i,j,k).

[F2]
[F3]

A nonempty subset H⊆G of a group G is a subgroup exactly when gh−1∈H for all g,h∈H (One-step subgroup test: a nonempty H⊆G is a subgroup iff gh−1∈H for all g,h∈H; the identity and the inverses of H are then those of G, Subgroup).

[F5]

If ord⁡(g)=m with m≥1, then for every integer t one has gt=e if and only if m∣t; the powers g0,…,gm−1 are pairwise distinct; and ⟨g⟩={gs:s<m} has exactly m elements (If ord⁡(g)=n then gk=e iff k is an integer multiple of n, the powers g0,…,gn−1 are distinct, and ⟨g⟩ has exactly n elements; if g has infinite order then gj=gk only for j=k).

Proof

technique · direct
1.1F1F2algebra

The element n=−1^ is central in H and satisfies n2=1. Centrality is the clause λ^x=xλ^ of [F1] with λ=−1; and n2=−1^ −1^, which the same clause evaluates at λ=−1 and x=(−1,0,0,0) to give (1,0,0,0)=1. Hence also −(−x)=n(nx)=n2x=x for every x, multiplication in H being associative by [F2].

2.1step 1.1F1algebra

The eight quaternions listed in Q8 are pairwise distinct, so ∣Q8∣=8. Written out as quadruples they are (±1,0,0,0), (0,±1,0,0), (0,0,±1,0), (0,0,0,±1), and two such quadruples agree only if they agree in every coordinate; since 1≠−1 and 1≠0 in R, no two of the eight agree.

2.2step 1.1F1F2

Q8 is closed under multiplication. Every element of Q8 is εu with u∈{1,i,j,k} and ε∈{1,n}, and for two such elements associativity and the centrality of step 1.1 give (εu)(δv)=(εδ)(uv). Here εδ∈{1,n} because n2=1, and uv∈{±1,±i,±j,±k} by the table in [F1]. Hence (εu)(δv)∈Q8.

3.1step 1.1step 2.2F1

Every element of Q8 has an inverse lying in Q8. From [F1], i(−i)=−(i2)=−(−1)=1 by step 1.1, and likewise j(−j)=k(−k)=1; also 1⋅1=1 and nn=1. So each of 1,−1 is its own inverse and each of ±i,±j,±k has its negative as inverse, all inside Q8.

3.2step 1.1step 2.1F2F4

ord⁡(1)=1 and ord⁡(−1)=2. The identity of Q8 is 1 by [F2], so ord⁡(1)=1 by [F4]. For −1=n we have n≠1 by step 2.1 and n2=1 by step 1.1, so 2 is the least m≥1 with nm=1.

3.3step 1.1step 2.1F1F4F5

Each of ±i,±j,±k has order 4. Write such an element as εu with u∈{i,j,k} and ε∈{1,n}. By step 1.1 and [F1], (εu)2=ε2u2=u2=−1, and (εu)4=((εu)2)2=(−1)2=1. So the order is finite by [F4] and divides 4 by [F5]; it is not 1 because (εu)1=εu≠1 by step 2.1, and not 2 because (εu)2=−1≠1 by step 2.1. The only remaining divisor of 4 is 4.

4.1step 2.1step 2.2step 3.1F3

Q8 is a subgroup of H×. It is nonempty and contained in H×, since none of its eight elements is 0H by step 2.1; and for g,h∈Q8 steps 2.2 and 3.1 give h−1∈Q8 and then gh−1∈Q8, which is the criterion [F3]. With step 2.1 this proves claim 1.

4.2step 2.1step 3.2step 3.3

Claim 2 follows: steps 3.2 and 3.3 assign an order to each of the eight elements of Q8, and among them exactly one has order 1, namely 1, and exactly one has order 2, namely −1.

5.1

⟨i⟩={1,i,−1,−i} has four elements and contains −1. By step 3.3 ord⁡(i)=4, so [F5] gives ⟨i⟩={i0,i1,i2,i3} with these four powers pairwise distinct, and [F6] confirms these are all the integer powers. Evaluating, i0=1, i1=i, i2=−1 by [F1], and i3=i2i=(−1)i=−i by step 1.1. The same computation with j and with k gives ⟨j⟩={1,j,−1,−j} and ⟨k⟩={1,k,−1,−k}, each of order 4 and each containing −1. This is claim 3. [step 1.1, step 3.3, F1, F5, F6] ■

Depends on

Used by

Dependency tree · two levels

53 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