prime_fivehundredthree
The declaration asserts that 503 is a prime natural number. Number theorists using arithmetic functions in the Recognition Science module would cite this fact when isolating prime cases inside Möbius sums or inversion identities. The proof reduces the claim to a direct computational decision via the native_decide tactic.
claim$503$ 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 supplied by the Basic submodule. Upstream results include the is interfaces from OptionAEmpiricalProgram, SimplicialLedger, MechanismDesignFromSigma, and MockThetaPhantom, which function as collision-free or tautological placeholders, together with the Prime abbrev itself.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the primality statement by direct computation.
why it matters in Recognition Science
The result supplies a concrete prime fact inside the arithmetic-functions module that supports Möbius footholds. It sits among the number-theoretic primitives that feed the Recognition Science forcing chain and phi-ladder constructions, although no downstream uses are recorded at present.
scope and limits
- Does not prove primality for any integer other than 503.
- Does not supply an analytic or constructive primality argument.
- Does not invoke or modify the Möbius function.
formal statement (Lean)
2390theorem prime_fivehundredthree : Prime 503 := by native_decide
proof body
Term-mode proof.
2391
2392/-- 509 is prime. -/