emirp_thirtyone
plain-language theorem explainer
The declaration verifies that 31 and its digit reversal 13 are both prime and distinct. Number theorists examining emirp pairs as footholds in Recognition Science arithmetic functions would cite this concrete check. The proof is a one-line native_decide term that discharges the primality conjunction computationally.
Claim. $31$ is prime, its digit reversal $13$ is prime, and $31$ is distinct from $13$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for Nat.Prime from the Basic submodule. This emirp check sits among small primality facts that may later support Dirichlet inversion or squarefree predicates.
proof idea
One-line wrapper that applies native_decide to the conjunction of the two primality statements and the inequality.
why it matters
It supplies a verified emirp instance inside the primes arithmetic functions file. No downstream theorems are recorded yet. The result aligns with the module's role as a Möbius foothold but carries no direct link to the forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.