theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_canonical_fiber_audit {N n : ℕ} (hn1 : 1 ≤ n) (hnN : n < N) : {v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) | goldbachG11LabelProd v ∣ n}.card ≤ 160000

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_exceptions_eps_zero_audit (delta : ℝ) (hdelta : 0 < delta) : ∃ (N0 : ℕ), 4 ≤ N0 ∧ ∀ (N : ℕ), N0 ≤ N → ↑(∑ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), goldbachG11RSquareCount (goldbachDifferenceCarrier N 0) v + ∑ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), goldbachG11NCount (goldbachDifferenceCarrier N 0) N v) ≤ delta * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)