bigOmega_factorial_five
plain-language theorem explainer
The total number of prime factors of 5! counted with multiplicity equals 5. Number theorists checking concrete evaluations of arithmetic functions would cite this instance. The proof is a one-line wrapper that invokes native_decide to compute the factorization of 120 directly.
Claim. $Ω(5!) = 5$, where $Ω(n)$ is the sum of exponents in the prime factorization of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The bigOmega function is introduced via its definition and apply lemmas as the total prime factor count with multiplicity. This theorem evaluates the function at the concrete input 5 factorial. Upstream results supply auxiliary constants such as the active edge count A per fundamental tick and coherence energy units, though the present computation stands apart from those structures.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic function on the fixed natural number 120.
why it matters
The declaration supplies a verified concrete value for the bigOmega function inside the arithmetic functions module. No parent theorems appear in the used_by list. It fills a basic evaluation slot in the primes layer without direct reference to the forcing chain steps T5 through T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.