theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g9_longAlpha_ne_zero_labels {N m : ℕ} {ρ : ℝ} {k : ℕ × ℕ × ℕ} (hm : fouvryG9LongAlpha N ρ k m ≠ 0) : ∃ z ∈ fouvryG9LongLabels N ρ k, z.1 * z.2 = m

A nonzero actual long coefficient supplies an actual ordered prime label.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g9_third_box_lower_of_large_witness {N : ℕ} {e ρ : ℝ} (hN : 1 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) {k : ℕ × ℕ × ℕ} (hlarge : ∃ y ∈ fouvryG9GridCell N e ρ k, ↑N ^ (1 / 3) ≤ ↑(y.1 / y.2.1)) : ↑N ^ (4 / 53) / 2 ≤ ρ ^ k.2.2

A genuine large-third witness in the cell controls the entire third box. This is a geometric premise, not a sieve-main-term premise. The current broad positive-prefix carrier does not itself supply such a witness.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g9_actual_weighted_euler_le_of_third_box {N : ℕ} {e ρ : ℝ} (hN : 1 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (k : ℕ × ℕ × ℕ) (hbig : 3 ≤ ρ ^ k.1) (hne : (fouvryG9GridCell N e ρ k).Nonempty) (h8 : 8 ≤ ↑N ^ (4 / 53)) (hthird : ↑N ^ (4 / 53) / 2 ≤ ρ ^ k.2.2) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p ∧ 2 < p) : have U := fouvryG9LongProducts N ρ k; have V := fouvryG9RectanglePrimeSupport N ρ k; have α := fouvryG9LongAlpha N ρ k; have β := fouvryG9RectangleBeta N; have L := ↑N ^ (4 / 53) / 2; ∑ m ∈ U, ∑ n ∈ V, α m * β n * ∏ p ∈ P, (1 - (LiLiuPrereqWF.progressionDensity (m * n)) p) ≤ LiLiuPrereqWF.g9BaseEuler P * (1 + 1 / (L - 2)) ^ 3 * ∑ m ∈ U, ∑ n ∈ V, α m * β n

Actual rectangle estimate, with the unresolved third-box condition exposed. All other prime support and size conditions are produced from the actual coefficients and the exact short interval. No copN is imposed on the third prime.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g9_actual_weighted_euler_le_of_large_witness {N : ℕ} {e ρ : ℝ} (hN : 1 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (k : ℕ × ℕ × ℕ) (hbig : 3 ≤ ρ ^ k.1) (hne : (fouvryG9GridCell N e ρ k).Nonempty) (h8 : 8 ≤ ↑N ^ (4 / 53)) (hlarge : ∃ y ∈ fouvryG9GridCell N e ρ k, ↑N ^ (1 / 3) ≤ ↑(y.1 / y.2.1)) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p ∧ 2 < p) : have U := fouvryG9LongProducts N ρ k; have V := fouvryG9RectanglePrimeSupport N ρ k; have α := fouvryG9LongAlpha N ρ k; have β := fouvryG9RectangleBeta N; have L := ↑N ^ (4 / 53) / 2; ∑ m ∈ U, ∑ n ∈ V, α m * β n * ∏ p ∈ P, (1 - (LiLiuPrereqWF.progressionDensity (m * n)) p) ≤ LiLiuPrereqWF.g9BaseEuler P * (1 + 1 / (L - 2)) ^ 3 * ∑ m ∈ U, ∑ n ∈ V, α m * β n

The desired actual estimate follows once a genuinely large-third cell witness is available. This is deliberately not claimed from nonemptiness alone.