superprime_three
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.