Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-07-31
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.

(Z/8)×={[1],[3],[5],[7]} is not cyclic because every element squares to [1]

Example

(Z/8)×={[1]8,[3]8,[5]8,[7]8}

is not cyclic: every element has square [1]8.

Facts & Assumptions

Given: The unit group (Z/8)×.

[L3]

Natural powers in a group satisfy g0=e and g2=gg (Powers gn: natural exponents in a monoid and integer exponents in a group, with g0=e).

[F1]

Equality of residue classes is congruence of representatives (The congruence class [a]n and the quotient set Z/n), and congruence means divisibility of their difference (Congruence modulo an integer: a≡b(modn) when n∣(a−b), including the moduli 0 and 1).

Verification

technique · direct
1.1

The odd standard representatives 1,3,5,7 are precisely those coprime to 8, giving the displayed unit group by [L1].

L1
1.2

Their squares are 12=1, 32=9≡1, 52=25≡1, and 72=49≡1(mod8). Hence every element has order at most 2.

L3F1
2.1

The group has cardinality 4 by step 1.1, but no element has order 4 by step 1.2. Therefore no element generates it, and [L2] shows that it is not cyclic.

step 1.1step 1.2L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

52 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