Canonical eventual Proposition 8.7
ProvedErdos390.Full.PaperBridgeFit.BridgeData.canonical_proposition87_compactFix a positive permitted-mesh constant , physical intervals with endpoints between and , natural guard budgets , and a guard ledger at every integer . There exist a tolerance and a prime cutoff with the following property. For every , finite nonempty head-pattern family supported exactly on the primes at most , nonnegative constants , and positive cell-mass margin , there exist a positive parameter radius and , chosen before the mesh. For every permitted regular relative mesh of width with , all sufficiently large have the following property.
Every bridge built from the canonical surviving cells at , with separated physical intervals, nonempty surviving cells, canonical scale-separated partition, bridge width , and barycentric baseline of cell margin at least , admits a physically centered fixed-partition fit. Here the band displacement satisfies the envelopes; monitored primes are primes at most ; , active mass , and each initial marked error is at most . The finite frozen layer has ambient weights in , frozen and active sample weights bounded respectively by and , separated head patterns, and integer quota equal to frozen mass plus . In the source's notation, the conclusion is
The fit is the source's bundled path certificate, including its displacement, invariance, marked-moment and feasibility requirements. The order of choices makes the analytic constants uniform before the eventual sample size.
import Definitions.Def_erdos390_remaining_analytic_propositions_001 universe u_1 u_2
theorem Erdos390.Full.PaperBridgeFit.BridgeData.canonical_proposition87_compact : Erdos390.RemainingAnalyticGoal001_009.{u_1, u_2} := by sorry