superprime_five
plain-language theorem explainer
Both 5 and 3 satisfy the primality predicate on natural numbers. Researchers initializing the phi-ladder for mass formulas in Recognition Science would cite this base fact. The proof executes as a direct native decision on the conjunction of the two primality checks.
Claim. $5$ and $3$ are both prime numbers in the natural numbers.
background
The module supplies lightweight wrappers around arithmetic functions, beginning with the Möbius function for later Dirichlet inversion steps. The primality predicate is the transparent local alias for the standard definition on natural numbers. Upstream results include foundational structures certifying collision-free properties and algebraic tautologies, plus the basic prime definition imported from the primes hierarchy.
proof idea
The proof is a one-line term that applies native_decide to evaluate the conjunction of the primality statements for 5 and 3.
why it matters
The declaration supplies the primality of 5 and 3 as concrete base cases, with the attached comment identifying 5 as a superprime instance. It supports initialization of the phi-ladder in the number theory layer of the Recognition framework. No downstream uses are recorded, leaving open its precise linkage to the forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.