Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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.

For k≥3, (Z/2kZ)×≅C2×C2k−2, generated uniquely as (−1)ε5j

Statement

For every k≥3,

(Z/2k)×≅C2×C2k−2.

More precisely, every unit has a unique representation (−1)ε5j with ε∈{0,1} and j modulo 2k−2.

Facts & Assumptions

Given: An integer k≥3.

[L1]

The class of 5 has order 2k−2 modulo 2k (For k≥3, the class of 5 has order 2k−2 modulo 2k).

[L3]

A direct product of finite groups has the product of their orders (For finite groups G and H, ∣G×H∣=∣G∣ ∣H∣).

[L4]

The units modulo 2k are the classes represented by odd integers (For n≥1, [a]n is a unit if and only if gcd⁡(a,n)=1).

[L5]

Multiplication modulo 2k is commutative and restricts to the unit group (The unit group (Z/n)× and Euler's totient φ(n)=∣(Z/n)×∣ for n≥1).

[L6]

A bijective group homomorphism is a group isomorphism (Group isomorphisms, automorphisms and the set Aut⁡(G)).

Proof

technique · direct
1.1L1algebra

The class of −1 has order 2, and [L1] gives order 2k−2 for 5.

1.2algebra

Every power of 5 is 1 modulo 4, whereas −1 is 3 modulo 4; hence ⟨−1⟩∩⟨5⟩={1}.

2.1step 1.1step 1.2L4L5

The map C2×C2k−2→(Z/2k)× given by (ε,j)↦(−1)ε5j is a homomorphism by [L5], and step 1.2 makes it injective.

3.1step 2.1L2L3

Its domain has 2k−1 elements by [L3], equal to the size of the target by [L2]; thus it is bijective.

4.1step 3.1L6∎

By [L6] the map is an isomorphism, and its bijectivity is exactly the asserted unique representation.

Depends on

Used by

Dependency tree · two levels

33 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