theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedOrdered_cofactor_geometry {N : ℕ} (hN : 4 ≤ N) {ρ : ℝ} (hρ : 1 ≤ ρ) (hρu : ρ ≤ 5 / 4) {v : GoldbachG11Label} (hv : v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) : have y := ρ ^ 2 * ↑N / ↑(goldbachG11LabelProd v); ↑N ^ (1 / 2) ≤ y ∧ y ≤ ↑N ^ 2 ∧ ↑N ^ (4 / 53) ≤ ↑v.snd.snd.snd ∧ ↑v.snd.snd.snd ≤ ↑N ^ (4 / 33) ∧ 17 / 4 ≤ Real.log y / Real.log ↑v.snd.snd.snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedRoughMass_le_sharpKernel (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ρ : ℝ), 1 ≤ ρ → ρ ≤ 5 / 4 → ∀ (h : ℝ → ℝ), (∀ (r : ℝ), 0 ≤ h r) → Real.log ↑N / ↑N * goldbachG11ExpandedRoughMass N ρ h ≤ ρ ^ 2 * (561522 / 1000000 + η) * goldbachG11PrimeKernel h N

Weighted original labelled mother, with its enlarged product endpoint, consumes the already proved sharp omega constant on its unchanged valid domain.