twin_prime_fortyone_fortythree
plain-language theorem explainer
41 and 43 form a twin prime pair. Number theorists verifying explicit small instances inside the Recognition Science arithmetic functions layer cite this result for concrete gap checks. The proof is a one-line native_decide term that evaluates the primality predicates and the exact difference directly.
Claim. $41$ and $43$ are both prime and satisfy $43 = 41 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function as a foothold for later Dirichlet work. Prime is the transparent alias for the standard Nat.Prime predicate on natural numbers. The declaration depends on the conjunction operator from CirclePhaseLift (which supplies an explicit log-derivative bound M) and on the basic Prime definition.
proof idea
A one-line term proof invokes native_decide to resolve the conjunction of the two primality statements and the arithmetic equality by direct computation.
why it matters
This supplies a verified twin-prime instance inside the arithmetic-functions section. It anchors small-scale number-theoretic facts that can support later prime-distribution or Möbius constructions, consistent with the framework's step-by-step build from basic definitions toward the phi-ladder and eight-tick structures. No immediate downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.