theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_product_le_fourthPower {N r q s t : ℕ} {z b : ℝ} (ht : t ∈ goldbachClosedPrimes N z b) (hs : s ∈ goldbachClosedPrimes N z ↑t) (hr : r ∈ goldbachClosedPrimes N z ↑s) (hq : q ∈ goldbachClosedPrimes N ↑r ↑s) : ↑(r * q * s * t) ≤ b ^ 4

Product geometry for the actual four closed prime carriers of G11, including repetitions.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_canonical_product_bounds {N r q s t : ℕ} (hN : 2 ≤ N) (ht : t ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) (hs : s ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) ↑t) (hr : r ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) ↑s) (hq : q ∈ goldbachClosedPrimes N ↑r ↑s) : ↑(r * q * s * t) ≤ ↑N ^ (16 / 33) ∧ ↑(r * q * s * t) < √↑N

The canonical G11 product stays strictly below square-root scale. This finite geometry is not a distribution or sieve upper-bound theorem.