def G12RectangleWF.linkedEmbed (p : ℕ × ℕ) : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom

Equations

• G12RectangleWF.linkedEmbed p = ⟨p.1, p.2⟩

theorem G12RectangleWF.linkedEmbed_injective : Function.Injective linkedEmbed

theorem G12RectangleWF.rectangle_image_subset (N : ℕ) (ε : ℝ) (M T : ℕ) (hlow : ↑N ^ (4 / 53) ≤ ↑T) (hhigh : ↑(2 * T) < ↑N ^ (1 / 10)) : Finset.image linkedEmbed (G12LowRectangle.rectangle N ε M T) ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε

theorem G12RectangleWF.linked_small_test (N : ℕ) (ε Z : ℝ) : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedSmallOutputMass N ε Z = ∑ x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε, if N - x.snd * x.fst < ⌈Z⌉₊ then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N x.fst else 0

theorem G12RectangleWF.smallOutput_le (N : ℕ) (hN : 2 ≤ N) (ε Z : ℝ) (M T : ℕ) (hlow : ↑N ^ (4 / 53) ≤ ↑T) (hhigh : ↑(2 * T) < ↑N ^ (1 / 10)) : smallOutput N ε Z M T ≤ 8000 * ↑⌈Z⌉₊

Inclusion in the actual global G12 mother supplies the established 20 per-output bound; the original multiplicity restores 8000, not 20.