Canonical moving-prime marked row from a Schur decomposition
ProvedErdos390.Full.PaperBridgeFit.BridgeData.exists_cutoff_eventually_canonical_movingPrime_markedRow_of_schurSpliceFix physical intervals between 1 and U≥1 and a guard ledger. There is a cutoff W₀ before all subsequent head and effective-ball choices. For W≥W₀, choose nonnegative CinvOrd,Tband,targetScale,Creg, positive γslow, a finite nonempty head family supported on primes ≤W, and a ball radius and positive target margin. There is Crow≥0 chosen before the relative mesh. For every mesh with δ>0, eventually any bridge whose sample equals the guarded canonical sample, whose physical intervals are separated and whose guarded cells remain nonempty, whose partition is the canonical mesh partition, and whose scale is w=δ+η has the following property. The barycentric target has the stated positive cell-mass margin and its baseline equals the bridge baseline. Suppose the full covariance has a positive gap on the ball; a family e_z equals the actual nuisance-Schur operator; its ordinary inverse norm is at most CinvOrd; the two-stage slow variance is at least γslow w²; the compensated target is at most w·targetScale; the projected band target norm is at most Tband; and the actual regression sharp norm is at most Creg w. For any finite set of monitored band primes, the covariance between marked valuation and the target vector-field score satisfies the displayed bound throughout the ball. The constant does not depend on the mesh.
import Definitions.Def_erdos390_remaining_analytic_propositions_001 import Definitions.Def_erdos390_analytic_nonstep_certificate 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_003 import Definitions.Def_erdos390_analytic_foundations_004 import Definitions.Def_erdos390_analytic_foundations_005 universe u_1
theorem Erdos390.Full.PaperBridgeFit.BridgeData.exists_cutoff_eventually_canonical_movingPrime_markedRow_of_schurSplice : Erdos390.RemainingAnalyticGoal001_014.{u_1} := by sorry