totient_onehundredtwenty
plain-language theorem explainer
Euler's totient function evaluates to 32 at 120. Researchers checking explicit values of arithmetic functions for small composites cite this evaluation. The proof is a one-line wrapper that invokes native_decide to compute the result directly from the definition.
Claim. $varphi(120) = 32$, where $varphi$ is Euler's totient function.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Euler's totient is introduced via the definition totient n := Nat.totient n. This specific evaluation appears among small-value computations that precede remarks on the Liouville function at small composites.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate totient 120.
why it matters
This supplies a verified concrete value for Euler's totient at 120 inside the arithmetic-functions module. It supports explicit checks for small composites but feeds no listed downstream theorems. The result sits outside the main forcing chain and does not touch open questions in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.