four_almost_prime_onehundredthirtysix
plain-language theorem explainer
The declaration confirms that 136 factors as 2^3 times 17 and therefore meets the four-almost-prime predicate with exactly four prime factors counted with multiplicity. Number theorists verifying small cases inside the Recognition Science arithmetic layer would cite this concrete instance when checking integers near the alpha band. The proof reduces to a single native_decide call that evaluates the bigOmega predicate directly on the input.
Claim. $136 = 2^3 17$ and therefore satisfies $Omega(136) = 4$, 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 and extending to bigOmega. The predicate isFourAlmostPrime n holds exactly when bigOmega n equals 4. The local setting is described in the module documentation as providing small wrappers around Mathlib's arithmetic function library for later Dirichlet algebra and inversion work.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate isFourAlmostPrime on the concrete value 136.
why it matters
This instance supports verification of small integers in the Recognition Science number-theory scaffolding, noting the factor 17 as RS-relevant. It contributes to the arithmetic-function layer that underpins Möbius inversion but has no downstream uses recorded. No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.