totient_threehundredsixty
plain-language theorem explainer
Euler's totient evaluates to 96 at the integer 360. Number theorists using the Recognition Science arithmetic functions layer would cite this for concrete calculations involving highly composite arguments. The verification is a direct evaluation via the native decision procedure on the underlying definition of totient.
Claim. $varphi(360) = 96$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including Euler's totient. The totient wrapper is defined directly as the standard natural-number totient operation. Upstream dependencies include a meta-realization structure recording orbit coherence axioms and an explicit log-derivative bound theorem on the circle, though the immediate content used here is the totient definition itself.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the concrete equality from the totient definition.
why it matters
This supplies an explicit numerical value for the totient function at 360 inside the arithmetic functions module. It supports downstream prime and squarefree calculations in the NumberTheory.Primes layer. No direct connection to the forcing chain T0-T8 or the Recognition Composition Law appears here; the result remains a basic computational anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.