totient_two_pow_four
plain-language theorem explainer
Computes Euler's totient at sixteen as eight. Researchers verifying small cases in prime-power arithmetic functions cite this when building tables or testing inversion formulas. The proof executes a native decision procedure on the definition.
Claim. Euler's totient function satisfies $φ(2^4) = 8$.
background
The module supplies lightweight wrappers for arithmetic functions, beginning with the Möbius function and extending to Euler's totient. The totient definition simply delegates to the standard Nat.totient implementation. This theorem supplies a concrete evaluation at the fourth power of two.
proof idea
One-line wrapper that invokes native_decide on the totient definition.
why it matters
Supplies a verified base case for totient evaluations on powers of two within the arithmetic functions module. Supports downstream number-theoretic constructions in the Recognition framework, though no direct dependents are listed yet. Aligns with the need for precise small-integer computations in the broader theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.