prime_fivehundredfiftyseven
plain-language theorem explainer
557 is a prime number. Number theorists applying Möbius inversion or arithmetic functions in the Recognition Science setting would cite this fact when checking small primes. The proof is a one-line wrapper that invokes native_decide to evaluate the primality predicate computationally.
Claim. $557$ is prime.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for the standard primality predicate on natural numbers. Upstream results include interface theorems from foundation modules that establish collision-free properties and algebraic tautologies, along with the basic Prime definition.
proof idea
The proof is a one-line wrapper that applies native_decide to confirm the primality condition on 557.
why it matters
This supplies a basic prime fact supporting the arithmetic functions module and potential Möbius applications. It fills a number-theoretic foothold before deeper Dirichlet algebra is layered on, though no downstream uses are recorded. It remains separate from the main forcing chain, RCL, or phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.