bigOmega_eq_omega_of_squarefree
plain-language theorem explainer
For nonzero squarefree natural numbers the total number of prime factors counting multiplicity equals the number of distinct prime factors. Number theorists simplifying sums or products over squarefree integers cite this identity to collapse Ω and ω. The proof is a term-mode wrapper that simplifies both sides to Mathlib cardFactors and cardDistinctFactors then invokes the squarefree characterization lemma.
Claim. For nonzero squarefree $n$, the total number of prime factors with multiplicity equals the number of distinct prime factors: $Ω(n) = ω(n)$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to related multiplicative functions for later Dirichlet inversion. bigOmega is the abbreviation for the arithmetic function that returns the total number of prime factors counting multiplicity. omega returns the number of distinct prime factors. The local setting keeps statements minimal so that deeper algebraic identities can be layered once the basic interfaces stabilize. Upstream results include the bigOmega abbreviation and the via structure from recognition-weighted stellar assembly derivations.
proof idea
The term proof first applies simp only to unfold bigOmega and omega into their underlying cardFactors and cardDistinctFactors. It then feeds the hypotheses n ≠ 0 and Squarefree n into the Mathlib lemma ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_squarefree, takes the symmetric of the resulting equality, and closes the goal.
why it matters
This identity is invoked inside liouville_eq_mobius_of_squarefree to equate the Liouville function λ(n) with the Möbius function μ(n) exactly on squarefree n. It supplies a basic reduction step in the arithmetic-functions toolkit that supports number-theoretic manipulations appearing in Recognition Science mass formulas and recognition-cost calculations. No direct connection to the T0-T8 forcing chain or the Recognition Composition Law appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.