Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Edge Propagation of Robin’s Inequality Along Prime Fibres

Abstract

A multiplicative edge test carries Robin’s inequality, its first layer controls a whole prime fibre, and prime replacement keeps it.

Write Z(n)=sigma(n)/n and RobinAt(n) for Z(n)<exp(gamma)log(log(n)). For a step n -> nm the edge test EdgeTest(n,m) asks that (Z(n*m)/Z(n)-1)log(log(n)) <= log(1+log(m)/log(n)). Since log(log(nm))=log(log(n))+log(1+log(m)/log(n)), the test says that the relative increase of Z, weighted by log(log(n)), is paid by the increase of the double logarithm. It discards the existing Robin slack at n, so it is sufficient for propagation and not necessary.

Theorem 1.1 (Positivity of the normalized divisor sum).

Lean statement: D5/S3/Arith/Robin/PrimeFiberPropagation.divisorRatio_pos

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/PrimeFiberPropagation.divisorRatio_pos (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural n with n!=0, divisorRatio(n)>0. The numerator sigma(1,n) and the denominator n are both positive. This permits logarithmic product identities at arbitrary positive arithmetic corners; no coprimality condition is needed for positivity.

Theorem 1.2 (A passing edge carries Robin’s inequality).

Lean statement: D5/S3/Arith/Robin/PrimeFiberPropagation.robinAt_mul_of_edgeTest

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/PrimeFiberPropagation.robinAt_mul_of_edgeTest (✓ std3). ∎

Source. Repository-derived.

Commentary.

For naturals n>1 and m>0, RobinAt(n) and EdgeTest(n,m) imply RobinAt(nm). The multiplier m is arbitrary; m=q^r gives the step along one prime direction. With rho=Z(nm)/Z(n)>0 the test gives rholog(log(n)) <= log(log(nm)). Robin at n forces log(log(n))>0, and multiplying the strict inequality by rho gives Z(nm)=rhoZ(n)<exp(gamma)log(log(nm)).

No estimate on sigma beyond its positivity is used. The statement does not decide whether a given edge passes; that is a separate numerical or analytic question.

Theorem 1.3 (The divisor sum at the next prime power).

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/PrimeFiberPropagation.sigma_prime_pow_succ (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every prime natural q and natural a, sigma(1,q^(a+1)) equals q*sigma(1,q^a)+1. The geometric divisor sum gives this recurrence; sigma_mul_prime uses it to compare consecutive prime layers.

Theorem 1.4 (The first layer of a prime fibre controls every later layer).

Lean statement: D5/S3/Arith/Robin/PrimeFiberPropagation.edgeTest_mul_prime_pow

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/PrimeFiberPropagation.edgeTest_mul_prime_pow (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let q be prime and let n satisfy log(n)>=3. If EdgeTest(n,q) holds, then EdgeTest(nq^k,q) holds for every k. The excess of one more factor q is exactly Z(nq)/Z(n)-1=1/(qsigma(q^a)) with a the exponent of q in n, from sigma multiplicativity and sigma(q^(a+1))=qsigma(q^a)+1. The next excess is therefore at most the present one divided by q.

Put L=log(n) and l=log(q). The step uses log(1+l/L)<=l/L, log(L+l)<=log(L)+l/L, log(1+l/(L+l))>=l/(L+2l), log(L)>=1, and (L+l)(L+2l)<=L^2*(1+l+l^2/2)<=L^2*exp(l), the middle inequality using L>=3. Together they turn the test at scale L into the test at scale L+l. No restriction q>7 is needed; every prime direction behaves the same way.

Theorem 1.5 (Robin’s inequality along a whole prime fibre).

Lean statement: D5/S3/Arith/Robin/PrimeFiberPropagation.robinAt_mul_prime_pow

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/PrimeFiberPropagation.robinAt_mul_prime_pow (✓ std3). ∎

Source. Repository-derived.

Commentary.

If q is prime, log(n)>=3, RobinAt(n) holds and EdgeTest(n,q) passes, then RobinAt(nq^k) holds for all k. Induction combines the two theorems above; log(nq^k)>=log(n)>=3 keeps every layer in the domain of the fibre step.

Combined with the frozen seven-smooth theorem, every certified seven-smooth core B>5040 whose first q-layer passes the test certifies the whole fibre Bq^k. The test can fail where Robin still holds: for B=27440=2^457^3 and q=11 the first layer fails numerically, while 301840=2744011 satisfies Robin with margin. Most integers have seven-smooth part at most 5040 and are not reached from that core at all. The theorem therefore reduces each prime fibre to its first layer; it does not prove Robin’s inequality for all n>5040, and the Riemann hypothesis remains open.

Theorem 1.6 (Replacing a prime by a larger prime keeps Robin’s inequality).

Lean statement: D5/S3/Arith/Robin/PrimeFiberPropagation.robinAt_prime_replace

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/PrimeFiberPropagation.robinAt_prime_replace (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let p<=q be primes, neither dividing m, and a any exponent. If RobinAt(p^am) holds, then Z(q^am)<exp(gamma)log(log(q^am)). The normalized divisor-sum factorization of ExponentExchange.IntegerSwap gives Z(r^am)=G_r(a)Z(m) with G_r(a) the sum of r^(-i) for i<=a. Each term of G_q(a) is at most the matching term of G_p(a), so the divisor ratio does not increase, while q^am>=p^am makes the double logarithm no smaller.

Repeating the replacement from the largest prime down moves a certified exponent pattern 2^a13^a25^a3*… to every integer q1^a1q2^a2q3^a3*… with distinct primes q1<q2<q3<… . Starting from the seven-smooth and eleven-smooth theorems, every integer above 5040 with at most five distinct primes whose compression to the first primes exceeds 5040 is certified this way. A compression at most 5040 needs a separate argument, and integers with six or more distinct primes are not reached.

References