Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Aut(Cn)(Z/nZ)×

Statement

For every n1,

Aut(Cn)(Z/n)×.

If Cn=g, the unit class [a] corresponds to the automorphism gga.

Facts & Assumptions

Given: An integer n1 and a cyclic group Cn=g.

[L1]

A cyclic group whose generator has finite order n is isomorphic to (Z/n,+) (Every cyclic group is isomorphic to (Z,+) or to (Z/n,+) for its finite order n1).

[L2]

A residue class modulo n is a unit exactly when its representative is coprime to n (For n1, [a]n is a unit if and only if gcd(a,n)=1).

[L4]

An automorphism is an isomorphism from a group to itself (Group isomorphisms, automorphisms and the set Aut(G)).

[L6]

The cyclic subgroup generated by g is exactly the set of integer powers of g (g={gn:nZ}, and every cyclic group is abelian).

Proof

technique · direct
1.1

By [L6] every element of Cn is a power gk, and a homomorphism f satisfies f(gk)=f(g)k, so f is determined by f(g); writing f(g)=ga, every endomorphism has the form fa(gk)=gak. By [L3], fa=fb exactly when ab(modn), so the endomorphisms are indexed by the residue classes of Z/n, which [L1] identifies with Cn as an additive group.

L1L3L6algebra
1.2

The element ga generates Cn exactly when gcd(a,n)=1: [L5] gives au+nv=1, hence g=(ga)u, in one direction, while a common divisor greater than one makes every power of ga have exponent divisible by that divisor in the other. Hence fa is an automorphism exactly when [a] is a unit by [L2] and [L4].

L2L3L4L5algebra
2.1

Since fafb=fab, the correspondence [a]fa is a group homomorphism. Steps 1.1 and 1.2 make it bijective, so it is the claimed isomorphism. For n=1, both groups are trivial.

step 1.1step 1.2L4

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 94 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources