totient_pos
Euler's totient function is strictly positive for every positive integer. Number theorists citing arithmetic-function properties would reference this result before applying Möbius inversion or coprimality counts. The proof is a term-mode one-liner that unfolds the local wrapper and invokes the matching library fact.
claimFor every positive integer $n$, Euler's totient function satisfies $0 < ϕ(n)$.
background
The ArithmeticFunctions module supplies thin wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including the totient. The totient wrapper is defined by direct delegation to the standard Nat.totient. The module keeps statements lightweight to support later Dirichlet inversion layers.
proof idea
The term proof first applies simp to replace the local totient definition with Nat.totient, then uses the library theorem Nat.totient_pos.mpr on the hypothesis that n is positive.
why it matters in Recognition Science
This theorem is invoked by the bidirectional statement totient_pos_iff in the same file, which equates positivity of the totient with positivity of the argument. It supplies a basic number-theoretic foothold inside the primes and arithmetic-functions layer; no direct tie to the forcing chain or phi-ladder appears in the supplied material.
scope and limits
- Does not define or compute an explicit formula for ϕ(n).
- Does not treat the case n = 0 or non-positive arguments.
- Does not extend the result to real or complex domains.
formal statement (Lean)
787theorem totient_pos {n : ℕ} (hn : 0 < n) : 0 < totient n := by
proof body
Term-mode proof.
788 simp only [totient]
789 exact Nat.totient_pos.mpr hn
790
791/-- φ(2^k) = 2^k - 2^(k-1) = 2^(k-1) for k ≥ 1 (concrete). -/