Canonical sharp-row transfer with box-independent leading constant
ProvedErdos390.Full.PaperBridgeFit.BridgeData.boxIndependent_canonicalRaw_fullSharpFix a finite nonempty head family , physical intervals with lower endpoints at least one and upper endpoints at most , and a guard ledger at every with fixed census constants . Let be the fixed box-independent prime-power constant. After choosing above all head primes, then , there exist a nonnegative and threshold such that and . Write , , and . Put , , and . Then . The estimates hold uniformly for every later finite band partition, bridge , and tilt parameter at ambient , provided its cutoff is , its sample data equal the canonical constructor with separated intervals and nonempty surviving cells, every effective prime coefficient is at most in absolute value, and the physical coordinate has absolute value at most . Write , with . For every band function with and every cell of center ,
All raw analytic, guard, and physical error inputs are constructed internally; only the canonical realization and genuine coefficient box are required at use.
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
theorem Erdos390.Full.PaperBridgeFit.BridgeData.boxIndependent_canonicalRaw_fullSharp : Erdos390.RemainingAnalyticGoal001_007.{u_1, u_3} := by sorry