prime_fivehundredfortyone
plain-language theorem explainer
541 is established as a prime natural number. Number theorists working with arithmetic functions such as the Möbius function in the Recognition Science framework would cite this fact when verifying small primes for computational checks. The proof is a direct term that applies native_decide to resolve the statement by algorithmic verification.
Claim. The natural number 541 is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is a transparent alias for the standard Nat.Prime predicate on natural numbers. Upstream results supply the Prime definition together with foundational structures whose doc-comments emphasize algebraic tautologies and zero-sorry verification.
proof idea
The proof is a one-line term that invokes native_decide to confirm primality of 541 by direct computation.
why it matters
This supplies a verified small-prime fact that supports arithmetic-function calculations in the Recognition Science number-theory layer. It aligns with the framework's use of precise integer facts for Möbius footholds without adding hypotheses or scaffolding. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.