Canonical squarefree slow rows converge relatively to reference rows
ProvedErdos390.Full.PaperBridgeFit.BridgeData.exists_global_cutoff_eventually_canonical_squarefreeSlowRow_sub_referenceThere is a global cutoff W₀. Choose W≥W₀, a relative mesh with δ>0, then the canonical finite head and physical data, nonnegative tilt bounds Acoef,Aphys, and an accuracy r>0. Here a canonical bridge means the guarded canonical sample at the indicated n and W, with separated physical intervals, a nonempty remainder in each cell, and the canonical mesh prime partition. The finite nonempty head family has exactly the primes at most W in each head pattern. Physical interval endpoints lie between 1 and a fixed upper bound; guard ledgers have fixed promotion and bank parameters. For all sufficiently large n, every canonical bridge with w=δ+η and every tilt ξ whose effective prime coefficients have absolute value at most Acoef and whose physical coordinate has absolute value at most Aphys satisfies the following estimate for every band. No profile or convergence assumptions are required as inputs.
import Definitions.Def_erdos390_remaining_analytic_propositions_002 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_003 import Definitions.Def_erdos390_analytic_foundations_004 import Definitions.Def_erdos390_analytic_foundations_005 universe u_1
theorem Erdos390.Full.PaperBridgeFit.BridgeData.exists_global_cutoff_eventually_canonical_squarefreeSlowRow_sub_reference : Erdos390.RemainingAnalyticGoal002_003.{u_1} := by sorry