strong_prime_eleven
plain-language theorem explainer
Eleven satisfies the strong prime condition 11 > (7 + 13)/2 together with the primality of 7, 11 and 13. Researchers examining prime gaps or arithmetic properties within the Recognition Science number theory layer would cite this for concrete verification of the eleven case. The proof reduces to a native_decide call that evaluates the finite numerical predicates directly.
Claim. $11$ is prime, $7$ is prime and $13$ is prime, and moreover $11 > (7 + 13)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard natural-number primality predicate. This theorem sits among siblings that define Möbius and big-Omega functions for square-free integers.
proof idea
The proof is a one-line wrapper that invokes native_decide to discharge the conjunction of primality checks and the inequality by direct computation.
why it matters
This declaration provides a verified instance of a strong prime relevant to the phi-ladder and eight-tick octave in the Recognition framework. It aligns with T7 by checking specific primes like 11, 7, 13 that appear in arithmetic function applications such as Möbius inversion. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.