weak_prime_fortyseven
plain-language theorem explainer
The declaration verifies that 47 satisfies the weak-prime condition 47 < (43 + 53)/2 while confirming the primality of 47, 43 and 53. Number theorists building arithmetic-function interfaces or checking small cases on the phi-ladder would cite this fact when validating base instances for Möbius or big-Omega computations. The proof is a one-line native_decide invocation that directly discharges the finite conjunction of primality predicates and the arithmetic inequality.
Claim. $47$ is prime, $43$ is prime, $53$ is prime, and $47 < (43 + 53)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent local alias for the standard predicate Nat.Prime on natural numbers. This theorem supplies one of the small primality facts that support those wrappers. Upstream results include the class is from OptionAEmpiricalProgram and the theorem is from EdgeLengthFromPsi, both of which treat algebraic or structural identities that later rely on verified small-integer data.
proof idea
The proof is a one-line wrapper that applies native_decide to the entire conjunction. No intermediate lemmas are invoked; the tactic evaluates the primality checks and the numerical comparison directly in the kernel.
why it matters
The result supplies a concrete, machine-checked instance of a weak prime inside the arithmetic-functions layer. It supports the module's goal of providing stable footholds for Möbius and related functions before deeper Dirichlet inversion is added. No downstream theorems are recorded, so the declaration functions as a foundational check rather than a step in a larger chain. It aligns with the need for exact small-integer verifications that appear throughout the Recognition Science number-theory scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.