two_pow_sixteen
plain-language theorem explainer
The equality 2^16 = 65536 is recorded directly in the natural numbers. Number theorists handling fixed powers of two during prime or arithmetic computations may reference the value. The proof executes via Lean's native_decide tactic, which reduces the expression at compile time.
Claim. $2^{16} = 65536$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ for Dirichlet inversion and squarefree checks. This theorem supplies a concrete numerical constant with no dependencies on sibling definitions such as mobius or bigOmega. The local setting centers on Möbius footholds before deeper algebra is layered in.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the power expression directly.
why it matters
This supplies a basic numerical constant inside the primes arithmetic functions module. It has no recorded parent theorems or downstream uses. The module context indicates support for concrete calculations involving powers, though it touches none of the Recognition Science landmarks such as the phi-ladder or J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.