@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachDoubleDifference (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachDoubleDifference P = Classical.propDecidable P

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.survivesSieve_mul_right_cutoff_prime_iff (N r n : ℕ) (hrPrime : Nat.Prime r) : SurvivesSieve (N * r) (↑r) n ↔ SurvivesSieve N (↑r) n

At cutoff r, adjoining the prime factor r to the sieve modulus does not change which smaller primes are sifted.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH_mul_right_cutoff_prime_eq (A : Finset ℕ) (N d r : ℕ) (hrPrime : Nat.Prime r) : literalH A (N * r) d ↑r = literalH A N d ↑r

The literal count H is unchanged when the sieve modulus is replaced by N*r, provided the cutoff is exactly the prime r.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachDoubleDifference_fixed_pair (A : Finset ℕ) (N r s : ℕ) (hrPrime : Nat.Prime r) (hsPrime : Nat.Prime s) (hrs : r < s) : literalH A N (r * s) ↑r - literalH A (N * r) (r * s) ↑s = ∑ q ∈ goldbachHalfOpenPrimes N ↑r ↑s with r < q, literalH A (N * r) (r * q * s) ↑q

Fixed-pair double-difference identity HD, with the genuine middle prime range r < q < s and the literal triple divisibility fibre.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachVStrict (A : Finset ℕ) (N : ℕ) (z y : ℝ) : ℤ

The strict part of V, with the diagonal removed but the same r<s carrier as U.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachVStrict A N z y = ∑ s ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachHalfOpenPrimes N z y, ∑ r ∈ MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.siftingPrimes N ↑s with z ≤ ↑r, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A (N * r) (r * s) ↑s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachV_eq_goldbachVStrict_add_goldbachQ (A : Finset ℕ) (N : ℕ) (z y : ℝ) : goldbachV A N z y = goldbachVStrict A N z y + goldbachQ A N z y

The weakly ordered double sum splits into its strict part plus the actual diagonal Q.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachUStrict_sub_goldbachVStrict_eq_goldbachWStrict (A : Finset ℕ) (N : ℕ) (z y : ℝ) : goldbachUStrict A N z y - goldbachVStrict A N z y = goldbachWStrict A N z y

Summing the fixed-pair double-difference identities gives the strict triple sum W.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachDoubleDifference_eq_goldbachWStrict_sub_goldbachQ (A : Finset ℕ) (N : ℕ) (z y : ℝ) : goldbachUStrict A N z y - goldbachV A N z y = goldbachWStrict A N z y - goldbachQ A N z y

Exact finite H3: the strict double difference equals the strict triple sum minus the actual diagonal square term.