totient_four
plain-language theorem explainer
Euler's totient function satisfies φ(4) = 2. Researchers verifying small instances of arithmetic functions within number theory libraries would cite this base case. The proof is a one-line wrapper that applies native decision to evaluate the wrapped definition directly.
Claim. $φ(4) = 2$ where $φ$ denotes Euler's totient function.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including Euler's totient. The totient definition is the direct wrapper def totient (n : ℕ) : ℕ := Nat.totient n, which counts integers up to n that are coprime to n. This theorem appears in the NumberTheory.Primes.ArithmeticFunctions section, whose module documentation describes the file as providing small interfaces for later Dirichlet algebra once basic cases stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the value of the totient definition at 4.
why it matters
This supplies a verified small case inside the arithmetic functions module that supports the broader number theory scaffolding. It sits upstream of potential Möbius and inversion results in the same file, though no downstream uses are recorded. The placement aligns with the module's focus on lightweight footholds rather than deep Recognition Science landmarks such as the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.