prime_fourhundredthirtythree
plain-language theorem explainer
433 is established as a prime natural number. Number theorists applying Möbius inversion or squarefree checks inside the Recognition Science arithmetic functions module would cite this fact. The proof is a one-line native decision procedure that directly evaluates the primality predicate.
Claim. $433$ is a prime number in the natural numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ. Prime is the transparent alias for Nat.Prime. This supplies a concrete prime instance for use alongside sibling results such as mobius_prime and mobius_apply_of_squarefree.
proof idea
The proof is a term-mode one-liner that applies native_decide to discharge the primality goal.
why it matters
The result supplies a verified prime for the arithmetic functions file, supporting sibling declarations that apply the Möbius function to primes. It fits the module's lightweight approach to Dirichlet algebra without invoking the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.