noncomputable def G12LowRectangle.mother (N : ℕ) (ε : ℝ) : Finset (ℕ × ℕ)

The physical low-r mother before testing primality of the output. The upper product endpoint is strict; the body multiplicity is not collapsed.

Equations

• G12LowRectangle.mother N ε = {p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N ×ˢ Finset.range (N + 1) | Nat.Prime p.2 ∧ p.2.Coprime N ∧ ↑N ^ (4 / 53) < ↑p.2 ∧ p.2 ≤ p.1.minFac ∧ ε * ↑N < ↑p.2 * ↑p.1 ∧ p.2 * p.1 < N ∧ ↑p.2 < ↑N ^ (1 / 10)}

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

Long-only safety filter: every short point in (T,2T] stays in the curves.

Equations

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

noncomputable def G12LowRectangle.longSet (N : ℕ) (ε : ℝ) (M T : ℕ) : Finset ℕ

Equations

• G12LowRectangle.longSet N ε M T = Finset.filter (G12LowRectangle.longOK N ε T) (Finset.Ioc M (2 * M))

def G12LowRectangle.shortSet (N T : ℕ) : Finset ℕ

Equations

• G12LowRectangle.shortSet N T = {r ∈ Finset.Ioc T (2 * T) | Nat.Prime r ∧ r.Coprime N}

noncomputable def G12LowRectangle.rectangle (N : ℕ) (ε : ℝ) (M T : ℕ) : Finset (ℕ × ℕ)

Equations

• G12LowRectangle.rectangle N ε M T = G12LowRectangle.longSet N ε M T ×ˢ G12LowRectangle.shortSet N T

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

This coefficient is independent of the short variable and the modulus.

Equations

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

def G12LowRectangle.beta (N r : ℕ) : ℝ

Equations

• G12LowRectangle.beta N r = if r.Coprime N then MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta r else 0

noncomputable def G12LowRectangle.discrepancy (N : ℕ) (S : Finset (ℕ × ℕ)) (Q : Finset ℕ) (c : ℕ → ℝ) : ℝ

Exact signed finite discrepancy; no absolute value is taken inside either sum.

Equations

• G12LowRectangle.discrepancy N S Q c = ∑ d ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q ↑N, c d * ((∑ p ∈ S, if ↑p.1 * ↑p.2 ≡ ↑N [ZMOD ↑d] then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 else 0) - (∑ p ∈ S, if (p.1 * p.2).Coprime d then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 else 0) / ↑d.totient)

noncomputable def G12LowRectangle.boundary (N : ℕ) (ε : ℝ) (M T : ℕ) : Finset (ℕ × ℕ)

The explicit unprocessed boundary, not an analytic error hypothesis.

Equations

• G12LowRectangle.boundary N ε M T = G12LowRectangle.mother N ε \ G12LowRectangle.rectangle N ε M T

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

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

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

def G12LowRectangle.shortInterval (T : ℕ) (hT : 1 ≤ T) : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.PrimeC2Interval

A dyadic interval in the exact C2 interval family.

Equations

• G12LowRectangle.shortInterval T hT = { scale := ↑T, lower := ↑T, upper := 2 * ↑T, one_le_scale := ⋯, scale_le_lower := ⋯, lower_le_upper := ⋯, upper_le_twice := ⋯ }

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

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

Exact inner coverage, with only explicit endpoint geometry as assumptions.

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

The filtered product really has the same long coefficient as C2.

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

Signed discrepancy equality preserves cancellation across all moduli.

theorem G12LowRectangle.rectangle_C2_input (N : ℕ) (ε : ℝ) (M T : ℕ) (hT : 1 ≤ T) (Q : Finset ℕ) (c : ℕ → ℝ) : discrepancy N (rectangle N ε M T) Q c = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError (Finset.Ioc M (2 * M)) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval (shortInterval T hT).lower (shortInterval T hT).upper) Q (alpha N ε T) (fun (r : ℕ) => if r.Coprime N then MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta r else 0) c ↑N

This is the literal C2 input, not a tuplewise absolute-error majorant.

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

Every atom is either in the certified rectangle or in the displayed boundary.

theorem G12LowRectangle.mem_boundary (N : ℕ) (ε : ℝ) (M T m r : ℕ) : (m, r) ∈ boundary N ε M T ↔ (m, r) ∈ mother N ε ∧ ¬(M < m ∧ m ≤ 2 * M ∧ longOK N ε T m ∧ T < r ∧ r ≤ 2 * T ∧ Nat.Prime r ∧ r.Coprime N)

Exact boundary membership displays each failed long-only safety condition.

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

Any real test, including the output-prime indicator, has this exact partition.

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

The boundary discrepancy is retained with its sign, not asserted to be small.

theorem G12LowRectangle.mother_output_iff (N m r : ℕ) (ε : ℝ) : (m, r) ∈ mother N ε ∧ Nat.Prime (N - r * m) ↔ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N ∧ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m ∧ ↑r < ↑N ^ (1 / 10)

Literal correspondence with the original first-prime fibre, including its output-prime test. No ambient-size hypothesis or new primality of k is required.

theorem G12LowRectangle.restore_multiplicity (N : ℕ) (S : Finset (ℕ × ℕ)) (f : ℕ × ℕ → ℝ) : 400 * ∑ p ∈ S, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p = ∑ p ∈ S, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)) p.1) * f p

All original repeated body representations are restored, for any test.

theorem G12LowRectangle.original_low_count (N : ℕ) (ε : ℝ) : (400 * ∑ p ∈ mother N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0) = ∑ 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

The exact low part of the original weighted product-fibre count.

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

Within the same geometric cell, the residual is exactly a failed safe least-factor or product-endpoint screen; none is paid for free.

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

theorem G12LowRectangle.long_support_geometry (M m : ℕ) (hm : m ∈ Finset.Ioc M (2 * M)) : ↑M ≤ ↑m ∧ ↑m ≤ 2 * ↑M

theorem G12LowRectangle.mother_linked_iff (N m r : ℕ) (ε : ℝ) : (m, r) ∈ mother N ε ↔ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N ∧ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m ∧ r.Coprime N ∧ r * m < N ∧ ↑r < ↑N ^ (1 / 10)

The genuine linked prime window, before output primality, with the strict upper product endpoint recorded explicitly rather than silently deleted.

theorem G12LowRectangle.original_low_partition (N : ℕ) (ε : ℝ) (M T : ℕ) (hlow : ↑N ^ (4 / 53) ≤ ↑T) (hhigh : ↑(2 * T) < ↑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 T, 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 T, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0

The original low count is exactly the certified inner rectangle plus the unpaid physical boundary. The coefficient 400 is retained on both terms.