Canonical nuisance-residual slow row at the paper scale
ProvedErdos390.Full.PaperBridgeFit.BridgeData.exists_global_cutoff_eventually_canonical_nonstepSlowResidualRow_le_compactThere exist CF,Cprod≥0 and W₀≥2, preceding the mesh and finite canonical data. Here a canonical bridge means the guarded canonical sample at the indicated n and W, with separated physical intervals, a nonempty remainder in each cell, and the canonical mesh prime partition. The finite nonempty head family has exactly the primes at most W in each head pattern. Physical interval endpoints lie between 1 and a fixed upper bound; guard ledgers have fixed promotion and bank parameters. The barycentric target has cell-mass margin at least a fixed positive marginFloor, and its baseline equals the bridge baseline. Conclusions are uniform on the closed effective-parameter ball of any fixed radius a ≥ 0. For W≥W₀, δ>0 and w=δ+η, eventually every band row of the slow score after the canonical nuisance regression satisfies the displayed bound, uniformly on the effective ball. Here R_res denotes normalizedBandCovarianceRow applied to nuisanceResidualScore(slowScore). This is the right-hand row estimate used in Lemma 8.6.
import Definitions.Def_erdos390_remaining_analytic_propositions_002 universe u_1
theorem Erdos390.Full.PaperBridgeFit.BridgeData.exists_global_cutoff_eventually_canonical_nonstepSlowResidualRow_le_compact : Erdos390.RemainingAnalyticGoal002_002.{u_1} := by sorry