five_almost_prime_twohundredseventytwo
plain-language theorem explainer
272 factors as 2^4 times 17 and therefore carries exactly five prime factors counted with multiplicity. Number theorists checking concrete instances inside Recognition Science arithmetic functions would cite this case. The verification is a direct computational reduction that evaluates the big-Omega count against five.
Claim. $Ω(272) = 5$, where $Ω(n)$ is the total number of prime factors of $n$ counted with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. A 5-almost prime is defined by the predicate that bigOmega n equals 5, i.e., the sum of exponents in the prime factorization is exactly five. The specific claim concerns 272, whose factorization 2^4 × 17 meets the count and is flagged as RS-relevant through the factor 17.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the boolean equality isFiveAlmostPrime 272 directly from the definition bigOmega n = 5.
why it matters
This supplies a verified numerical anchor inside the arithmetic-functions layer. It sits downstream of the isFiveAlmostPrime definition and supports later checks on the phi-ladder or specific constants, though no immediate parent theorems are recorded. The instance aligns with the framework's pattern of concrete checks that tie to T5–T8 forcing steps and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.