prime_twohundredsixtythree
plain-language theorem explainer
263 is a prime natural number. Researchers handling arithmetic functions or Möbius inversions in the Recognition Science number-theory layer would cite this fact as a verified base case. The proof is a one-line native_decide invocation that reduces the claim to an immediate computational check inside Lean.
Claim. $263$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib's arithmetic-function library, beginning with the Möbius function μ. Prime is defined locally as the transparent alias abbrev Prime (n : ℕ) : Prop := Nat.Prime n. The surrounding file keeps statements minimal so that deeper Dirichlet inversion can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide, invoking Lean's built-in decision procedure to confirm that 263 has no proper divisors.
why it matters
The declaration supplies a concrete prime inside the arithmetic-functions module, anchoring potential later uses of the Möbius function or square-free checks. It sits within the NumberTheory.Primes hierarchy that supports the Recognition Science foundation but carries no recorded downstream citations yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.