theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_body_survives {q s t k : ℕ} (hq : Nat.Prime q) (hs : Nat.Prime s) (ht : Nat.Prime t) (hqs : q ≤ s) (hst : s ≤ t) (hk : SurvivesSieve 1 (↑q) k) : SurvivesSieve 1 (↑q) (q * s * t * k)

The three selected factors and the remaining rough cofactor form an ordinary rough body. This is independent of the Goldbach prime-output condition.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_body_minFac {q s t k : ℕ} (hq : Nat.Prime q) (hs : Nat.Prime s) (ht : Nat.Prime t) (hqs : q ≤ s) (hst : s ≤ t) (hk : SurvivesSieve 1 (↑q) k) : (q * s * t * k).minFac = q

Even with repeated selected primes, the second original prime is determined by the switched product itself. This does not identify the remaining two labels.