totient_one
plain-language theorem explainer
Euler's totient satisfies φ(1) = 1. Number theorists building arithmetic-function interfaces for prime factorization in the Recognition framework cite this identity as a base case. The proof is a one-line term reduction that invokes the wrapper definition together with the standard library fact on the totient of unity.
Claim. $φ(1) = 1$, where $φ$ is Euler's totient function.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and its squarefree properties. The totient wrapper is defined by direct delegation to the natural-number totient. Upstream results include the totient definition itself and a meta-realization structure that records structural axioms without adding content to this identity.
proof idea
One-line term proof that applies simplification on the totient wrapper and the library fact Nat.totient_one.
why it matters
The identity supplies the base case for the arithmetic-functions layer that supports Möbius footholds in the primes module. It fills the standard property required before Dirichlet inversion or inversion formulas can be layered on, consistent with the module's goal of stabilizing basic interfaces. No downstream uses are recorded yet, and the result does not invoke the forcing chain or phi-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.