@[reducible, inline]

noncomputable abbrev G12FlexibleRectangle.mother (N : ℕ) (ε : ℝ) : Finset (ℕ × ℕ)

The original physical mother and discrepancy, without changing N or epsilon.

Equations

• G12FlexibleRectangle.mother = G12LowRectangle.mother

@[reducible, inline]

noncomputable abbrev G12FlexibleRectangle.discrepancy (N : ℕ) (S : Finset (ℕ × ℕ)) (Q : Finset ℕ) (c : ℕ → ℝ) : ℝ

Equations

• G12FlexibleRectangle.discrepancy = G12LowRectangle.discrepancy

@[reducible, inline]

abbrev G12FlexibleRectangle.beta (N r : ℕ) : ℝ

Equations

• G12FlexibleRectangle.beta = G12LowRectangle.beta

def G12FlexibleRectangle.longOK (N : ℕ) (ε : ℝ) (T V m : ℕ) : Prop

Safety depends only on the long variable and the actual short endpoints.

Equations

• G12FlexibleRectangle.longOK N ε T V m = (m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N ∧ V ≤ m.minFac ∧ ε * ↑N ≤ ↑T * ↑m ∧ V * m < N)

noncomputable def G12FlexibleRectangle.longSet (N : ℕ) (ε : ℝ) (M U T V : ℕ) : Finset ℕ

Equations

• G12FlexibleRectangle.longSet N ε M U T V = Finset.filter (G12FlexibleRectangle.longOK N ε T V) (Finset.Ioc M U)

def G12FlexibleRectangle.shortSet (N T V : ℕ) : Finset ℕ

Equations

• G12FlexibleRectangle.shortSet N T V = {r ∈ Finset.Ioc T V | Nat.Prime r ∧ r.Coprime N}

noncomputable def G12FlexibleRectangle.rectangle (N : ℕ) (ε : ℝ) (M U T V : ℕ) : Finset (ℕ × ℕ)

Equations

• G12FlexibleRectangle.rectangle N ε M U T V = G12FlexibleRectangle.longSet N ε M U T V ×ˢ G12FlexibleRectangle.shortSet N T V

noncomputable def G12FlexibleRectangle.alpha (N : ℕ) (ε : ℝ) (T V m : ℕ) : ℝ

Equations

• G12FlexibleRectangle.alpha N ε T V m = if G12FlexibleRectangle.longOK N ε T V m then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m else 0

noncomputable def G12FlexibleRectangle.boundary (N : ℕ) (ε : ℝ) (M U T V : ℕ) : Finset (ℕ × ℕ)

This residual is retained; no estimate is claimed for it.

Equations

• G12FlexibleRectangle.boundary N ε M U T V = G12FlexibleRectangle.mother N ε \ G12FlexibleRectangle.rectangle N ε M U T V

theorem G12FlexibleRectangle.alpha_bounds (N : ℕ) (ε : ℝ) (T V m : ℕ) : 0 ≤ alpha N ε T V m ∧ alpha N ε T V m ≤ 1

theorem G12FlexibleRectangle.alpha_tau (N : ℕ) (ε : ℝ) (M U T V m : ℕ) (hm : m ∈ Finset.Ioc M U) : |alpha N ε T V m| ≤ ↑((MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau 1) m)

def G12FlexibleRectangle.shortInterval (T V : ℕ) (hT : 1 ≤ T) (hTV : T ≤ V) (hV : V ≤ 2 * T) : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.PrimeC2Interval

The source scale remains T, even when V is arbitrarily close to T.

Equations

• G12FlexibleRectangle.shortInterval T V hT hTV hV = { scale := ↑T, lower := ↑T, upper := ↑V, one_le_scale := ⋯, scale_le_lower := ⋯, lower_le_upper := ⋯, upper_le_twice := ⋯ }

theorem G12FlexibleRectangle.shortInterval_support (T V : ℕ) (hT : 1 ≤ T) (hTV : T ≤ V) (hV : V ≤ 2 * T) : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval (shortInterval T V hT hTV hV).lower (shortInterval T V hT hTV hV).upper = Finset.Ioc T V

theorem G12FlexibleRectangle.rectangle_subset_mother (N : ℕ) (ε : ℝ) (M U T V : ℕ) (hlow : ↑N ^ (4 / 53) ≤ ↑T) (hhigh : ↑V < ↑N ^ (1 / 10)) : rectangle N ε M U T V ⊆ mother N ε

Actual endpoint geometry, not the enclosing dyadic geometry, gives coverage.

