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

Carmichael's $λ (n)$ is the maximum order of a unit modulo $n$

Statement

For every $n \geq 1$ there is a unit modulo $n$ of order $λ (n)$ , and every unit has order dividing $λ (n)$ . Thus $λ (n)$ is the maximum element order in $(Z / n)^{\times}$ .

Facts & Assumptions

Given: A positive integer $n$ .

[L1]

$λ (n)$ is the exponent of the unit group (Carmichael's function $λ (n)$ as the exponent of $(Z / n Z)^{\times}$ ).

[L2]

The unit group is a finite direct product of cyclic groups with the explicit $2$ -power factors described in The unit group modulo $n$ is the product of its odd-prime cyclic factors and its explicit $2$ -power factor.

[L3]

An element of order $r$ is killed precisely by the multiples of $r$ (If $ord (g) = n$ then $g^{k} = e$ iff $k$ is an integer multiple of $n$ , the powers $g^{0}, \dots, g^{n - 1}$ are distinct, and $⟨ g ⟩$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$ ).

[L4]

For $a, b \in Z$ both nonzero, $lcm (a, b)$ is the least positive common multiple of $a$ and $b$ ; if $a = 0$ or $b = 0$ then the only common multiple is $0$ and $lcm (a, b) = 0$ . It is defined for two arguments only (Common multiple, and the least common multiple $lcm (a, b)$ , taken to be $0$ when $a = 0$ or $b = 0$ ).

[L5]

Every common multiple of $a$ and $b$ is a multiple of $lcm (a, b)$ (Every common multiple of $a$ and $b$ is a multiple of $lcm (a, b)$ , and $\gcd (a, b) \cdot lcm (a, b) = ∣ a b ∣$ ).

[L6]

If $g$ and $h$ have finite orders $m, n \geq 1$ , then $ord (g, h) = lcm (m, n)$ in the external direct product (If $g$ and $h$ have finite orders $m$ and $n$ , then $ι (ord (g, h)) = lcm (ι (m), ι (n))$ in $G \times H$ ).

Proof

technique · direct

1.1

In the decomposition [L2], choose a generator in every cyclic factor, including generators of both cyclic factors in the exceptional $2$ -power component.

L2choose

1.2

Let $r_{0}, \dots, r_{k - 1}$ be the orders of the chosen generators and define the iterated least common multiple from the binary operation of [L4] by $ℓ_{0} = 1$ and $ℓ_{s + 1} = lcm (ℓ_{s}, r_{s})$ ; [L4] supplies only the binary operation, so this recursion is what gives the list value. Induction on $s$ shows a positive $m$ satisfies $ℓ_{s} ∣ m$ exactly when $r_{i} ∣ m$ for every $i < s$ : at $s = 0$ both sides always hold, and $ℓ_{s + 1} ∣ m$ holds exactly when $ℓ_{s} ∣ m$ and $r_{s} ∣ m$ , by [L5] one way and because both divide $ℓ_{s + 1}$ the other. By [L3] a power kills the product exactly when it is divisible by every $r_{i}$ , so the exponent of the product is $ℓ_{k}$ .

L1L2L3L4L5algebra

2.1

The tuple of chosen generators has order $ℓ_{k}$ : iterating [L6] over the $k$ factors gives $ord$ of the tuple as the same iterated least common multiple, with the empty product contributing the identity of order $ℓ_{0} = 1$ .

step 1.1step 1.2L3L4L6

3.1

Steps 2.1 and 1.2 produce a unit of order $λ (n)$ , while [L1] makes every element order divide $λ (n)$ . The empty product at $n = 1$ gives the identity of order $1$ .

step 2.1step 1.2L1L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 119 results over 25 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

Peter Hackman, Elementary Number Theory, Lemma C.V.5 (standard reference, not scraped)

Carmichael's λ(n)λ(n) is the maximum order of a unit modulo nn