CoefficientLimitRigidity

CoefficientLimitRigidity

Compactness bridge scaffold whose only public downstream output is a finite coefficient-threshold theorem.

theorem DimdPolyLEAN.positiveGauge_coercivity {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) (hF_ne : F ≠ 0) (hF_norm : ‖F‖ = 1) : ∃ (C_F : ℝ), 0 < C_F ∧ ∀ (G : Pkappa d kappa), positivePhaseGauge F (F + G) → ‖G‖ ≤ C_F * defect F G

theorem DimdPolyLEAN.lowAnnulusDefectControl {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) (hF_ne : F ≠ 0) (hF_norm : ‖F‖ = 1) (J : ℕ) : ∃ (delta_low : ℝ), 0 < delta_low ∧ ∀ {H : Pkappa d kappa} {t : ℝ}, orthogonalToPk F H → ‖H‖ = 1 → 0 < t → t ≤ 4 → highAnnulusMass J (ofPkappa kappa H) ≤ 1 / 4 → defect F (t • H) ≤ delta_low * t → lowAnnulusMass J (ofPkappa kappa H) ≤ 1 / 4