totient_two
Euler totient evaluates to one at the integer two. Number theorists applying arithmetic functions to prime factorizations or inversion formulas would cite this base case. The proof reduces directly via simplification on the totient definition.
claimEuler's totient function satisfies $φ(2) = 1$.
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. The local setting keeps statements minimal to support later Dirichlet algebra and inversion once interfaces stabilize.
proof idea
One-line wrapper that applies simplification on the totient definition, reducing the equality to the known value of φ(2).
why it matters in Recognition Science
This evaluation supplies a base case for arithmetic-function calculations in the module. It supports downstream work on Möbius properties and squarefree detection, which feed into prime-related results. No direct link to Recognition Science landmarks such as the forcing chain or RCL appears here.
scope and limits
- Does not compute totient values for any integer other than 2.
- Does not relate totient to the Möbius function.
- Does not address generalizations or extensions beyond the natural numbers.
formal statement (Lean)
465theorem totient_two : totient 2 = 1 := by
proof body
Term-mode proof.
466 simp [totient]
467
468/-- φ(3) = 2. -/