prime_onehundredseventynine
plain-language theorem explainer
Establishes that 179 is a prime natural number. Number theorists working with Möbius functions or arithmetic operations would cite this for concrete small-prime instances. The proof executes a direct computational check via Lean's native decision procedure.
Claim. $179$ is a prime number.
background
The module supplies lightweight wrappers around arithmetic functions, beginning with the Möbius function. Prime is the standard primality predicate on natural numbers, defined as an alias for Nat.Prime. This supplies a verified instance for use inside such functions.
proof idea
One-line wrapper that invokes the native_decide tactic to reduce the claim to a decidable computational check of primality for 179.
why it matters
Supplies a basic primality fact inside the arithmetic-functions module. It supports the number-theory layer that underpins Möbius calculations in the Recognition Science framework. No connection appears to the forcing chain, J-uniqueness, or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.