prime_twohundredthirtythree
plain-language theorem explainer
233 is a prime number. Number theorists applying Möbius inversion or squarefree checks in the Recognition Science arithmetic functions layer would cite this fact for the specific case of 233. The proof reduces to a single native_decide call that evaluates the primality predicate by direct computation.
Claim. $233$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ. The local setting keeps statements minimal before layering Dirichlet algebra. Prime is the repo-local transparent alias for the standard primality predicate on natural numbers.
proof idea
The proof is a term-mode one-line wrapper that invokes native_decide to compute and confirm that 233 satisfies the primality condition.
why it matters
This supplies a concrete prime instance inside the NumberTheory.Primes.ArithmeticFunctions module, supporting sibling lemmas on the Möbius function at prime arguments. It populates basic number-theoretic facts without touching the forcing chain, phi-ladder, or Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.