Three canonical ordinary perturbation estimates
ProvedErdos390.Full.PaperBridgeFit.BridgeData.exists_cutoff_eventually_canonical_ordinary_perturbation_rowsFix Cref>0 and Rproj≥0. There is a cutoff W₀ chosen before the finite head family, physical intervals, guard ledger and effective ball. Head primes need only be at most W. For W≥W₀, 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. Physical interval endpoints lie between 1 and a fixed upper bound; guard ledgers have fixed promotion and bank parameters. The barycentric target has cell-mass margin at least a fixed positive marginFloor, and its baseline equals the bridge baseline. Conclusions are uniform on the closed effective-parameter ball of any fixed radius a ≥ 0. For an arbitrary finite nonempty band type assume ∑H_jα_j≤Rproj∑H_jα_j². Eventually, for every raw-gauge q and every band i, the squarefree/reference and full/squarefree row differences are bounded by the canonical ordinary row tolerance τ=canonicalOrdinaryRowTolerance(Cref,Rproj). The actual nuisance-Schur/full-map difference is bounded by σ=canonicalOrdinarySchurTolerance(Cref).
import Definitions.Def_erdos390_remaining_analytic_propositions_001 import Definitions.Def_erdos390_analytic_nonstep_certificate 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 u_2
theorem Erdos390.Full.PaperBridgeFit.BridgeData.exists_cutoff_eventually_canonical_ordinary_perturbation_rows : Erdos390.RemainingAnalyticGoal001_015.{u_1, u_2} := by sorry