strong_prime_sixtyseven
plain-language theorem explainer
67 satisfies the strong prime condition 67 > (61 + 71)/2 together with the primality of 61, 67 and 71. Researchers examining specific prime instances within arithmetic functions would cite this result. The verification relies on native_decide, which computationally confirms the primality predicates and the numerical inequality.
Claim. $67$ is prime, $61$ is prime, $71$ is prime, and $67 > (61 + 71)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Local notation includes the transparent alias Prime for Nat.Prime. The theorem appears among sibling definitions for Möbius and bigOmega but stands apart as a concrete numerical check. Upstream results supply the Prime abbreviation and assorted 'is' markers from Foundation and GameTheory modules that flag algebraic or collision-free properties.
proof idea
The proof is a one-line wrapper that applies native_decide to discharge the conjunction of three primality statements and the arithmetic inequality.
why it matters
This supplies a concrete numerical fact about the prime 67 inside the arithmetic functions module. It feeds no downstream theorems in the current graph. Within Recognition Science it offers a specific instance that could support prime-ladder calculations, though it carries no direct tie to the forcing chain T0-T8, the Recognition Composition Law, or phi-based constants. The doc-comment labels it explicitly as the strong-prime verification for 67.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.