totient_seventytwo
plain-language theorem explainer
Euler's totient evaluates to 24 at argument 72. Number theorists using arithmetic functions for prime-related calculations would cite this evaluation. The proof applies a native decision tactic that computes the result from the underlying definition without manual expansion.
Claim. Euler's totient function satisfies $varphi(72) = 24$.
background
The module supplies lightweight wrappers for Mathlib arithmetic functions, starting with the Möbius function as a foothold. Euler's totient is introduced via the definition that maps each natural number n to its standard count of integers up to n coprime to n. This setting prepares for deeper Dirichlet inversion once interfaces stabilize, as noted in the module documentation.
proof idea
The proof is a one-line wrapper applying the native_decide tactic to evaluate the totient at 72 directly from its definition.
why it matters
This theorem supplies a verified value for the totient at 72 within the arithmetic functions module. It supports basic number-theoretic computations but connects to no parent theorems in the current dependency graph. The result remains isolated from the core Recognition Science forcing chain and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.