theorem G12FlexibleRectangle.local_boundary_iff (N m r M U T V : ℕ) (ε : ℝ) (h : (m, r) ∈ mother N ε) (hm : m ∈ Finset.Ioc M U) (hr : r ∈ Finset.Ioc T V) : (m, r) ∈ boundary N ε M U T V ↔ m.minFac < V ∨ ↑T * ↑m < ε * ↑N ∨ N ≤ V * m

Within a cell the physical boundary is exactly the three failed safety tests.

theorem G12FlexibleRectangle.rectangle_test (N : ℕ) (ε : ℝ) (M U T V : ℕ) (f : ℕ → ℕ → ℝ) : ∑ p ∈ rectangle N ε M U T V, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p.1 p.2 = ∑ m ∈ Finset.Ioc M U, ∑ r ∈ Finset.Ioc T V, alpha N ε T V m * beta N r * f m r

Equality with the same normalized coefficient, before any modulus summation.

theorem G12FlexibleRectangle.rectangle_signedError (N : ℕ) (ε : ℝ) (M U T V : ℕ) (Q : Finset ℕ) (c : ℕ → ℝ) : discrepancy N (rectangle N ε M U T V) Q c = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError (Finset.Ioc M U) (Finset.Ioc T V) Q (alpha N ε T V) (beta N) c ↑N

Full signed equality uses exactly the same moduli and c, preserving cancellation.

theorem G12FlexibleRectangle.mother_partition (N : ℕ) (ε : ℝ) (M U T V : ℕ) (hlow : ↑N ^ (4 / 53) ≤ ↑T) (hhigh : ↑V < ↑N ^ (1 / 10)) : Disjoint (rectangle N ε M U T V) (boundary N ε M U T V) ∧ rectangle N ε M U T V ∪ boundary N ε M U T V = mother N ε

theorem G12FlexibleRectangle.weighted_partition (N : ℕ) (ε : ℝ) (M U T V : ℕ) (hlow : ↑N ^ (4 / 53) ≤ ↑T) (hhigh : ↑V < ↑N ^ (1 / 10)) (f : ℕ × ℕ → ℝ) : 400 * ∑ p ∈ mother N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p = 400 * ∑ p ∈ rectangle N ε M U T V, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p + 400 * ∑ p ∈ boundary N ε M U T V, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p

Body multiplicity 400 remains on both the inner and residual sums.

theorem G12FlexibleRectangle.signed_partition (N : ℕ) (ε : ℝ) (M U T V : ℕ) (hlow : ↑N ^ (4 / 53) ≤ ↑T) (hhigh : ↑V < ↑N ^ (1 / 10)) (Q : Finset ℕ) (c : ℕ → ℝ) : discrepancy N (mother N ε) Q c = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError (Finset.Ioc M U) (Finset.Ioc T V) Q (alpha N ε T V) (beta N) c ↑N + discrepancy N (boundary N ε M U T V) Q c

theorem G12FlexibleRectangle.original_low_partition (N : ℕ) (ε : ℝ) (M U T V : ℕ) (hlow : ↑N ^ (4 / 53) ≤ ↑T) (hhigh : ↑V < ↑N ^ (1 / 10)) : ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)) m) * ↑{r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m | ↑r < ↑N ^ (1 / 10)}.card = (400 * ∑ p ∈ rectangle N ε M U T V, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0) + 400 * ∑ p ∈ boundary N ε M U T V, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0

The original low count splits with its full repeated-body coefficient. The old mother-to-fibre identification is reused, not reproved.

theorem G12FlexibleRectangle.dyadic_specialization (N : ℕ) (ε : ℝ) (M T : ℕ) : rectangle N ε M (2 * M) T (2 * T) = G12LowRectangle.rectangle N ε M T

The old dyadic rectangle is a specialization, not a second physical mother.

theorem G12FlexibleRectangle.mother_zero (ε : ℝ) : mother 0 ε = ∅

theorem G12FlexibleRectangle.rectangle_zero (ε : ℝ) (M U T V : ℕ) : rectangle 0 ε M U T V = ∅

theorem G12FlexibleRectangle.rectangle_empty_long (N : ℕ) (ε : ℝ) (M T V : ℕ) : rectangle N ε M M T V = ∅

theorem G12FlexibleRectangle.rectangle_empty_short (N : ℕ) (ε : ℝ) (M U T : ℕ) : rectangle N ε M U T T = ∅

theorem G12FlexibleRectangle.product_endpoint_excluded (N m r : ℕ) (ε : ℝ) (he : r * m = N) : (m, r) ∉ mother N ε