theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProductQFiber_subset_zeroPrefix (N : ℕ) (ε : ℝ) (m : ℕ) : goldbachB10ProductQFiber N ε m ⊆ goldbachB10ProductQFiber N 0 m

Only the enlarged right-hand mother family loses its epsilon lower endpoint.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedCount_le_zeroPrefix (N : ℕ) (ε b c Z : ℝ) : goldbachB10SiftedCount N ε b c Z ≤ goldbachB10SiftedCount N 0 b c Z

Literal fibre multiplicities and the output sieve remain unchanged.