Uniform signed profiles for the actual guarded medium-tilted cells
ProvedErdos390.Full.PaperBridgeFit.BridgeData.exists_boxIndependent_actual_medium_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 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 universe u_1 u_3
theorem Erdos390.Full.PaperBridgeFit.BridgeData.exists_boxIndependent_actual_medium_signed_profiles_compact : Erdos390.RemainingAnalyticGoal001_011.{u_1, u_3} := by sorry