superprime_thirtyone
plain-language theorem explainer
The declaration asserts that both 31 and 11 are prime numbers. It would be cited when verifying concrete prime instances that support arithmetic function calculations in the Recognition Science setup. The proof reduces the claim to a single native_decide call that performs the decidable primality computation.
Claim. $31$ and $11$ are both prime numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The local theoretical setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once interfaces stabilize. The predicate Prime is the transparent alias for Nat.Prime. Upstream results include the Prime alias itself together with several structure and theorem declarations that encode collision-free or algebraic-tautology properties.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic directly to the conjunction of the two primality statements.
why it matters
The result supplies a verified prime instance inside the arithmetic-functions module. It sits beneath any later use of the Möbius function or square-free checks that rely on concrete primes, though no downstream declarations currently reference it. The placement aligns with the basic number-theory scaffolding that precedes deeper Recognition Science constructions such as the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.