emirp_seventynine
plain-language theorem explainer
79 and 97 form an emirp pair as both satisfy the primality predicate and are distinct. Number theorists working on digit-reversal properties or concrete prime instances would cite the result. The proof reduces the entire conjunction to a single native_decide call that evaluates it inside the kernel.
Claim. The numbers 79 and 97 are distinct primes.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The predicate appearing in the statement is the standard primality test on natural numbers, defined as an alias in the sibling Basic module. Upstream results include structural definitions from foundation modules that support the decidability environment used by the proof.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of the two primality statements and the inequality.
why it matters
The declaration supplies a verified concrete emirp instance inside the arithmetic functions file. It has no downstream uses listed and sits outside the main Recognition Science forcing chain or phi-ladder constructions. It contributes a basic number-theoretic fact that may be referenced in later prime-counting or arithmetic-function arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.