palindromic_prime_sevenhundredninetyseven
plain-language theorem explainer
797 is a prime whose decimal digits form a palindrome. Number theorists cataloging explicit primes or building examples for arithmetic function libraries would cite the fact. The proof is a one-line term that invokes native_decide to settle primality by direct computation.
Claim. $797$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related maps. Prime is the repo-local transparent alias for Nat.Prime. The local setting is therefore a collection of small, decidable statements about specific integers that can later support Dirichlet inversion or square-free detection.
proof idea
The proof is a one-line term that applies native_decide to the goal Prime 797.
why it matters
The declaration supplies an explicit palindromic prime inside the primes submodule. It forms part of the concrete number-theoretic base that Recognition Science uses before ascending to the J-cost and phi-ladder constructions. No downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.