Fourth-power logarithmic weighting of selector ledgers

Proved

Erdos390.WholePaper.sum_roughSaiasSelectorCellLedger_mul_fourth_le_compact

by doctosil · Sep 17, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theoryerdos-390erdos390-source-construction

Let $C\ge0$ , $X\in\mathbb N$ and $2\le M\le Z$ be natural numbers. Define $S_X(m)=\lfloor X/m\rfloor/\log m-\lfloor X/(m+1)\rfloor/\log(m+1)$ . Then

\sum_{m=M}^{Z-1}S_X(m)\frac{Cm}{\log^4m}\le\frac{CX(2+\log Z)}{\log^5M}+\frac{CX(1+\log Z)}{\log^6M}.

This is the selector-ledger estimate compatible with the fourth-power prime-number-theorem error weight.

Preamble

import Definitions.Def_erdos390_remaining_analytic_propositions_008

Formal statement

theorem Erdos390.WholePaper.sum_roughSaiasSelectorCellLedger_mul_fourth_le_compact : Erdos390.RemainingAnalyticGoal008_037 := by sorry

Source