prime_threehundredfortyseven
plain-language theorem explainer
347 is established as a prime integer. Number theorists applying Möbius inversion or arithmetic functions would cite this for small-prime verifications inside the Recognition Science number-theory layer. The proof is a one-line term that invokes native_decide to resolve the primality predicate computationally.
Claim. $347$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for Nat.Prime. The local setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line term that applies native_decide to the primality statement.
why it matters
This supplies a verified small-prime fact that can serve as input for Möbius-function calculations in the arithmetic-functions module. It does not touch the forcing chain, RCL, or phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.