theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG6Pairs_eq_filter_product (N : ℕ) (z b : ℝ) : goldbachG6Pairs N z b = {a ∈ (goldbachClosedPrimes N z b).product (goldbachClosedPrimes N z b) | a.1 ≤ a.2}

The original nested G6 labels are exactly the closed upper triangle.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.symmetric_sum_triangle (S : Finset ℕ) (W : ℕ → ℕ → ℝ) (hW : ∀ (r s : ℕ), W r s = W s r) : 2 * ∑ a ∈ S.product S with a.1 ≤ a.2, W a.1 a.2 = ∑ r ∈ S, ∑ s ∈ S, W r s + ∑ r ∈ S, W r r

Square = twice the closed triangle minus its diagonal, for any symmetric kernel.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG6Pairs_symmetric_sum (N : ℕ) (z b : ℝ) (W : ℕ → ℕ → ℝ) (hW : ∀ (r s : ℕ), W r s = W s r) : 2 * ∑ a ∈ goldbachG6Pairs N z b, W a.1 a.2 = ∑ r ∈ goldbachClosedPrimes N z b, ∑ s ∈ goldbachClosedPrimes N z b, W r s + ∑ r ∈ goldbachClosedPrimes N z b, W r r

Exact square–triangle–diagonal identity on the original G6 labels.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG6Pairs_half_square_le (N : ℕ) (z b : ℝ) (W : ℕ → ℕ → ℝ) (hW : ∀ (r s : ℕ), W r s = W s r) (hdiag : ∀ r ∈ goldbachClosedPrimes N z b, 0 ≤ W r r) : 1 / 2 * ∑ r ∈ goldbachClosedPrimes N z b, ∑ s ∈ goldbachClosedPrimes N z b, W r s ≤ ∑ a ∈ goldbachG6Pairs N z b, W a.1 a.2

Only the diagonal must be nonnegative; off-diagonal weights may be signed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG6Pairs_product_sum (N : ℕ) (z b : ℝ) (h : ℕ → ℝ) : 2 * ∑ a ∈ goldbachG6Pairs N z b, h (a.1 * a.2) = ∑ r ∈ goldbachClosedPrimes N z b, ∑ s ∈ goldbachClosedPrimes N z b, h (r * s) + ∑ r ∈ goldbachClosedPrimes N z b, h (r ^ 2)

Product-dependent weights are symmetric without any separability assumption.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG6Pairs_product_half_square_le (N : ℕ) (z b : ℝ) (h : ℕ → ℝ) (hdiag : ∀ r ∈ goldbachClosedPrimes N z b, 0 ≤ h (r ^ 2)) : 1 / 2 * ∑ r ∈ goldbachClosedPrimes N z b, ∑ s ∈ goldbachClosedPrimes N z b, h (r * s) ≤ ∑ a ∈ goldbachG6Pairs N z b, h (a.1 * a.2)

A signed product kernel needs nonnegativity only at the square labels.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG6Pairs_totient_product_sum (N : ℕ) (z b : ℝ) (h : ℕ → ℝ) : 2 * ∑ a ∈ goldbachG6Pairs N z b, h (a.1 * a.2) / ↑(a.1 * a.2).totient = ∑ r ∈ goldbachClosedPrimes N z b, ∑ s ∈ goldbachClosedPrimes N z b, h (r * s) / ↑(r * s).totient + ∑ r ∈ goldbachClosedPrimes N z b, h (r ^ 2) / ↑(r ^ 2).totient

The totient is evaluated at the full product, including the square diagonal. The original closed-prime carrier, hence its coprimality screen, is unchanged.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG6Pairs_totient_product_half_square_le (N : ℕ) (z b : ℝ) (h : ℕ → ℝ) (hdiag : ∀ r ∈ goldbachClosedPrimes N z b, 0 ≤ h (r ^ 2)) : 1 / 2 * ∑ r ∈ goldbachClosedPrimes N z b, ∑ s ∈ goldbachClosedPrimes N z b, h (r * s) / ↑(r * s).totient ≤ ∑ a ∈ goldbachG6Pairs N z b, h (a.1 * a.2) / ↑(a.1 * a.2).totient

No off-diagonal sign condition or false totient factorization is needed.