theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g9_third_box_four_eq_three {N i j : ℕ} {z : ℕ × ℕ} (hz : z ∈ fouvryG9LongLabels N (5 / 4) (i, j, 4)) : z.2 = 3

The third box with rho=5/4 and index 4 contains only the integer 3.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g9_small_third_box_euler_eq_mass (N i j : ℕ) (U V : Finset ℕ) (β : ℕ → ℝ) : ∑ m ∈ U, ∑ n ∈ V, fouvryG9LongAlpha N (5 / 4) (i, j, 4) m * β n * ∏ p ∈ {3}, (1 - (LiLiuPrereqWF.progressionDensity (m * n)) p) = ∑ m ∈ U, ∑ n ∈ V, fouvryG9LongAlpha N (5 / 4) (i, j, 4) m * β n

In this third box, the actual Euler product for P={3} is exactly one on every nonzero long coefficient. This uses the actual LongAlpha, not a model.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g9_small_third_box_obstruction (N i j : ℕ) (U V : Finset ℕ) (β : ℕ → ℝ) (hpos : 0 < ∑ m ∈ U, ∑ n ∈ V, fouvryG9LongAlpha N (5 / 4) (i, j, 4) m * β n) : ¬∑ m ∈ U, ∑ n ∈ V, fouvryG9LongAlpha N (5 / 4) (i, j, 4) m * β n * ∏ p ∈ {3}, (1 - (LiLiuPrereqWF.progressionDensity (m * n)) p) ≤ LiLiuPrereqWF.g9BaseEuler {3} * (1 + 1 / (8 - 2)) ^ 3 * ∑ m ∈ U, ∑ n ∈ V, fouvryG9LongAlpha N (5 / 4) (i, j, 4) m * β n

Thus the proposed factor at L=8 is strictly too small whenever this actual third box has positive mass. This is a formal obstruction, not an unconditional counterexample claiming to instantiate the whole occupied cell.