totient_three_pow_one
plain-language theorem explainer
φ(3) equals 2, supplying a concrete base case for totient evaluations at the smallest odd prime. Arithmetic function work in prime-power settings cites this when initializing identities or inversion formulas. The proof reduces to a single native decision step that computes the wrapped Nat.totient value directly.
Claim. $φ(3) = 2$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and including the Euler totient. The totient wrapper is defined by direct delegation to the standard Nat.totient, which counts integers up to n that are coprime to n. This theorem belongs to the documented collection of φ(3^k) values that support basic arithmetic identities.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic on the totient definition applied to the concrete input 3.
why it matters
The declaration fills a basic evaluation slot in the φ(3^k) series, providing a concrete anchor for arithmetic function development in the module. It supports later Möbius-related constructions even though no immediate downstream theorems are recorded. The result remains isolated from the Recognition Science forcing chain and physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.