four_almost_prime_onehundredforty
plain-language theorem explainer
140 factors as 2 squared times 5 times 7 and therefore satisfies the 4-almost-prime predicate. Number theorists building explicit factorization examples for sieve or Chen-prime arguments would cite this verification. The proof is a one-line native decision that evaluates the predicate directly on the concrete integer.
Claim. The integer $140 = 2^2 5 7$ is a 4-almost prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The four-almost-prime predicate counts prime factors with multiplicity and is defined in the same file. Upstream results include basic structures from constants and foundations that embed these number-theoretic tools inside the Recognition Science setting.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate isFourAlmostPrime on the fixed integer 140.
why it matters
This concrete check supplies an explicit base case inside the arithmetic-functions module. It supports later constructions such as Chen primes noted in the surrounding comments and contributes a verified instance to the number-theory footholds required by the overall framework. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.