totient_isMultiplicative
Euler's totient satisfies φ(mn) = φ(m)φ(n) for coprime natural numbers m and n. Number theorists handling multiplicative arithmetic functions or Dirichlet series would cite this property. The proof is a one-line wrapper applying the coprime multiplication lemma after introducing the hypothesis.
claimIf natural numbers $m$ and $n$ are coprime, then Euler's totient function satisfies $ϕ(mn) = ϕ(m)ϕ(n)$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to related maps such as totient. Local conventions keep statements minimal to support later Dirichlet inversion once interfaces stabilize. The totient wrapper is defined by totient n := Nat.totient n, and the present theorem encodes the standard multiplicativity property under the coprimeness hypothesis.
proof idea
This is a one-line wrapper that applies totient_mul_of_coprime after introducing the coprime hypothesis m and n.
why it matters in Recognition Science
The result records the multiplicativity of totient, a basic arithmetic-function property that supports Möbius inversion and prime-power divisor counts within the module. It sits downstream of the totient definition and the coprime multiplication lemma, feeding potential extensions to Dirichlet algebra. No immediate downstream uses appear in the current graph, leaving open its integration into Recognition Science spectral or complexity structures.
scope and limits
- Does not establish multiplicativity when m and n share a common factor.
- Does not compute explicit values of totient at prime powers.
- Does not link the property to phi-ladder mass formulas or J-cost minimization.
- Does not address analytic continuation or Dirichlet series convergence.
formal statement (Lean)
532theorem totient_isMultiplicative :
533 ∀ {m n : ℕ}, Nat.Coprime m n → totient (m * n) = totient m * totient n := by
proof body
Term-mode proof.
534 intro m n h
535 exact totient_mul_of_coprime h
536
537/-! ### Divisors of prime powers -/
538
539/-- The divisors of p^k are exactly {p^0, p^1, ..., p^k}. -/