Uniform Divisor Weight Transfer

Abstract

Factorial congruences preserve relative normalized divisor weights uniformly on exponential height bounds.

Definition 1.1 (High-prime divisor weight).

$$\forall m,n\in \mathbb{N},0<n\Rightarrow H\left(m,n\right)=\prod _{p\mid n,\mathrm{Prime}\left(p\right),m<p}z\left(p,v\left(p,n\right)\right)\wedge \forall m\in \mathbb{N},H\left(m,0\right)=1$$

Formalization. D5/S3/Arith/FibonacciAtomic/UniformDivisorWeightTransfer.highWeight (✓ std3).

Source. Repository-derived.

Commentary.

For positive n, H(m,n) is the product of reciprocal geometric sums z(p,v)=sum(i=0..v) p^(-i) over prime divisors p of n greater than m. The exponent v(p,n) is the natural prime factorization exponent. The value H(m,0) is one.

Definition 1.2 (Complete Euler product).

$$\forall x\in \mathbb{R},P\left(x\right)=\prod _{0<p\le \lfloor x\rfloor ,\mathrm{Prime}\left(p\right)}(1-\frac{1}{p}{)}^{-1}$$

Formalization. D5/S3/Arith/FibonacciAtomic/UniformDivisorWeightTransfer.primeProduct (✓ std3).

Source. Repository-derived.

Commentary.

P(x) is the product of (1-1/p)^(-1) over positive primes p at most the natural floor of the real cutoff x. The natural floor is zero when x is negative.

Definition 1.3 (Normalized divisor weight).

$$\forall n\in \mathbb{N},0<n\Rightarrow Z\left(n\right)=\frac{\mathrm{sigma}\left(n\right)}{n}\wedge Z\left(0\right)=0$$

Formalization. D5/S3/Arith/FibonacciAtomic/UniformDivisorWeightTransfer.normalizedWeight (✓ std3).

Source. Repository-derived.

Commentary.

For a positive natural n, Z(n) is the sum of positive divisors of n divided by n. The value at zero is zero, following real division by zero in the formal definition.

Definition 1.4 (Uniform relative error).

$$\forall C\in \mathbb{R},\forall m\in \mathbb{N},U\left(C,m\right)={\sup }_{a,b\in \mathbb{N},0<a,0<b,a,b\le \exp \left(Cm\log \left(m\right)\right),a\equiv b(\mathrm{mod}m!)}\left|\frac{Z\left(a\right)}{Z\left(b\right)}-1\right|$$

Formalization. D5/S3/Arith/FibonacciAtomic/UniformDivisorWeightTransfer.uniformError (✓ std3).

Source. Repository-derived.

Commentary.

U(C,m) is the supremum of the absolute relative errors over positive integers a,b bounded by exp(Cmlog(m)) and congruent modulo m!. The real supremum of an empty admissible set is defined as zero.

Theorem 1.5 (Cutoff envelope and uniform congruence transfer).

$$(\forall m,n\in \mathbb{N},m\ge 2\wedge 0<n\Rightarrow \forall X\in \mathbb{R},m\le X\Rightarrow 1\le H\left(m,n\right)\le \frac{P\left(X\right)}{P\left(m\right)}\exp \left(\frac{\log \left(n\right)}{(X-1)\log \left(X\right)}\right))\wedge (\forall C\in \mathbb{R},0<C\Rightarrow \forall epsilon\in \mathbb{R},0<epsilon\Rightarrow \exists M\in \mathbb{N},\forall m\in \mathbb{N},M\le m\Rightarrow \forall a,b\in \mathbb{N},0<a,0<b,a\le \exp \left(Cm\log \left(m\right)\right),b\le \exp \left(Cm\log \left(m\right)\right),a\equiv b(\mathrm{mod}m!)\Rightarrow \left|\frac{Z\left(a\right)}{Z\left(b\right)}-1\right|<epsilon)\wedge (\forall C\in \mathbb{R},0<C\Rightarrow \underset{m\to \infty }{\lim }U\left(C,m\right)=0)$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/UniformDivisorWeightTransfer.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural m >= 2 and positive natural n, every real cutoff X >= m gives the first bound. Write Z(n)=sigma(n)/n, where sigma is the sum of positive divisors. For every fixed positive real C, every positive epsilon admits a natural threshold M. All m >= M and positive a,b bounded by exp(Cmlog(m)) and congruent modulo m! then satisfy the second bound. This is the epsilon form of the third conclusion: U(C,m) tends to zero as m tends to infinity.

Split the actual prime divisors above m at X. Complete the product on m < p <= X to P(X)/P(m). Above X, each logarithmic Euler factor is at most 1/(X-1), and the number of distinct prime divisors is at most log(n)/log(X). The divisor-sum product splits into its small and high prime factors. Set X=m*(log(m))^2. Mertens’ product estimate and log(X)/log(m) tending to one make the complete interval product tend to one. The height bound makes the remaining exponential factor tend to one uniformly. The factorial congruence squeeze controls the small factors; applying the same bounds to a and b in both orders gives the absolute relative error bound.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/UniformDivisorWeightTransfer.highWeight
• Truth anchor: D5/S3/Arith/FibonacciAtomic/UniformDivisorWeightTransfer.normalizedWeight
• Truth anchor: D5/S3/Arith/FibonacciAtomic/UniformDivisorWeightTransfer.primeProduct
• Truth anchor: D5/S3/Arith/FibonacciAtomic/UniformDivisorWeightTransfer.result
• Truth anchor: D5/S3/Arith/FibonacciAtomic/UniformDivisorWeightTransfer.uniformError
• Dependency: D5/S3/Arith/FibonacciAtomic/ModularDivisorWeightTransfer