twin_prime_onehundredone_onehundredthree
plain-language theorem explainer
The declaration asserts that 101 and 103 form a twin prime pair. Number theorists checking small prime constellations or building arithmetic function examples in the Recognition Science module would cite this concrete case. The proof reduces the entire conjunction to a single native_decide call that evaluates the predicates computationally.
Claim. The integers $101$ and $103$ are both prime and satisfy $103 = 101 + 2$.
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 predicate Nat.Prime on natural numbers. The surrounding file keeps statements minimal so that Dirichlet inversion and related algebra can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the conjunction of primality statements and the difference equation by direct computation.
why it matters
This supplies a verified twin-prime instance inside the number-theory layer that supports later arithmetic-function work. No parent theorems or downstream uses are recorded, so the result functions as an illustrative check rather than a chain step. It remains isolated from the forcing chain T0-T8 and from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.