superprime_onehundredtwentyseven
plain-language theorem explainer
127 and 31 are both prime, with 127 identified as the 31st prime and a superprime in the Recognition Science sense. Number theorists applying arithmetic functions or phi-ladder mass formulas would cite this fact for exact prime inputs. The proof is a one-line native_decide tactic that computationally confirms both primality statements.
Claim. The integers 127 and 31 are both prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ. Prime is the repo-local alias for the standard predicate Nat.Prime on natural numbers. Upstream results include the transparent abbrev Prime and several 'is' declarations from foundational modules that encode collision-free or tautological properties used in decidability contexts.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the conjunction Prime 127 ∧ Prime 31.
why it matters
The declaration supplies concrete prime facts required for arithmetic-function evaluations on the phi-ladder. It aligns with the framework's use of Mersenne primes such as 2^7 - 1 in number-theoretic components, though no downstream theorems currently invoke it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.