theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67_ideal_normalized (B ρ : ℝ) (hB : 0 ≤ B) (hρ : 0 < ρ) (hρK : ρ < 53 / (2 * Real.exp Real.eulerMascheroniConstant)) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N), (53 / (2 * Real.exp Real.eulerMascheroniConstant) - ρ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) * goldbachPairIdealSum N (2 * ρ) (goldbachG6Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ goldbachPairMovingMain N hEven ε B ρ (goldbachG6Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ∧ (53 / (2 * Real.exp Real.eulerMascheroniConstant) - ρ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) * goldbachPairIdealSum N (2 * ρ) (goldbachG7Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) ≤ goldbachPairMovingMain N hEven ε B ρ (goldbachG7Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)))

Both original closed pair families consume the same scalar and coordinate threshold.