three_almost_prime_seventysix
plain-language theorem explainer
The declaration establishes that 76 factors as 2 squared times 19 and thus has exactly three prime factors counting multiplicity. Number theorists working on almost-prime counts in the Recognition Science setting would reference this concrete check. The proof reduces to a single native decision procedure that evaluates the big-Omega function directly on the integer.
Claim. The integer 76 satisfies $Ω(76) = 3$, where $Ω$ counts prime factors with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. A number n is declared three-almost-prime when its total number of prime factors with multiplicity, denoted bigOmega n, equals three. The upstream definition isThreeAlmostPrime n := bigOmega n = 3 supplies the predicate used here.
proof idea
One-line wrapper that applies native_decide to evaluate the predicate isThreeAlmostPrime on the constant 76.
why it matters
This supplies a verified arithmetic fact for use in calculations involving RS constants, as indicated by the following section on σ_2 and σ_3. It closes a specific check in the primes layer without relying on general theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.