totient_pos_iff
Euler's totient function is positive precisely when its argument is a positive natural number. Researchers working with arithmetic functions and Möbius inversion cite the equivalence to drop zero cases from sums and products. The proof is a one-line wrapper that unfolds the local definition and invokes the corresponding Mathlib fact.
claimFor every natural number $n$, $0 < ϕ(n)$ if and only if $0 < n$, 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 as a companion. The totient wrapper is defined by direct delegation: totient n := Nat.totient n. An upstream one-sided result establishes that positivity holds whenever the argument is positive.
proof idea
The proof is a one-line wrapper. Simplification unfolds the totient definition, after which the Mathlib theorem Nat.totient_pos is applied directly.
why it matters in Recognition Science
This equivalence completes the basic positivity statement for totient inside the arithmetic functions module. It supports later Möbius inversion and Dirichlet series constructions that rest on these footholds. No downstream uses are recorded yet.
scope and limits
- Does not compute explicit values of totient for specific arguments.
- Does not extend the statement beyond natural numbers.
- Does not connect totient to the phi-ladder or Recognition Science constants.
formal statement (Lean)
134theorem totient_pos_iff {n : ℕ} : 0 < totient n ↔ 0 < n := by
proof body
Term-mode proof.
135 simp only [totient]
136 exact Nat.totient_pos
137
138/-! ### Von Mangoldt function Λ -/
139
140/-- The von Mangoldt function (as an arithmetic function `ℕ → ℝ`). -/