palindromic_prime_seven
plain-language theorem explainer
7 is established as a prime number in the natural numbers. Number theorists working with small palindromic cases or arithmetic function foundations would cite it for basic verification. The proof is a one-line native_decide term that evaluates the primality predicate directly.
Claim. The integer $7$ satisfies the primality predicate, i.e., it is prime in the natural numbers.
background
The ArithmeticFunctions module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for the standard Nat.Prime predicate on natural numbers. Upstream results include the is class from OptionAEmpiricalProgram ensuring collision-free properties and the is theorem from EdgeLengthFromPsi confirming algebraic tautologies or hypothesis discharge.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the primality predicate for 7.
why it matters
This supplies a basic verified fact about the single-digit palindromic prime 7 inside the primes module. It supports the module's goal of stabilizing small cases before layering Dirichlet algebra. No downstream theorems are listed, and it touches no open scaffolding in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.