five_almost_prime_onehundredseventysix
plain-language theorem explainer
The declaration establishes that 176 factors as 2^4 times 11 and therefore satisfies big-Omega equal to five. Researchers checking arithmetic properties of integers near the Recognition Science critical value phi^5 would cite this concrete case. The proof is a direct native decision that evaluates the predicate on the fixed input.
Claim. $176 = 2^4 11$ and therefore satisfies $Omega(176) = 5$, where $Omega(n)$ counts the prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. A number is 5-almost prime precisely when its big-Omega value equals five. The upstream definition states: 'A number is 5-almost prime if Ω(n) = 5.' This sits inside the NumberTheory.Primes.ArithmeticFunctions module whose local setting is to stabilize basic interfaces before layering Dirichlet algebra.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the predicate isFiveAlmostPrime on the concrete input 176.
why it matters
This verification supplies an instance of a 5-almost prime containing the factor 11, which lies near the Recognition Science critical value phi^5. It supports the mass formula and yardstick constructions on the phi-ladder by confirming arithmetic properties of relevant integers. No downstream theorems depend on it yet, leaving open whether it will be invoked in larger prime-counting arguments within the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.