twin_prime_three_five
plain-language theorem explainer
The statement confirms that 3 and 5 are both prime and differ by exactly 2. Number theorists verifying base cases for twin prime pairs or arithmetic function setups would reference this explicit check. The proof executes via native_decide, which reduces the entire conjunction to a decidable computation.
Claim. $3$ and $5$ are prime numbers with $5 = 3 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ for later Dirichlet inversion work. Prime is the transparent alias for Nat.Prime. The upstream and result from CirclePhaseLift supplies an explicit log-derivative bound M on a disk, while the Basic module keeps the prime predicate as a direct alias.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the primality predicates for the small constants and the arithmetic equality directly.
why it matters
The declaration supplies a verified twin prime pair at the base of the arithmetic functions module. It supports prime-related tools that may feed into Recognition Science constructions such as the phi-ladder or forcing chain steps, even though no immediate downstream theorems depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.