Canonical geometry and regression coefficients for Lemma 8.6
ProvedErdos390.Full.PaperBridgeFit.BridgeData.exists_paperFineMesh_cutoff_eventually_canonical_lemma86_geometry_coefficientsFor cMesh>0 there are meshTol,Csharp,Cordinary>0, Crow≥0 and W₀, all preceding the permitted mesh. 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. If W≥W₀, δ>0, w=δ+η≤meshTol and M is permitted with constant cMesh, then eventually the canonical partition has |dev|≤w, L₁≤7w, w²≤(456/cMesh²)V, V≤4w² and V≤centerEnergy. On the same ball there is an equivalence e_z equal to the actual nuisance-Schur operator, with sharp and ordinary inverse bounds Csharp and Cordinary. Its slow residual row is bounded by Crow·wα_i. Writing Creg=2Csharp Crow, the corresponding actual regression q_z solves its literal normal equation and its compensated coefficients d_p satisfy the following bounds. This package preserves a single inverse witness throughout.
import Definitions.Def_erdos390_remaining_analytic_propositions_002 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_paperFineMesh_cutoff_eventually_canonical_lemma86_geometry_coefficients : Erdos390.RemainingAnalyticGoal002_004.{u_1} := by sorry