weak_prime_thirteen
plain-language theorem explainer
The declaration verifies that 13 meets the weak prime criterion by being prime while lying strictly below the average of its immediate prime neighbors 11 and 17. Researchers handling explicit small-prime checks inside Recognition Science arithmetic modules would reference this instance for direct verification. The proof applies a native decision procedure that evaluates the full conjunction by computation.
Claim. $13$ is prime, $11$ is prime, $17$ is prime, and $13 < (11 + 17)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and squarefree predicates. The local Prime abbreviation is the transparent alias for the standard predicate that a natural number is prime. Upstream dependencies include structural interfaces from foundation, simplicial ledger, game theory, and Ramanujan bridge modules, none of which supply lemmas for this numerical check.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the conjunction of three primality statements and the arithmetic inequality by direct computation.
why it matters
The result supplies a concrete, machine-checked instance of a weak prime inside the number-theory layer of the Recognition Science framework. It fills a small explicit case in the arithmetic-functions file whose module doc focuses on Möbius footholds, though it records no downstream uses. The statement aligns with the framework's pattern of verifying small numerical facts that can later support larger constructions such as the phi-ladder or eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.