prime_fourhundrednineteen
plain-language theorem explainer
The declaration asserts that 419 is a prime number. Number theorists checking small primes for arithmetic function calculations, such as Möbius evaluations, would reference it as an explicit verified fact. The proof is a direct computational verification via the native_decide tactic applied to the primality predicate.
Claim. $419$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for Nat.Prime. The local setting is basic number-theoretic scaffolding for later Dirichlet algebra and inversion, with no deeper RS content introduced here.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the Prime predicate on 419.
why it matters
This supplies a concrete small-prime fact inside the arithmetic functions file. It supports sibling results such as mobius_prime and mobius_apply_of_squarefree. No downstream use is recorded yet, and the result touches none of the core Recognition Science landmarks such as the J-uniqueness forcing step or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.