prime_fourhundredone
plain-language theorem explainer
401 is a prime number. This specific primality fact supports arithmetic function evaluations in the Recognition Science number theory layer, particularly when Möbius or related sums encounter this integer. The proof is a direct computational verification performed by the native_decide tactic.
Claim. The natural number 401 satisfies Nat.Prime(401).
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 declaration depends on this alias plus several interface structures from Foundation and GameTheory modules whose 'is' predicates serve as collision-free or tautological markers.
proof idea
One-line term proof that applies native_decide to evaluate the primality predicate directly.
why it matters
Supplies a verified concrete prime for downstream arithmetic calculations in the Recognition framework. No parent theorems are listed in the used-by edges; the result sits inside the arithmetic-functions scaffolding that prepares Möbius footholds for later Dirichlet inversion work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.