Alphabeta Math
LemmaStatement: 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.

For k≥3, the class of 5 has order 2k−2 modulo 2k

Statement

For every integer k≥3, the residue class of 5 has order 2k−2 in (Z/2k)×.

Facts & Assumptions

Given: An integer k≥3.

[L4]

Mathematical induction holds on N (The principle of mathematical induction).

[L5]

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

Proof

technique · induction
1.1baseL3L5algebra

The odd integer 5 is coprime to 2k, so [L5] puts its class in the unit group. At j=0, 520−1=4, so its 2-adic valuation is 2.

1.2ihL2L3

Assume v2(52j−1)=j+2. Since 52j≡1(mod4), the factor 52j+1 is congruent to 2 modulo 4 and has valuation 1. The factorisation 52j+1−1=(52j−1)(52j+1) and [L3] therefore give valuation j+3.

2.1step 1.1step 1.2L4

By induction, v2(52j−1)=j+2 for all j≥0.

3.1step 2.1L3

Step 2.1 with j=k−2 gives 52k−2≡1(mod2k), while the case j=k−3 gives 52k−3≢1(mod2k).

4.1step 1.1step 3.1L1discharge-induction∎

By [L1], the order divides 2k−2; every proper divisor of this prime power divides 2k−3, which step 3.1 excludes. Hence the order is 2k−2.

Depends on

Used by

Dependency tree · two levels

48 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