Erdos392.Factorization.lowest_score

@[blueprint  "score-lowest"  (statement := /-- One can bring any factorization into balance without increasing the score. -/)  (proof := /-- Apply strong induction on the total imbalance of the factorization and use the  previous three sublemmas.-/)  (latexEnv := "lemma")]theorem Factorization.lowest_score {n : ℕ} (f : Factorization n) (L : ℕ) :    ∃ f' : Factorization n, f'.total_imbalance = 0 ∧ f'.score L ≤ f.score L := by  induction h : f.total_imbalance using Nat.strong_induction_on generalizing f with  | _ k ih =>    obtain rfl | hk := k.eq_zero_or_pos    · exact ⟨f, h, le_refl _⟩    · have step : ∀ g : Factorization n, g.total_imbalance < k →          ∃ f' : Factorization n, f'.total_imbalance = 0 ∧ f'.score L ≤ g.score L :=        fun g hg ↦ ih g.total_imbalance (h ▸ hg) g rfl      have reduce (f₁ : Factorization n) (hlt : f₁.total_imbalance < f.total_imbalance)          (hle : f₁.score L ≤ f.score L) :          ∃ f' : Factorization n, f'.total_imbalance = 0 ∧ f'.score L ≤ f.score L :=        let ⟨f', hbal, hle'⟩ := step f₁ (h ▸ hlt); ⟨f', hbal, hle'.trans hle⟩      by_cases! h1 : ∃ p ∈ (n + 1).primesBelow, f.balance p > 0      · exact let ⟨f₁, hlt, hle⟩ := lower_score_1 f L h1; reduce f₁ hlt hle      · by_cases! h2 : ∃ p ∈ (n + 1).primesBelow, p > L ∧ f.balance p < 0        · exact let ⟨f₁, hlt, hle⟩ := lower_score_2 f L h2; reduce f₁ hlt hle        · have h3 : ∃ p ∈ (n + 1).primesBelow, p ≤ L ∧ f.balance p < 0 := by            by_contra! hc            exact hk.ne' <| h ▸ sum_eq_zero fun p hp ↦ by              have := h1 p hp              have := if hpL : p ≤ L then hc p hp hpL                else h2 p hp (lt_of_not_ge hpL)              omega          exact let ⟨f₁, hlt, hle⟩ := lower_score_3 f L h3; reduce f₁ hlt hle