omega_eighthundredforty
plain-language theorem explainer
The arithmetic function ω counts distinct prime factors of a positive integer. For 840 the value is exactly 4, given by the primes 2, 3, 5 and 7. Researchers computing divisor sums or radical distributions inside the Recognition Science number-theory layer cite this evaluation. The proof is a one-line native_decide computation that evaluates the definition directly.
Claim. $ω(840) = 4$, where $ω(n)$ is the number of distinct prime factors of the positive integer $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The function ω is the standard little-omega that returns the count of distinct prime factors. Upstream results include the radical distribution of the rank-one Hessian metric, the structure of nuclear densities in φ-tiers, and ledger factorization in the positive reals under multiplication. These place concrete integer evaluations inside the discrete φ-ladder setting of Recognition Science.
proof idea
The proof is a one-line term that invokes native_decide to compute the value of ω at 840 directly from its definition.
why it matters
This evaluation supports the companion result sigma_zero_eighthundredforty stating that σ_0(840) = 32. It supplies a concrete arithmetic datum for radical or divisor calculations that feed into nucleosynthesis tiers and simplicial-ledger constructions. The result sits in the number-theory foothold layer that precedes applications of the Recognition Composition Law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.