@[instance_reducible]

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

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachT16Coverage_pointwise_geometry {N : ℕ} {α β γ : ℝ} {rs : ℕ × ℕ} {t : ℕ} (hN : 2 ≤ N) (hαβ : α ≤ β) (_hβ : 1 / 18 < β) (hβγ : β < (1 - 3 * β) / 3) (hγ : (1 - 3 * β) / 3 < γ) (_hγu : γ < 1 / 3) (hrs : rs ∈ goldbachC10Pairs N (↑N ^ β) (↑N ^ γ)) (ht : t ∈ goldbachClosedPrimes N (↑rs.2) (goldbachC10Cutoff N rs)) : Nat.Prime rs.1 ∧ Nat.Prime rs.2 ∧ Nat.Prime t ∧ ¬rs.1 ∣ N ∧ ¬rs.2 ∣ N ∧ ¬t ∣ N ∧ ↑N ^ α ≤ ↑rs.1 ∧ ↑N ^ β ≤ ↑rs.1 ∧ ↑rs.1 ≤ ↑N ^ γ ∧ ↑N ^ γ ≤ ↑rs.2 ∧ ↑rs.1 ≤ ↑rs.2 ∧ ↑rs.1 ≤ ↑t ∧ ↑rs.2 ≤ ↑t ∧ ↑N ^ β < ↑rs.2 ∧ ↑t < ↑N ^ (1 / 3)

The literal pointwise geometry taking a genuine T16 label ((r,s),t) into the future closed-prime upper-middle carrier.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachT16Coverage_pointwise_membership {N : ℕ} {α β γ : ℝ} {rs : ℕ × ℕ} {t : ℕ} (hN : 2 ≤ N) (hαβ : α ≤ β) (hβ : 1 / 18 < β) (hβγ : β < (1 - 3 * β) / 3) (hγ : (1 - 3 * β) / 3 < γ) (hγu : γ < 1 / 3) (hrs : rs ∈ goldbachC10Pairs N (↑N ^ β) (↑N ^ γ)) (ht : t ∈ goldbachClosedPrimes N (↑rs.2) (goldbachC10Cutoff N rs)) : t ∈ goldbachClosedPrimes N (↑N ^ α) (↑N ^ (1 / 3)) ∧ rs.1 ∈ goldbachClosedPrimes N (↑N ^ α) ↑t ∧ rs.2 ∈ {s ∈ goldbachClosedPrimes N ↑rs.1 ↑t | ↑N ^ β < ↑s}

Actual membership of a T16 label in the explicit closed-prime target carrier used later for the upper-middle contribution.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightT16_le_explicitClosedPrimeTripleSum (A : Finset ℕ) (N : ℕ) {α β γ : ℝ} (hN : 2 ≤ N) (hαβ : α ≤ β) (hβ : 1 / 18 < β) (hβγ : β < (1 - 3 * β) / 3) (hγ : (1 - 3 * β) / 3 < γ) (hγu : γ < 1 / 3) : goldbachWeightT16 A N (↑N ^ β) (↑N ^ γ) ≤ ∑ t ∈ goldbachClosedPrimes N (↑N ^ α) (↑N ^ (1 / 3)), ∑ r ∈ goldbachClosedPrimes N (↑N ^ α) ↑t, ∑ s ∈ goldbachClosedPrimes N ↑r ↑t with ↑N ^ β < ↑s, literalH A (N * r) (r * s * t) ↑s

The genuine T16 contribution embeds, with label order preserved, into the explicit closed-prime triple sum that later serves as the upper-middle carrier.