superprime_three
The declaration asserts that both 2 and 3 are prime numbers. Number theorists initializing arithmetic functions such as the Möbius function in the Recognition Science primes module would cite this fact to anchor the prime ladder. The proof reduces to a direct native decision procedure that verifies the two primality conditions without further lemmas.
claim$2$ and $3$ are both prime numbers, where primality is the standard predicate on natural numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for Nat.Prime. The local setting is the establishment of basic footholds for Dirichlet algebra and inversion once the interfaces stabilize. The upstream Prime abbrev supplies the predicate used in the conjunction.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of the two primality statements.
why it matters in Recognition Science
This supplies a minimal prime fact inside the NumberTheory.Primes.ArithmeticFunctions module that supports later Möbius and big-Omega constructions. It sits at the base of the prime ladder referenced in mass formulas and the phi-ladder, though it carries no direct link to the forcing chain T0-T8 or the recognition composition law. No downstream uses are recorded, so the result functions as an unelaborated anchor.
scope and limits
- Does not prove primality for any integer larger than 3.
- Does not connect primality to the J-cost, defect distance, or eight-tick octave.
- Does not supply a constructive or analytic proof of primality.
formal statement (Lean)
2788theorem superprime_three : Prime 3 ∧ Prime 2 := by native_decide
proof body
Term-mode proof.
2789
2790/-- p_3 = 5 is a superprime. -/