totient_prime
The theorem establishes that Euler's totient satisfies φ(p) = p - 1 for any prime p. Number theorists building arithmetic function interfaces in the Recognition Science setting cite it as the base case for prime inputs. The proof is a short tactic sequence that converts the local Prime predicate via prime_iff and invokes the Mathlib result Nat.totient_prime.
claimFor any prime number $p$, Euler's totient function satisfies $φ(p) = p - 1$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function and including the totient wrapper. The totient definition is totient n := Nat.totient n. The Prime predicate is the transparent alias Prime n := Nat.Prime n, equipped with the equivalence prime_iff n : Prime n ↔ Nat.Prime n.
proof idea
The proof obtains Nat.Prime p from the hypothesis via the left direction of prime_iff, then simplifies using the totient definition together with Mathlib's Nat.totient_prime applied to that prime.
why it matters in Recognition Science
This supplies the prime case for the totient function inside the arithmetic-functions module whose stated purpose is to provide Möbius footholds for later Dirichlet inversion. It sits upstream of any composite or power formulas that would be needed for the phi-ladder constructions elsewhere in the framework, though no direct dependents appear yet.
scope and limits
- Does not prove the totient formula for prime powers.
- Does not address composite inputs or inversion formulas.
- Does not link to the forcing chain or Recognition Science constants.
formal statement (Lean)
108theorem totient_prime {p : ℕ} (hp : Prime p) : totient p = p - 1 := by
proof body
Term-mode proof.
109 have hp' : Nat.Prime p := (prime_iff p).1 hp
110 simp [totient, Nat.totient_prime hp']
111
112/-- φ(p^k) = p^(k-1) * (p - 1) for prime p and k ≥ 1. -/