Moments of the Distinct Prime-Factor Count

Abstract

The zeta-law distinct-prime count has the exact Bernoulli mean and variance.

Definition 1.1 (The distinct prime-factor count reuses Mathlib omega).

$$\mathrm{PrimeFactorCount}\left(n\right)=\mathrm{omega}\left(n\right)$$

Formalization. D5/S3/Analytic/ZetaObservation/PrimeFactorCountMoments.primeFactorCount (✓ std3).

Source. Repository-derived.

Commentary.

The named wrapper exposes FPOD’s distinct-prime count while retaining Mathlib’s totalized values at zero and one.

Definition 1.2 (A prime-support coordinate is a real indicator).

$$\mathrm{PrimeSupportIndicator}\left(p,n\right)=\mathrm{indicator}\left(0<\mathrm{factorExponent}\left(n,p\right)\right)$$

Formalization. D5/S3/Analytic/ZetaObservation/PrimeFactorCountMoments.primeSupportIndicator (✓ std3).

Source. Repository-derived.

Commentary.

The coordinate is one exactly when the selected prime has positive factorization exponent, and zero otherwise.

Theorem 1.3 (The count is the pointwise sum of support indicators).

$$\mathrm{PrimeFactorCount}\left(n\right)=\sum _{p\in \mathbb{P}}\mathrm{PrimeSupportIndicator}\left(p,n\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/ZetaObservation/PrimeFactorCountMoments.primeFactorCount_eq_tsum_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural number, factorization support is finite. The count is therefore the prime-indexed sum of its zero-one coordinates, including at zero and one.

Theorem 1.4 (The zeta-law mean is the prime evidence sum).

$$1<s\Rightarrow \mathrm{ExpectationUnderZeta}\left(s,\mathrm{PrimeFactorCount}\left(N\right)\right)=\sum _{p\in \mathbb{P}}{p}^{-s}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/ZetaObservation/PrimeFactorCountMoments.prime_factor_count_expectation (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is the full zeta-law result, not the assumption-based fallback. The repository’s zeta probability measure and Bernoulli support coordinates are reused.

Interchanging expectation and the countable sum uses the sharp summability theorem for the prime evidence series above one.

Theorem 1.5 (The variance is the sum of Bernoulli variances).

$$1<s\Rightarrow \mathrm{VarianceUnderZeta}\left(s,\mathrm{PrimeFactorCount}\left(N\right)\right)=\sum _{p\in \mathbb{P}}{p}^{-s}\cdot 1-p^{-s}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/ZetaObservation/PrimeFactorCountMoments.prime_factor_count_variance (✓ std3). ∎

Source. Repository-derived.

Commentary.

Mutual independence comes from unique factorization through the existing prime-coordinate theorem. It is not a consequence of the index type merely being countable.

The second moment separates diagonal Bernoulli terms from products of distinct coordinates. Both resulting prime series are summable when the exponent is above one.

Theorem 1.6 (Zero, one, and a prime realize the basic degeneracies).

$$\mathrm{PrimeFactorCount}\left(0\right)=0\wedge \left(\mathrm{PrimeFactorCount}\left(1\right)=0\wedge \mathrm{PrimeFactorCount}\left(p\right)=1\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/ZetaObservation/PrimeFactorCountMoments.prime_factor_count_degenerate_audit (✓ std3). ∎

Source. Repository-derived.

Commentary.

The count vanishes at zero and one and equals one at a prime. Empty and singleton finite support families are already covered by the mutual independence theorem used in the variance proof.

Theorem 1.7 (Exponent one is a named nonsummable counterexample).

$$\neg \mathrm{Summable}\left(p\mapsto p^{-1}\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/ZetaObservation/PrimeFactorCountMoments.moment_threshold_is_necessary (✓ std3). ∎

Source. Repository-derived.

Commentary.

At exponent one the reciprocal-prime evidence family is not summable, so the strict threshold in the moment theorems cannot be weakened to a non-strict inequality.

Prime distribution is load-bearing only for this analytic threshold. The Bernoulli moment algebra itself applies to any independent summable zero-one family.

References

• Truth anchor: D5/S3/Analytic/ZetaObservation/PrimeFactorCountMoments.moment_threshold_is_necessary
• Truth anchor: D5/S3/Analytic/ZetaObservation/PrimeFactorCountMoments.primeFactorCount
• Truth anchor: D5/S3/Analytic/ZetaObservation/PrimeFactorCountMoments.primeFactorCount_eq_tsum_support
• Truth anchor: D5/S3/Analytic/ZetaObservation/PrimeFactorCountMoments.primeSupportIndicator
• Truth anchor: D5/S3/Analytic/ZetaObservation/PrimeFactorCountMoments.prime_factor_count_degenerate_audit
• Truth anchor: D5/S3/Analytic/ZetaObservation/PrimeFactorCountMoments.prime_factor_count_expectation
• Truth anchor: D5/S3/Analytic/ZetaObservation/PrimeFactorCountMoments.prime_factor_count_variance
• Dependency: D5/S3/Analytic/ZetaEntropyPlane/PrimeEvidenceSharpThreshold
• Dependency: D5/S3/Analytic/ZetaObservation/MultiplicativeComplexityActivation
• Dependency: D5/S3/Analytic/ZetaObservation/PrimeSupportBernoulliIndependence