weak_prime_seven
plain-language theorem explainer
Verification that 7 is a weak prime proceeds by confirming primality of 7, 5 and 11 together with the strict inequality 7 less than their average. Number theorists working on small-case checks inside Recognition Science arithmetic functions cite this result. Native decision procedures evaluate the entire conjunction in one computational step.
Claim. $7$ is prime, $5$ is prime, $11$ is prime, and $7 < (5 + 11)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ for later Dirichlet inversion work. The primality predicate is the standard natural-number version. Upstream results supply foundational 'is' predicates that enforce collision-free properties in option structures and algebraic tautologies in simplicial and game-theoretic settings.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the conjunction of the three primality statements and the numerical inequality.
why it matters
This supplies a concrete base-case verification for the weak-prime property inside the arithmetic-functions module. It supports the Recognition Science number-theory layer that later feeds Möbius and big-Omega tools. No downstream theorems are recorded, indicating it functions as an isolated small-integer check rather than a lemma for larger results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.