noncomputable def G12FineGrid.longLower (ρ : ℝ) (k : ℕ × ℕ) : ℕ

Equations

• G12FineGrid.longLower ρ k = max 0 (G12FineGrid.endpoint ρ k.1)

noncomputable def G12FineGrid.longUpper (ρ : ℝ) (N : ℕ) (k : ℕ × ℕ) : ℕ

Equations

• G12FineGrid.longUpper ρ N k = min (N - 1) (G12FineGrid.endpoint ρ (k.1 + 1))

noncomputable def G12FineGrid.shortLower (ρ : ℝ) (N : ℕ) (k : ℕ × ℕ) : ℕ

Equations

• G12FineGrid.shortLower ρ N k = max (G12FineGrid.lowCut N) (G12FineGrid.endpoint ρ k.2)

noncomputable def G12FineGrid.shortUpper (ρ : ℝ) (N : ℕ) (k : ℕ × ℕ) : ℕ

Equations

• G12FineGrid.shortUpper ρ N k = min (G12FineGrid.highCut N) (G12FineGrid.endpoint ρ (k.2 + 1))

noncomputable def G12FineGrid.safe (ρ : ℝ) (N : ℕ) (ε : ℝ) (k : ℕ × ℕ) : Finset (ℕ × ℕ)

The exact production rectangle, at the actual clipped endpoints.

Equations

• G12FineGrid.safe ρ N ε k = G12FlexibleRectangle.rectangle N ε (G12FineGrid.longLower ρ k) (G12FineGrid.longUpper ρ N k) (G12FineGrid.shortLower ρ N k) (G12FineGrid.shortUpper ρ N k)

noncomputable def G12FineGrid.boundaryCell (ρ : ℝ) (N : ℕ) (ε : ℝ) (k : ℕ × ℕ) : Finset (ℕ × ℕ)

This set has no analytic smallness assertion.

Equations

• G12FineGrid.boundaryCell ρ N ε k = G12FineGrid.motherCell ρ N ε k \ G12FineGrid.safe ρ N ε k

theorem G12FineGrid.short_lower_valid (ρ : ℝ) (N : ℕ) (k : ℕ × ℕ) : ↑N ^ (4 / 53) ≤ ↑(shortLower ρ N k)

theorem G12FineGrid.highCut_strict {N : ℕ} (hN : 1 ≤ N) : ↑(highCut N) < ↑N ^ (1 / 10)

theorem G12FineGrid.short_upper_valid (ρ : ℝ) {N : ℕ} (hN : 1 ≤ N) (k : ℕ × ℕ) : ↑(shortUpper ρ N k) < ↑N ^ (1 / 10)

theorem G12FineGrid.safe_subset (ρ : ℝ) {N : ℕ} (hN : 1 ≤ N) (ε : ℝ) (k : ℕ × ℕ) : safe ρ N ε k ⊆ motherCell ρ N ε k

theorem G12FineGrid.boundaryCell_iff (ρ : ℝ) (N : ℕ) (ε : ℝ) (k : ℕ × ℕ) (m r : ℕ) (hp : (m, r) ∈ motherCell ρ N ε k) : (m, r) ∈ boundaryCell ρ N ε k ↔ m.minFac < shortUpper ρ N k ∨ ↑(shortLower ρ N k) * ↑m < ε * ↑N ∨ N ≤ shortUpper ρ N k * m

All three failed tests are still in the boundary, without paying for them.

theorem G12FineGrid.local_partition (ρ : ℝ) {N : ℕ} (hN : 1 ≤ N) (ε : ℝ) (k : ℕ × ℕ) : Disjoint (safe ρ N ε k) (boundaryCell ρ N ε k) ∧ safe ρ N ε k ∪ boundaryCell ρ N ε k = motherCell ρ N ε k

theorem G12FineGrid.local_weighted_partition (ρ : ℝ) {N : ℕ} (hN : 1 ≤ N) (ε : ℝ) (k : ℕ × ℕ) (f : ℕ × ℕ → ℝ) : ∑ p ∈ motherCell ρ N ε k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p = ∑ p ∈ safe ρ N ε k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p + ∑ p ∈ boundaryCell ρ N ε k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p

theorem G12FineGrid.refined_weighted_partition {ρ : ℝ} (hρ : 1 < ρ) {N : ℕ} (hN : 1 ≤ N) (ε : ℝ) (f : ℕ × ℕ → ℝ) : 400 * ∑ p ∈ G12FlexibleRectangle.mother N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p = 400 * ∑ p ∈ cutoffSlice N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p + 400 * ∑ k ∈ indices ρ N, (∑ p ∈ safe ρ N ε k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p + ∑ p ∈ boundaryCell ρ N ε k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p)

An exact three-way ledger: cutoff slice, safe rectangles, and unpaid boundary.

theorem G12FineGrid.mother_long_scale {N m r : ℕ} {ε : ℝ} (hp : (m, r) ∈ G12FlexibleRectangle.mother N ε) : ↑N ^ (4 / 53) ≤ ↑m

Only the large-N source-scale gate remains; active long coordinates are real.

theorem G12FineGrid.high_endpoint_excluded {N m r : ℕ} {ε : ℝ} (hr : ↑r = ↑N ^ (1 / 10)) : (m, r) ∉ G12FlexibleRectangle.mother N ε

Equality at the high real cutoff is excluded even if the cutoff is prime.

theorem G12FineGrid.cutoffSlice_iff (N m r : ℕ) (ε : ℝ) : (m, r) ∈ cutoffSlice N ε ↔ (m, r) ∈ G12FlexibleRectangle.mother N ε ∧ r = lowCut N

The retained slice has precisely its literal mother predicate.

theorem G12FineGrid.short_dyadic {ρ : ℝ} (hρ : 1 < ρ) (hu : ρ ≤ 3 / 2) (N : ℕ) (k : ℕ × ℕ) (hT : 3 ≤ shortLower ρ N k) : shortUpper ρ N k ≤ 2 * shortLower ρ N k

theorem G12FineGrid.long_dyadic {ρ : ℝ} (hρ : 1 < ρ) (hu : ρ ≤ 3 / 2) (N : ℕ) (k : ℕ × ℕ) (hM : 3 ≤ longLower ρ k) : longUpper ρ N k ≤ 2 * longLower ρ k

theorem G12FineGrid.occupied_endpoint_order {ρ : ℝ} {N : ℕ} {k p : ℕ × ℕ} (hp : p ∈ box ρ N k) : longLower ρ k < longUpper ρ N k ∧ shortLower ρ N k < shortUpper ρ N k

theorem G12FineGrid.original_high_endpoint {N m r : ℕ} {ε : ℝ} (hf : r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m) (hr : ↑r = ↑N ^ (1 / 10)) : r ∈ {r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m | ↑N ^ (1 / 10) ≤ ↑r}

A high endpoint in the original fibre stays in the high half, with no assumption that the endpoint is composite.

theorem G12FineGrid.original_low_safe_partition {ρ : ℝ} (hρ : 1 < ρ) {N : ℕ} (hN : 1 ≤ N) (ε : ℝ) : ∑ 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 ∈ cutoffSlice N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0) + 400 * ∑ k ∈ indices ρ N, ((∑ p ∈ safe ρ N ε k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0) + ∑ p ∈ boundaryCell ρ N ε k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0)

Full original count, retaining both the slice and all three safety failures.