prime_threehundredfortynine
plain-language theorem explainer
349 is established as a prime natural number. Researchers working with arithmetic functions such as the Möbius function in the Recognition Science number theory layer would cite this when verifying small prime inputs for squarefree or inversion calculations. The proof is a direct one-line computational check via the native_decide tactic.
Claim. The natural number $349$ satisfies the primality predicate, i.e., $349$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function and related predicates such as squarefree checks. Prime is the transparent local alias for the standard primality predicate on natural numbers. Upstream dependencies include the basic Prime definition together with interface 'is' statements from foundation, simplicial ledger, game theory, and Ramanujan bridge modules that enforce algebraic or collision-free properties.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the primality claim by direct computation.
why it matters
The declaration supplies a verified small prime inside the arithmetic functions module, supporting downstream Möbius and big-Omega constructions even though no explicit used-by edges are recorded. It fills a basic number-theory foothold consistent with the Recognition Science emphasis on prime factorization for the phi-ladder and mass formulas. No open scaffolding questions are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.