totient_two_pow_one
plain-language theorem explainer
Euler totient evaluates to 1 at the prime power 2. Number theorists handling arithmetic functions or prime-power cases would reference this concrete evaluation. The proof proceeds via native decision procedure that directly computes the value.
Claim. $varphi(2^1) = 1$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including Euler totient. The totient definition delegates directly to the standard implementation: def totient (n : ℕ) : ℕ := Nat.totient n. Local setting focuses on small interfaces for Dirichlet algebra and inversion once the basic layers stabilize.
proof idea
One-line wrapper that applies the native_decide tactic to evaluate the concrete expression totient (2 ^ 1) by direct computation.
why it matters
This supplies a basic concrete case for totient at the smallest prime power, supporting the arithmetic functions layer in NumberTheory.Primes. It aligns with the general pattern φ(2^k) = 2^{k-1} for k ≥ 1 noted in the declaration comment but has no recorded downstream uses. It does not yet connect to Recognition Science landmarks such as the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.