Uniform signed profiles for the full actual bridge component laws
ProvedErdos390.Full.PaperBridgeFit.BridgeData.exists_boxIndependent_actual_component_signed_profiles_compactFor 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 lower interval endpoint is at least one and every upper endpoint is at most . Fix also a nonnegative bound on the physical parameter. 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 full actual component valuation law, and the bridge parameter must also satisfy . Thus the common profile includes the valuation tilt, guard deletion, and physical tilt, while retaining the rate needed for sharp rows. The moving prime band is .
import Definitions.Def_erdos390_remaining_analytic_propositions_001 universe u_1 u_3
theorem Erdos390.Full.PaperBridgeFit.BridgeData.exists_boxIndependent_actual_component_signed_profiles_compact : Erdos390.RemainingAnalyticGoal001_010.{u_1, u_3} := by sorry