Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Canonical sharp-row transfer with box-independent leading constant

Proved
Erdos390.Full.PaperBridgeFit.BridgeData.boxIndependent_canonicalRaw_fullSharp

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

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

Fix a finite nonempty head family PPP, physical intervals III with lower endpoints at least one and upper endpoints at most Cmax⁡C_{\max}Cmax​, and a guard ledger at every nnn with fixed census constants Cprom,CbankC_{\rm prom},C_{\rm bank}Cprom​,Cbank​. Let C∗C_*C∗​ be the fixed box-independent prime-power constant. After choosing W>1W>1W>1 above all head primes, then Ac,Ap≥0A_c,A_p\ge0Ac​,Ap​≥0, there exist a nonnegative ϵn\epsilon_nϵn​ and threshold N0N_0N0​ such that ϵn→0\epsilon_n\to0ϵn​→0 and ϵnlog⁡log⁡n→0\epsilon_n\log\log n\to0ϵn​loglogn→0. Write G=canonicalPhysicalPowerCorrectionConstant(P,I,Cmax⁡,W,Ac)G=\mathrm{canonicalPhysicalPowerCorrectionConstant}(P,I,C_{\max},W,A_c)G=canonicalPhysicalPowerCorrectionConstant(P,I,Cmax​,W,Ac​), en=Aplog⁡Cmax⁡/log⁡ne_n=A_p\log C_{\max}/\log nen​=Ap​logCmax​/logn, and Rn=physicalPowerCorrectionRowError(en,G,n,W)R_n=\mathrm{physicalPowerCorrectionRowError}(e_n,G,n,W)Rn​=physicalPowerCorrectionRowError(en​,G,n,W). Put Ce=valuationLogCoefficient(Cmax⁡,W)C_e=\mathrm{valuationLogCoefficient}(C_{\max},W)Ce​=valuationLogCoefficient(Cmax​,W), D=canonicalGuardPerturbationConstant(P,I,AcCe)D=\mathrm{canonicalGuardPerturbationConstant}(P,I,A_cC_e)D=canonicalGuardPerturbationConstant(P,I,Ac​Ce​), and Tn=Rn+guardPowerCorrectionWeightedMajorant(Cprom,Cbank,Ce,D,n)T_n=R_n+\mathrm{guardPowerCorrectionWeightedMajorant}(C_{\rm prom},C_{\rm bank},C_e,D,n)Tn​=Rn​+guardPowerCorrectionWeightedMajorant(Cprom​,Cbank​,Ce​,D,n). Then Tnlog⁡log⁡n→0T_n\log\log n\to0Tn​loglogn→0. The estimates hold uniformly for every later finite band partition, bridge BBB, and tilt parameter ξ\xiξ at ambient n≥N0n\ge N_0n≥N0​, provided its cutoff is WWW, its sample data equal the canonical constructor with separated intervals and nonempty surviving cells, every effective prime coefficient is at most AcA_cAc​ in absolute value, and the physical coordinate has absolute value at most ApA_pAp​. Write HT=∑W<p≤⌊n2/9⌋tp/pH_T=\sum_{W<p\le\lfloor n^{2/9}\rfloor}t_p/pHT​=∑W<p≤⌊n2/9⌋​tp​/p, with tp=log⁡p/log⁡(n2/9)t_p=\log p/\log(n^{2/9})tp​=logp/log(n2/9). For every band function qqq with ∣qj∣≤1|q_j|\le1∣qj​∣≤1 and every cell iii of center cic_ici​,

C∗>0,∣fullSharpRow(q,i)−squarefreeSharpRow(q,i)∣≤3C∗(HT+1)W+3ϵn(HT/ci+1)W+Tnci.C_*>0,\qquad|\mathrm{fullSharpRow}(q,i)-\mathrm{squarefreeSharpRow}(q,i)|\le\frac{3C_*(H_T+1)}W+\frac{3\epsilon_n(H_T/c_i+1)}W+\frac{T_n}{c_i}.C∗​>0,∣fullSharpRow(q,i)−squarefreeSharpRow(q,i)∣≤W3C∗​(HT​+1)​+W3ϵn​(HT​/ci​+1)​+ci​Tn​​.

All raw analytic, guard, and physical error inputs are constructed internally; only the canonical realization and genuine coefficient box are required at use.

Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_001
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_002
import Definitions.Def_erdos390_analytic_foundations_004
import Definitions.Def_erdos390_analytic_foundations_005

universe u_1 u_3
Formal statement
theorem Erdos390.Full.PaperBridgeFit.BridgeData.boxIndependent_canonicalRaw_fullSharp : Erdos390.RemainingAnalyticGoal001_007.{u_1, u_3} := by sorry
Source
https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/Full/PaperBridgeCanonicalPowerCorrectionTriangle.lean#L567-L739

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me