theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5_cofactor_prime_or_square {N n r s : ℕ} (hr : Nat.Prime r) (_hs : Nat.Prime s) (hcop : n.Coprime N) (hn : n < N) (hlarge : r * s < n) (hsecond : N ≤ s ^ 3) (hpoint : literalHPoint (N * r) (r * s) (↑s) n) : Nat.Prime (n / (r * s)) ∨ r ^ 2 ∣ n

A cofactor in the large-second-prime S5 region is prime, unless the exempted first prime occurs a second time. The square exception is retained.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Closed_cofactor_prime_or_square {N n : ℕ} {ε : ℝ} {rs : ℕ × ℕ} (hN : 2 ≤ N) (hε : 0 < ε) (hcut : ↑N ^ (2 / 3) ≤ ε * ↑N) (hrs : rs ∈ {rs ∈ goldbachS4Pairs N (↑N ^ (4 / 53)) | ↑rs.1 ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) ≤ ↑rs.2}) (hn : n ∈ goldbachDifferenceCarrier N ε) (hcop : n.Coprime N) (hpoint : literalHPoint (N * rs.1) (rs.1 * rs.2) (↑rs.2) n) : Nat.Prime (n / (rs.1 * rs.2)) ∨ rs.1 ^ 2 ∣ n

Specialization to the literal closed S5 pair filter and original difference carrier. The cutoff inequality is a scalar threshold, not a primality premise.