prime_fivehundredsixtynine
plain-language theorem explainer
The theorem establishes that 569 is a prime number. Number theorists handling arithmetic functions such as the Möbius function in the Recognition Science setting would cite this fact for prime inputs in inversion formulas. The proof is a direct one-line native decision that evaluates the primality predicate by computation.
Claim. $569$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Local conventions keep statements minimal until Dirichlet algebra and inversion layers stabilize. Upstream, the primality predicate is the standard natural-number definition Nat.Prime, kept as a transparent alias.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the primality predicate directly.
why it matters
This supplies a verified prime fact that supports the arithmetic functions module and its Möbius footholds. It fills a basic number-theoretic slot in the Recognition Science framework without touching forcing chains or constants. No downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.