prime_triplet_three_five_seven
plain-language theorem explainer
Verification that the integers 3, 5, and 7 are each prime supplies a base case for arithmetic functions in the Recognition Science number theory development. Researchers constructing Möbius inversions or square-free checks would reference this fact. The proof reduces immediately to a native decision procedure on the small constants.
Claim. The natural numbers 3, 5, and 7 are each prime, i.e., $3$, $5$, and $7$ satisfy the standard primality predicate on $ℕ$.
background
The module supplies lightweight wrappers for Mathlib arithmetic functions, beginning with the Möbius function μ and related square-free checks. The Prime predicate is a transparent local alias for the standard Nat.Prime test on natural numbers. Upstream gap definitions compute logarithmic ratios of the form ln(1 + Z/φ)/ln(φ) for anchor scales and mass residues, yet remain unused by this declaration.
proof idea
The proof is a one-line term wrapper that applies the native_decide tactic to evaluate the conjunction of the three primality predicates on the concrete constants.
why it matters
This result populates the arithmetic functions module with an explicit prime triplet instance that can support Möbius lemmas on small primes. No parent theorems appear in the used_by graph. The declaration sits outside the main forcing chain, RCL, and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.