noncomputable def G12FlexibleWF.sieve (N : ℕ) (hEven : Even N) (A : Finset (ℕ × ℕ)) (Z : ℝ) : BoundingSieve

The finite pushforward uses the physical weights and inherits the B10 density.

Equations

• G12FlexibleWF.sieve N hEven A Z = { support := Finset.image (fun (p : ℕ × ℕ) => N - p.2 * p.1) A, prodPrimes := (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve N hEven 0 0 0 Z (G12FlexibleWF.mass N A)).prodPrimes, prodPrimes_squarefree := ⋯, weights := fun (n : ℕ) => ∑ p ∈ A with N - p.2 * p.1 = n, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1, weights_nonneg := ⋯, totalMass := (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve N hEven 0 0 0 Z (G12FlexibleWF.mass N A)).totalMass, nu := (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve N hEven 0 0 0 Z (G12FlexibleWF.mass N A)).nu, nu_mult := ⋯, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

theorem G12FlexibleWF.sieve_totalMass (N : ℕ) (hEven : Even N) (A : Finset (ℕ × ℕ)) (Z : ℝ) : (sieve N hEven A Z).totalMass = mass N A

theorem G12FlexibleWF.sieve_test (N : ℕ) (hEven : Even N) (A : Finset (ℕ × ℕ)) (Z : ℝ) (P : ℕ → Prop) [DecidablePred P] : ∑ n ∈ (sieve N hEven A Z).support with P n, (sieve N hEven A Z).weights n = ∑ p ∈ A, if P (N - p.2 * p.1) then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 else 0

theorem G12FlexibleWF.sieve_rem (N : ℕ) (hEven : Even N) (A : Finset (ℕ × ℕ)) (Z : ℝ) {d : ℕ} (hd : d ∣ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z) : BoundingSieve.rem d = residue N A d

theorem G12FlexibleWF.smallOutput_le (N : ℕ) (hN : 2 ≤ N) (ε Z : ℝ) (A : Finset (ℕ × ℕ)) (hA : Finset.image G12RectangleWF.linkedEmbed A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε) : smallOutput N A Z ≤ 8000 * ↑⌈Z⌉₊

Any genuine global subfamily inherits the established small-output bound.

theorem G12FlexibleWF.rectangle_safe (N : ℕ) (ε : ℝ) (M U T V : ℕ) (p : ℕ × ℕ) (hp : p ∈ G12FlexibleRectangle.rectangle N ε M U T V) : p.2 * p.1 < N

The actual upper endpoint V, not 2T, supplies subtraction safety.

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

theorem G12FlexibleWF.exists_rectangle_full_sieve : ∃ (K : ℝ) (C : ℝ), 1 < K ∧ 0 < C ∧ ∀ (η : ℝ), 0 < η → η < 1 / 8 → ∃ (Q₀ : ℝ), 4 ≤ Q₀ ∧ ∀ (Q : ℝ), Q₀ ≤ Q → ∀ (N : ℕ), 2 ≤ N → Even N → ∀ (ε Z : ℝ) (M U T V : ℕ), ↑N ^ (4 / 53) ≤ ↑T → ↑V < ↑N ^ (1 / 10) → 2 ≤ Z → Z ≤ √Q → have A := G12FlexibleRectangle.rectangle N ε M U T V; have P := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z; have D := MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η; have Euler := ∏ p ∈ P, (1 - AnalyticNumberTheory.Sieve.goldbachNu p); have E := C * (η + (η ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3))); (∀ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true P D η Z, MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable (MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true P D η Z t) Q ∧ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable 1 Q fun (d : ℕ) => (MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true P D η Z t) d) ∧ (400 * ∑ p ∈ A, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0) ≤ (400 * mass N A * Euler * (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log Q / Real.log Z) + E) + 400 * ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true P D η Z, have c := MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true P D η Z t; G12FlexibleRectangle.discrepancy N A (Finset.Ioc 0 ⌊Q⌋₊) ⇑c - G12RectangleWF.gate N A (Finset.Ioc 0 ⌊Q⌋₊) ⇑c - outsidePrimorial N A Z Q ⇑c) + 8000 * ↑⌈Z⌉₊

Arbitrarily thin actual rectangles consume the same external family on the full original modulus interval. Both signed transport corrections are retained.

theorem G12FlexibleWF.family_C2_bound (A : ℕ) {Cscale ζ : ℝ} (hCscale : 1 ≤ Cscale) (hζ : 0 < ζ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M U T V : ℕ), 1 ≤ M → M ≤ U → U ≤ 2 * M → 1 ≤ T → T ≤ V → V ≤ 2 * T → ∀ (ν : ℝ), 4 * ↑M * ↑T = x → ζ ≤ ν → ν ≤ 1 / 10 + ζ / 10 → ↑T = x ^ ν → ∀ (N : ℕ), 0 < N → ↑N ≤ Cscale * x → ∀ (ε η Z : ℝ) (t : List ℕ), have Q := x ^ ((5 - 5 * ν) / 9 - ζ); have c := MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z t; MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable c Q → |G12FlexibleRectangle.discrepancy N (G12FlexibleRectangle.rectangle N ε M U T V) (Finset.Ioc 0 ⌊Q⌋₊) ⇑c| ≤ x / Real.log x ^ A

Each actual external member is passed unchanged to the flexible C2 producer.