totient_fortyeight
plain-language theorem explainer
Euler's totient evaluates to 16 at argument 48. Number theorists verifying concrete arithmetic function values would cite this equality for table checks or reductions. The proof is a one-line native decision that delegates through the totient wrapper to Nat.totient and confirms the equality directly.
Claim. $φ(48) = 16$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including Euler's totient. The upstream totient definition is the direct wrapper totient n := Nat.totient n, described as Euler's totient function wrapper. This theorem lives in the NumberTheory.Primes.ArithmeticFunctions module, whose local setting is to keep statements lightweight until deeper Dirichlet algebra can be layered on.
proof idea
The proof is a one-line wrapper that applies native_decide to the equality after the totient definition reduces the left-hand side to Nat.totient 48.
why it matters
This supplies a concrete evaluation of the totient function at 48, supporting downstream arithmetic computations in the Recognition Science number theory layer. It builds directly on the totient definition and aligns with the module goal of stabilizing basic interfaces for Möbius and related functions. No parent theorems are listed among the used-by edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.