totient_eighthundredforty
plain-language theorem explainer
Euler totient evaluates to 192 at 840. Number theorists citing concrete arithmetic values inside the Recognition Science primes module would reference this evaluation. The proof is a one-line native decision on the wrapped standard totient definition.
Claim. Euler's totient function satisfies $varphi(840) = 192$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function as the initial foothold. Euler totient is defined directly as totient n := Nat.totient n, keeping statements minimal ahead of deeper Dirichlet algebra. The local setting is therefore a thin interface layer rather than a full development of inversion formulas.
proof idea
One-line wrapper that applies native_decide to the totient definition at 840.
why it matters
This supplies a verified numerical instance inside the arithmetic functions file, supporting the module's role in establishing Möbius footholds. No downstream theorems depend on it in the current graph, and it does not engage the forcing chain, RCL, or phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.