prime_fiftythree
plain-language theorem explainer
The declaration establishes that 53 satisfies the primality predicate on natural numbers. Number theorists applying arithmetic functions such as the Möbius function would cite it when verifying small prime inputs for inversion formulas. The proof reduces to a single decide tactic that evaluates the predicate by direct computation.
Claim. $53$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, starting with the Möbius function. The local setting keeps statements minimal so that deeper Dirichlet algebra can be added once basic interfaces stabilize. The sole upstream result is the transparent alias Prime n := Nat.Prime n, which imports the standard primality predicate without additional hypotheses.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute the truth value of Nat.Prime 53.
why it matters
This supplies a concrete small-prime fact inside the arithmetic-functions module of the Recognition Science framework. It supports Möbius calculations on primes but has no recorded downstream uses yet. It fills a basic verification slot without touching the J-cost, phi-ladder, or T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.