theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_audit_canonical (N : ℕ) (ε : ℝ) (hε : 0 ≤ ε) : ∑ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), goldbachG11RoughCount N ε v ≤ goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) ∧ goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) ≤ ∑ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), goldbachG11RoughCount N ε v + ∑ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), goldbachG11RSquareCount (goldbachDifferenceCarrier N ε) v + ∑ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), goldbachG11NCount (goldbachDifferenceCarrier N ε) N v

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_audit_epsilon_zero (N : ℕ) (z b : ℝ) : ∑ v ∈ goldbachG11Labels N z b, goldbachG11RoughCount N 0 v ≤ goldbachWeightG11 (goldbachDifferenceCarrier N 0) N z b ∧ goldbachWeightG11 (goldbachDifferenceCarrier N 0) N z b ≤ ∑ v ∈ goldbachG11Labels N z b, goldbachG11RoughCount N 0 v + ∑ v ∈ goldbachG11Labels N z b, goldbachG11RSquareCount (goldbachDifferenceCarrier N 0) v + ∑ v ∈ goldbachG11Labels N z b, goldbachG11NCount (goldbachDifferenceCarrier N 0) N v

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_audit_difference_ne_zero {N n : ℕ} (hn : n ∈ goldbachDifferenceCarrier N 0) : n ≠ 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_audit_cofactor_one {N p : ℕ} {ε : ℝ} {v : GoldbachG11Label} : (p, 1) ∈ goldbachG11RoughPairs N ε v ↔ Nat.Prime p ∧ ↑p < (1 - ε) * ↑N ∧ p + goldbachG11LabelProd v = N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_audit_first_diagonal (N r s t : ℕ) (z b : ℝ) : ⟨t, ⟨s, ⟨r, r⟩⟩⟩ ∈ goldbachG11Labels N z b ↔ Nat.Prime r ∧ Nat.Prime s ∧ Nat.Prime t ∧ (r * r * s * t).Coprime N ∧ z ≤ ↑r ∧ r ≤ s ∧ s ≤ t ∧ ↑t ≤ b

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_audit_middle_diagonal (N r s t : ℕ) (z b : ℝ) : ⟨t, ⟨s, ⟨r, s⟩⟩⟩ ∈ goldbachG11Labels N z b ↔ Nat.Prime r ∧ Nat.Prime s ∧ Nat.Prime t ∧ (r * s * s * t).Coprime N ∧ z ≤ ↑r ∧ r ≤ s ∧ s ≤ t ∧ ↑t ≤ b

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_audit_last_diagonal (N r q s : ℕ) (z b : ℝ) : ⟨s, ⟨s, ⟨r, q⟩⟩⟩ ∈ goldbachG11Labels N z b ↔ Nat.Prime r ∧ Nat.Prime q ∧ Nat.Prime s ∧ (r * q * s * s).Coprime N ∧ z ≤ ↑r ∧ r ≤ q ∧ q ≤ s ∧ ↑s ≤ b

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_audit_first_diagonal_exception (A : Finset ℕ) (r s t : ℕ) : goldbachG11RSquareException A ⟨t, ⟨s, ⟨r, r⟩⟩⟩ = ∅