totient_apply
plain-language theorem explainer
Equating the Recognition Science wrapper for Euler's totient to the standard definition on natural numbers allows direct compatibility with Mathlib. Number theorists building arithmetic function interfaces in the Recognition framework cite this to confirm that the wrapper introduces no deviation. The proof reduces to a single reflexivity step on the wrapper definition.
Claim. For every natural number $n$, the Euler totient wrapper satisfies $varphi(n) = mathrm{Nat.totient}(n)$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function as a foothold for later Dirichlet algebra. The totient wrapper is defined directly as an alias to the standard implementation. This upstream definition supplies the exact equality that the theorem invokes.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity to the totient definition.
why it matters
The declaration anchors the arithmetic functions module by confirming that the totient wrapper matches the classical value exactly. It supports the module's stated goal of providing stable interfaces before layering deeper inversion results. No downstream uses appear yet, so the result functions as a compatibility layer for subsequent Möbius and squarefree theorems in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.