weak_prime_twentythree
plain-language theorem explainer
The theorem verifies that 23 satisfies the weak-prime condition by confirming primality of 19, 23 and 29 together with the inequality 23 < (19 + 29)/2. Number theorists working on prime gaps or arithmetic-function identities in the Recognition Science setting would cite the fact. The proof reduces the entire conjunction to a single native_decide call that settles the predicates and arithmetic by direct computation.
Claim. $23$ is prime, $19$ is prime, $29$ is prime, and $23 < (19 + 29)/2$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic-function library, beginning with the Möbius function. Prime is the transparent alias for the standard Nat.Prime predicate. The local setting keeps statements minimal so that deeper Dirichlet algebra can be added once the basic interfaces stabilize. Upstream results include structural 'is' declarations from foundation, simplicial-ledger and game-theory modules that guarantee algebraic or collision-free properties, though none of them participate in this numerical check.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to resolve the three primality predicates and the numerical inequality by direct computation.
why it matters
The declaration supplies a concrete verified instance of a weak prime that can support later arithmetic-function identities or gap analyses. It sits inside the number-theory layer that underpins Möbius inversion and related tools. No downstream uses are recorded, indicating it functions as a self-contained fact rather than an active lemma. It touches the T0-T8 chain only indirectly through the number-theoretic primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.