prime_fivehundrednine
plain-language theorem explainer
509 is established as a prime number. Number theorists applying the Möbius function within the Recognition Science arithmetic-functions module would cite this fact for squarefree checks and inversion steps. The proof reduces to a single native_decide call that delegates the primality test to the computational engine.
Claim. The natural number $509$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Statements remain minimal until Dirichlet algebra and inversion layers stabilize. The Prime predicate is the transparent alias for Nat.Prime.
proof idea
Term-mode proof consisting of a single native_decide tactic that computes primality directly.
why it matters
The declaration supplies a concrete prime fact for Möbius-related calculations in the module. It occupies a basic slot in the NumberTheory.Primes hierarchy without reference to the forcing chain, phi-ladder, or Recognition Composition Law. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.