two_pow_five
plain-language theorem explainer
The equality 2 raised to the fifth power equals 32 holds in the natural numbers. It supplies a verified numerical constant for arithmetic calculations involving primes or powers. The proof proceeds by direct evaluation via Lean's native decision procedure.
Claim. $2^5 = 32$
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. This theorem supplies a basic power equality that may underpin calculations involving primes or squarefree numbers. No upstream lemmas are referenced, as the result is a direct numerical identity.
proof idea
It is a one-line wrapper applying the native_decide tactic to evaluate the power expression directly.
why it matters
This result anchors numerical computations in the primes module. It does not connect to the main Recognition Science chain steps such as J-uniqueness or the phi fixed point, serving instead as a foundational arithmetic fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.