theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Labels_eq_filter (N : ℕ) (z b c : ℝ) : goldbachG12Labels N z b c = {v ∈ goldbachG11Labels N z c | ↑v.snd.fst ≤ b ∧ b ≤ ↑v.fst}

The original three-low/one-high labels are exactly a restriction of the parameterized G11 labels, not an enlargement of the count.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12_switch_predicate (v : GoldbachG11Label) (k : ℕ) (b : ℝ) : ↑(goldbachG11SwitchedBodyOf v k).snd.fst ≤ b ∧ b ≤ ↑(goldbachG11SwitchedBodyOf v k).fst ↔ ↑v.snd.fst ≤ b ∧ b ≤ ↑v.fst

The cross restriction does not depend on the rough cofactor k.

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

Same switched body type, with both cross endpoints retained.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12CrossSwitchedBodies N z b c = {u ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodies N z c | ↑u.snd.fst ≤ b ∧ b ≤ ↑u.fst}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG12CrossSwitchedBodies_iff {N t s q k : ℕ} {z b c : ℝ} : ⟨t, ⟨s, ⟨q, k⟩⟩⟩ ∈ goldbachG12CrossSwitchedBodies N z b c ↔ Nat.Prime q ∧ Nat.Prime s ∧ Nat.Prime t ∧ (q * s * t).Coprime N ∧ z ≤ ↑q ∧ q ≤ s ∧ ↑s ≤ b ∧ b ≤ ↑t ∧ ↑t ≤ c ∧ 1 ≤ k ∧ k ≤ N ∧ SurvivesSieve 1 (↑q) k ∧ q * s * t * k < N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12RoughSum_eq_crossSwitched (N : ℕ) (ε z b c : ℝ) : ∑ v ∈ goldbachG12Labels N z b c, goldbachG11RoughCount N ε v = ∑ u ∈ goldbachG11SwitchedBodies N z c with ↑u.snd.fst ≤ b ∧ b ≤ ↑u.fst, ↑(goldbachG11FirstPrimeFiber N ε z u).card

Exact finite switch of the original cross rough sum. No restrictions on N, epsilon, or endpoint order are needed; the output-prime fibre is unchanged.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12RoughSum_eq_crossSwitchedBodies (N : ℕ) (ε z b c : ℝ) : ∑ v ∈ goldbachG12Labels N z b c, goldbachG11RoughCount N ε v = ∑ u ∈ goldbachG12CrossSwitchedBodies N z b c, ↑(goldbachG11FirstPrimeFiber N ε z u).card