Uniform signed profiles for the actual guarded medium-tilted cells
ProvedErdos390.Full.PaperBridgeFit.BridgeData.exists_boxIndependent_actual_medium_signed_profilesFor a divisor , let denote the common paper divisibility main term; write and . Fix a nonempty finite head set with patterns , two fixed physical intervals , a common upper bound , and guard ledgers with fixed promotion and bank parameters. Fix containing all head primes and a nonnegative effective prime-coefficient bound . Assume each upper interval endpoint is at least one and at most . There exist a nonnegative sequence and , independent of the later choice of band index set and bridge data, such that and . For any such bridge at whose head patterns, physical endpoints, guard set, and cutoff are exactly the prescribed ones, and whose effective prime coefficients are bounded by , all component laws satisfy
for distinct moving-band primes . Here is the actual guarded medium-tilted cell law. This attaches the abstract marked profiles to the concrete bridge using only structural identifications. The moving prime band is .
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.exists_boxIndependent_actual_medium_signed_profiles : Erdos390.RemainingAnalyticGoal001_011.{u_1, u_3} := by sorry