prime_threehundredfiftythree
plain-language theorem explainer
353 is established as a prime number. Number theorists applying Möbius function identities to small integers would cite this fact when verifying squarefree cases or inversion formulas. The proof is a one-line native decision that resolves the primality predicate by direct computation.
Claim. The natural number 353 is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for the standard Nat.Prime predicate on natural numbers. Upstream results include the basic Prime definition together with structural assertions from foundational modules on collision-free programs and simplicial structures, though none alter the primality check itself.
proof idea
The proof is a one-line wrapper that applies native_decide to discharge the primality statement by computational verification.
why it matters
The declaration supplies a verified small-prime instance inside the arithmetic-functions module, supporting later Möbius statements such as mobius_prime. It fills a concrete number-theoretic foothold but does not invoke Recognition Science landmarks such as the J-uniqueness map, the phi-ladder, or the eight-tick octave. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.