palindromic_prime_onehundredfiftyone
plain-language theorem explainer
151 is asserted to be a prime number. Number theorists referencing basic facts inside Recognition Science arithmetic-function modules would cite this instance when building toward Möbius or divisor-function statements. The verification is a direct computational check via native decision that confirms the primality predicate holds.
Claim. $151$ is a prime number in the natural numbers, i.e., its only positive divisors are $1$ and itself.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is a transparent alias for Nat.Prime. The local setting keeps statements minimal so that deeper Dirichlet inversion can be added once interfaces stabilize. Upstream results include the definition of Prime as the standard primality predicate on naturals together with several class and structure declarations that supply collision-free or empirical-program interfaces used elsewhere in the monolith.
proof idea
The proof is a one-line term wrapper that applies native_decide to discharge the primality goal for the concrete numeral 151.
why it matters
This supplies a concrete palindromic-prime fact inside the number-theory layer that can feed arithmetic-function constructions. No downstream uses are recorded yet, so the declaration currently serves as a verified constant rather than an active lemma. It sits alongside the Möbius footholds and aligns with the framework's use of number-theoretic primitives before linking to constants such as the alpha band or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.