prime_fourhundredthirtynine
plain-language theorem explainer
439 is established as a prime natural number. Number theorists applying arithmetic functions such as the Möbius function within the Recognition Science module cite this fact for concrete prime instances. The verification reduces directly to a computational check via the native_decide tactic.
Claim. $439$ is a prime natural number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is defined locally as a transparent alias for Nat.Prime. The setting keeps statements minimal so that Dirichlet inversion can be added once interfaces stabilize. Upstream results include foundational 'is' declarations from option programs, simplicial ledgers, and mechanism design that enforce algebraic or collision-free properties, though this theorem relies only on the Prime abbreviation.
proof idea
The proof is a one-line term that applies the native_decide tactic to discharge the primality statement by direct computation.
why it matters
This supplies a concrete prime instance for sibling results such as mobius_prime inside the same module. It supports the arithmetic-function infrastructure without reference to the forcing chain T0-T8, the recognition composition law, or physical constants. No downstream usage is recorded and no open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.