Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual Robin Maxima on Forced Multiples

Abstract

An actual GA2 witness yields an attained Robin maximum on every divisible forced base.

For positive integers n at least three, R(n) is the existing robinRatio(n) = sigma_1(n)/(exp(gamma)nlog(log(n))). Thus G(n) = exp(gamma)*R(n), with gamma the Euler constant. The fixed positive scalar cancels from GA2, maximization, and the tail bound. C(q) denotes actualGA2(q). All logarithms are real natural logarithms.

Definition 1.1 (All positive multipliers).

Formalization. D5/S3/Arith/Robin/GA2ForcedPrimeSource.actualGA2 (✓ std3).

Source. Repository-derived.

Commentary.

The condition includes q >= 3, so every tested integer aq has positive log(log(aq)). It compares the literal divisor-sum objective for every natural multiplier a >= 1.

Theorem 1.2 (The lcm tail envelope).

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

Source. Repository-derived.

Commentary.

For any integer n >= 3 and actual GA2 integer q, the inequality holds even when n is not a multiple of q. Every denominator is positive.

Put L = lcm(q,n). The reciprocal divisor-sum identity from GoldenResourceOptimalInteger and inclusion of divisor sets give sigma_1(n)/n <= sigma_1(L)/L. Since q divides L, actual GA2 bounds R(L) by R(q). Finally L <= q*n, logarithmic monotonicity and log(1+t) <= t give the displayed explicit envelope. Its correction tends to zero as n tends to infinity with q fixed.

Theorem 1.3 (Attainment on the entire multiples domain).

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

Source. Repository-derived.

Commentary.

The base m is any natural integer at least three. It divides the supplied actual GA2 integer q. There exists N >= m divisible by m, with R(N) >= R(q), itself actual GA2, and maximizing R over every positive multiple of m.

If no multiple improves q, choose q. Otherwise a strictly better multiple and the explicit vanishing envelope bound all sufficiently large integers strictly below that witness. A finite maximum below this derived cutoff is then a maximum on the entire infinite domain. Every positive multiple of N remains a multiple of m, giving actual GA2(N). All maximizing ties are allowed. The fixed-price maximum in GoldenFutureExtensionMaximum concerns a different objective.

This proves actual attainment without assuming an unbounded GA2 supplier, RH failure, or an analytic prime estimate. The subsequent own-price insertion and permitted deletion thresholds, lcm inventory characterization, forced 5040p singleton accounting and uniform activation-loss estimate remain separate obligations. The exact finite lcm comparison must retain its same-integer terminal clock and all defect terms. The same-source signed Tpsi lower budget and formal U/GM suppliers are unresolved; the full RH/Robin/5040 inequality remains unproved.

The completed ordinary audit is a design input, not a fresh adjudication of this implementation. The mathematical module and its retained Reg mirror have passed scoped Lean compilation using only propext, Classical.choice and Quot.sound. The Reg mirror supplies the complete law equivalence, variation, whole-family sensitivity and observational dependence proofs. Raw source-occurrence binding is explicitly unfinished; no declared_validated registration is claimed. These checks cover this increment and its imports, not the whole repository or the full RH goal.

References