Eventual existence of central-anchor certificates

Proved

Erdos390.WholePaper.exists_eventually_centralAnchorCertificate

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

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

For every real $c>C_0$ , there exists an integer $R\ge201$ such that every sufficiently large natural $n$ admits a central-anchor certificate. More explicitly, it gives a valid large-prime cofactor choice $q$ , its full anchor set $A\subset(n,2n]$ , and central divisor $D$ , with

\prod_{a\in A}a=\binom{2n}{n}D,\qquad D\mid T_c(n),

where $T_c(n)$ is the central tail product. Every prime divisor of $D$ is at most $2R+1$ , and for every prime $p\le2R+1$ ,

v_p(D)+\frac{c-C_0}{3(p-1)}\frac n{\log n}\le v_p(T_c(n)).

The certificate packages the exact central product together with a positive tail-valuation reserve.

Preamble

import Definitions.Def_erdos390_remaining_analytic_propositions_008
import Mathlib
import Definitions.Def_erdos390_source_bank_interface
import Definitions.Def_erdos390_dickman_step_function
import Theorems.Thm_MediumPNT
import Definitions.Def_erdos390_analytic_foundations_001
import Theorems.Thm_Erdos390_Full_DickmanBasic_kernel_product_bound
import Theorems.Thm_Erdos390_Full_DickmanBasic_rho_pos_on_zero_five
import Theorems.Thm_Erdos390_Full_DickmanBasic_kernel_secondDerivative_first_bound
import Definitions.Def_erdos390_analytic_foundations_006
import Definitions.Def_erdos390_analytic_foundations_007

Formal statement

theorem Erdos390.WholePaper.exists_eventually_centralAnchorCertificate : Erdos390.RemainingAnalyticGoal008_012 := by sorry

Source

https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/CentralAnchorExistence.lean#L70-L248

View graph