A normalized rough-head candidate lower bound

Proved

Erdos390.WholePaper.tangentRoughHeadCandidateMain_normalized_ge_three_quarters_compact

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

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

Let $W,n,K,h,u,v$ be natural numbers with $n,u,v>0$ , and let $1<r_0<2$ with $u/v\le r_0$ . Put $d=d_W$ , $P$ equal to the rough-head modulus, and $g=d(2-r_0)$ . Suppose

d\frac{Kh}{n}\le\frac g{16},\qquad \frac un(d+P)\le\frac g{16}.

Let $B=\mathrm{tangentBroadUpper}(n,K,h)$ and $M$ be the canonical rough-head candidate main term for these parameters. Then, with both quotients in the first inequality interpreted as natural division,

\lfloor n/v\rfloor\le\lfloor B/u\rfloor,\qquad \frac{3g}{4}\le\frac un M.

This turns control of moving-tail and floor losses into a positive candidate margin.

Preamble

import Definitions.Def_erdos390_remaining_analytic_propositions_008

Formal statement

theorem Erdos390.WholePaper.tangentRoughHeadCandidateMain_normalized_ge_three_quarters_compact : Erdos390.RemainingAnalyticGoal008_040 := by sorry

Source

https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/TangentPaperCleanListAbsorption.lean#L560-L731

View graph