def G12RectangleGate.linkEmbed (A : Finset (ℕ × ℕ)) : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom

Equations

• G12RectangleGate.linkEmbed A = Finset.image G12RectangleWF.linkedEmbed A

theorem G12RectangleGate.atom_data {N : ℕ} {ε : ℝ} (hN : 2 ≤ N) {x : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom} (hx : x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε) : 0 < x.fst * x.snd ∧ x.fst * x.snd < N ∧ (∀ p ∈ (x.fst * x.snd).primeFactors, ↑N ^ (4 / 53) ≤ ↑p) ∧ (x.fst * x.snd).primeFactors.card ≤ 20

All prime factors of the full product, including the short prime.

theorem G12RectangleGate.linked_mass_le {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) : ∑ x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N x.fst ≤ 20 * ↑N

Weighted global mass uses the established output-fibre bound, not injectivity.

theorem G12RectangleGate.subset_mass_le {N : ℕ} {ε : ℝ} {A : Finset (ℕ × ℕ)} (hN : 2 ≤ N) (hA : linkEmbed A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε) : ∑ p ∈ A, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 ≤ 20 * ↑N

theorem G12RectangleGate.gate_le_mass {N q : ℕ} {A : Finset (ℕ × ℕ)} {Q : Finset ℕ} {c : ℕ → ℝ} {z : ℝ} {K : ℕ} (hq : q ≤ N) (hz : 0 < z) (hQ : Q ⊆ Finset.Icc 1 q) (hc : ∀ d ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q ↑N, |c d| ≤ 1) (hpos : ∀ p ∈ A, 0 < p.1 * p.2) (hf : ∀ p ∈ A, ∀ l ∈ (p.1 * p.2).primeFactors, z ≤ ↑l) (hK : ∀ p ∈ A, (p.1 * p.2).primeFactors.card ≤ K) : |G12RectangleWF.gate N A Q c| ≤ 2 * ↑K / z * AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor N ^ 2 * ∑ p ∈ A, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1

A nonnegative finite union bound; the signed original gate is untouched.

theorem G12RectangleGate.gate_le {N q : ℕ} {ε : ℝ} {A : Finset (ℕ × ℕ)} {Q : Finset ℕ} {c : ℕ → ℝ} (hN : 2 ≤ N) (hq : q ≤ N) (hA : linkEmbed A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε) (hQ : Q ⊆ Finset.Icc 1 q) (hc : ∀ d ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q ↑N, |c d| ≤ 1) : |G12RectangleWF.gate N A Q c| ≤ 800 * ↑N / ↑N ^ (4 / 53) * (1 + Real.log ↑N) ^ 2

Full-product gcd gate, uniformly for every subset of the original linked atoms.