noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Labels (N : ℕ) (z b c : ℝ) : Finset GoldbachG11Label

Original closed cross carrier, with coordinates t, s, r, q.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Labels N z b c = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N b c).sigma fun (_t : ℕ) => (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N z b).sigma fun (s : ℕ) => (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N z ↑s).sigma fun (r : ℕ) => MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N ↑r ↑s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Labels_sum (N : ℕ) (z b c : ℝ) (f : GoldbachG11Label → ℤ) : ∑ v ∈ goldbachG12Labels N z b c, f v = ∑ t ∈ goldbachClosedPrimes N b c, ∑ s ∈ goldbachClosedPrimes N z b, ∑ r ∈ goldbachClosedPrimes N z ↑s, ∑ q ∈ goldbachClosedPrimes N ↑r ↑s, f ⟨t, ⟨s, ⟨r, q⟩⟩⟩

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG12_eq_label_sum (A : Finset ℕ) (N : ℕ) (z b c : ℝ) : goldbachWeightG12 A N z b c = ∑ v ∈ goldbachG12Labels N z b c, literalH A (N * v.snd.snd.fst) (goldbachG11LabelProd v) ↑v.snd.snd.snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG12Labels_iff {N r q s t : ℕ} {z b c : ℝ} : ⟨t, ⟨s, ⟨r, q⟩⟩⟩ ∈ goldbachG12Labels N z b c ↔ Nat.Prime r ∧ Nat.Prime q ∧ Nat.Prime s ∧ Nat.Prime t ∧ (r * q * s * t).Coprime N ∧ z ≤ ↑r ∧ r ≤ q ∧ q ≤ s ∧ ↑s ≤ b ∧ b ≤ ↑t ∧ ↑t ≤ c

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Labels_subset_goldbachG11Labels (N : ℕ) (z b c : ℝ) : goldbachG12Labels N z b c ⊆ goldbachG11Labels N z c

Membership itself supplies all endpoint order needed for the G11 cell API.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LabelProd_pos {N : ℕ} {z b c : ℝ} {v : GoldbachG11Label} (hv : v ∈ goldbachG12Labels N z b c) : 0 < goldbachG11LabelProd v

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12RoughCount_eq_filter (N : ℕ) (ε : ℝ) (v : GoldbachG11Label) {z b c : ℝ} (hε : 0 ≤ ε) (hv : v ∈ goldbachG12Labels N z b c) : goldbachG11RoughCount N ε v = ↑{n ∈ goldbachDifferenceCarrier N ε | goldbachG11LabelProd v ∣ n ∧ SurvivesSieve 1 (↑v.snd.snd.snd) (n / goldbachG11LabelProd v)}.card

The rough count is the actual quotient-filter cardinal, not a modulus-N sieve.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12_cell_sandwich (N : ℕ) (ε : ℝ) (v : GoldbachG11Label) {z b c : ℝ} (hε : 0 ≤ ε) (hv : v ∈ goldbachG12Labels N z b c) : goldbachG11RoughCount N ε v ≤ literalH (goldbachDifferenceCarrier N ε) (N * v.snd.snd.fst) (goldbachG11LabelProd v) ↑v.snd.snd.snd ∧ literalH (goldbachDifferenceCarrier N ε) (N * v.snd.snd.fst) (goldbachG11LabelProd v) ↑v.snd.snd.snd ≤ goldbachG11RoughCount N ε v + goldbachG11RSquareCount (goldbachDifferenceCarrier N ε) v + goldbachG11NCount (goldbachDifferenceCarrier N ε) N v

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG12_roughQuotient_sandwich (N : ℕ) (ε z b c : ℝ) (hε : 0 ≤ ε) : ∑ v ∈ goldbachG12Labels N z b c, goldbachG11RoughCount N ε v ≤ goldbachWeightG12 (goldbachDifferenceCarrier N ε) N z b c ∧ goldbachWeightG12 (goldbachDifferenceCarrier N ε) N z b c ≤ ∑ v ∈ goldbachG12Labels N z b c, goldbachG11RoughCount N ε v + ∑ v ∈ goldbachG12Labels N z b c, goldbachG11RSquareCount (goldbachDifferenceCarrier N ε) v + ∑ v ∈ goldbachG12Labels N z b c, goldbachG11NCount (goldbachDifferenceCarrier N ε) N v

Both bounds retain exactly the original cross labels, including repeated primes.