emirp_onehundredfiftyseven
plain-language theorem explainer
157 reversed is 751, and both are distinct primes. Number theorists cataloging emirps or verifying digit-reversal properties would cite this explicit case. The proof is a one-line computational decision via native_decide that evaluates the conjunction directly.
Claim. $157$ is prime, $751$ is prime, and $157 ≠ 751$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent local alias for the standard primality predicate on natural numbers. Upstream decidability interfaces from empirical programs and simplicial constructions enable direct evaluation of such predicates without additional hypotheses.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the conjunction of the two primality statements and the inequality.
why it matters
This supplies a concrete emirp instance inside the primes arithmetic functions section. It populates specific numerical facts used in the broader number-theory scaffolding for Recognition Science, though it carries no downstream citations. The example sits alongside repunit-prime remarks and supports the framework's reliance on verified small cases en route to T5 J-uniqueness and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.