totient_twentyfour
plain-language theorem explainer
Euler totient evaluates to 8 at argument 24. Number theorists verifying small cases of arithmetic functions or preparing Möbius-based computations cite this equality. The proof is a direct native decision on the totient definition.
Claim. $varphi(24) = 8$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including Euler totient as a basic tool. Totient is defined directly as the standard Nat.totient, which counts integers up to n that are coprime to n. This theorem records the explicit value at 24, resting on the upstream totient wrapper.
proof idea
A one-line term proof applies native_decide to evaluate totient 24 against its definition as Nat.totient.
why it matters
It supplies a verified numerical fact for the totient function at 24 inside the arithmetic functions module. No immediate parent theorems appear in the dependents, yet it fills a basic slot that supports later Dirichlet algebra once interfaces stabilize. The result touches none of the Recognition Science forcing chain steps or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.