two_pow_twenty
plain-language theorem explainer
The equality 2 raised to the twentieth power equals 1048576 holds in the naturals. Number theorists needing an exact power-of-two anchor for arithmetic calculations would cite it. The proof is a one-line native decision that evaluates the expression directly.
Claim. $2^{20} = 1048576$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and its basic squarefreeness properties. Local conventions keep statements minimal so that Dirichlet inversion can be added later once interfaces stabilize. This numerical equality supplies a concrete integer fact that can be referenced inside larger arithmetic identities without external computation.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to reduce the power expression to a decidable equality.
why it matters
The declaration records a verified numerical constant inside the arithmetic-functions module. It supports exact integer manipulations that may appear in prime-counting or Möbius-related calculations. No direct link to the Recognition forcing chain or phi-ladder is present, yet the fact closes a small computational gap for downstream arithmetic work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.