prime_fourhundrednine
plain-language theorem explainer
The theorem asserts that 409 is prime. Number theorists applying arithmetic functions such as the Möbius function within the Recognition Science framework would cite it to confirm small prime inputs for inversion formulas. The proof is a one-line native decision procedure that directly verifies the primality predicate.
Claim. $409$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Prime is the repo-local alias for Nat.Prime. The local setting keeps statements minimal so that deeper Dirichlet algebra and inversion can be added once basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to discharge the primality goal for 409.
why it matters
This declaration supplies a verified small prime inside the arithmetic functions module. It supports siblings such as mobius_prime and mobius_apply_of_squarefree that rely on prime inputs. No direct connection to the T0-T8 forcing chain or Recognition Composition Law appears; the result remains a pure number-theoretic foothold with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.