twin_prime_fourhundredthirtyone_fourhundredthirtythree
plain-language theorem explainer
The declaration asserts that 431 and 433 form a twin prime pair. Number theorists checking explicit small prime constellations or embedding concrete arithmetic facts into larger frameworks would reference it. The proof reduces to a single native decision procedure that evaluates the primality predicates and the required difference directly.
Claim. $431$ and $433$ are both prime numbers satisfying $433 = 431 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and keeping statements minimal before Dirichlet inversion layers are added. The local setting therefore treats basic number-theoretic predicates as stable interfaces. The Prime predicate is the repository-local transparent alias for the standard Nat.Prime predicate on natural numbers.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of the two primality statements and the difference equality.
why it matters
The result supplies an explicit twin-prime datum inside the NumberTheory.Primes.ArithmeticFunctions submodule. It fills a basic verification step for arithmetic-function constructions, though recorded downstream uses are empty and no direct link to the forcing chain, RCL, or phi-ladder appears. Its role therefore remains that of a concrete check whose integration into larger Recognition Science arguments is still open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.