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.

Carmichael's function on prime powers and its least-common-multiple formula

Statement

Carmichael's function satisfies $λ (1) = 1$ , and for prime powers,

$λ (p^{k}) = p^{k - 1} (p - 1) (p odd, k \geq 1),$

$λ (2) = 1, λ (4) = 2, λ (2^{k}) = 2^{k - 2} (k \geq 3) .$

If $n = \prod_{i < r} q_{i}^{e_{i}}$ is its prime-power factorisation, then

$λ (n) = {lcm}_{i < r} λ (q_{i}^{e_{i}}) .$

Here $lcm$ of a finite list is the iterated binary least common multiple of Common multiple, and the least common multiple $lcm (a, b)$ , taken to be $0$ when $a = 0$ or $b = 0$ , which defines that operation for two arguments only: set ${lcm}_{i < 0} a_{i} : = 1$ and ${lcm}_{i < s + 1} a_{i} : = lcm ({lcm}_{i < s} a_{i}, a_{s})$ . In particular the empty least common multiple is $1$ , which is the value taken at $n = 1$ .

Facts & Assumptions

Given: A positive integer $n$ and its prime-power factorisation.

[L1]

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

[L2]

The structure theorem gives every prime-power factor of the unit group explicitly (The unit group modulo $n$ is the product of its odd-prime cyclic factors and its explicit $2$ -power factor).

[L3]

An exponent kills an element precisely when it is divisible by that element's order (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 ∣$ ).

Proof

technique · direct

1.1

Reading the exponents of the cyclic factors in [L2] gives the displayed odd-prime and $2$ -power formulas, as well as $λ (1) = 1$ .

L1L2L3

1.2

Let $a_{0}, \dots, a_{r - 1}$ be the factor exponents and $ℓ_{s} = {lcm}_{i < s} a_{i}$ as defined in the Statement from the binary operation of [L4]. Induction on $s$ shows that a positive integer $m$ satisfies $ℓ_{s} ∣ m$ exactly when $a_{i} ∣ m$ for every $i < s$ : at $s = 0$ both sides hold always, since $ℓ_{0} = 1$ and the condition is vacuous; and $ℓ_{s + 1} = lcm (ℓ_{s}, a_{s})$ divides $m$ exactly when $ℓ_{s} ∣ m$ and $a_{s} ∣ m$ , by [L5] for one direction and because $ℓ_{s}$ and $a_{s}$ both divide $ℓ_{s + 1}$ for the other. In a finite direct product a power kills every tuple exactly when it is divisible by the exponent of each factor, by [L1] and [L3]; so the least such positive power is $ℓ_{r}$ .

L1L3L4L5algebra

2.1

Apply step 1.2 to the CRT decomposition in [L2] to obtain the formula for general $n$ , including the empty product at $n = 1$ .

step 1.2L2∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 115 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, Theorem C.V.6 (standard reference, not scraped)