noncomputable def G12FineGrid.lowCut (N : ℕ) : ℕ

The lower cutoff is not deleted: its integer slice is retained separately.

Equations

• G12FineGrid.lowCut N = ⌈↑N ^ (4 / 53)⌉₊

noncomputable def G12FineGrid.highCut (N : ℕ) : ℕ

Equations

• G12FineGrid.highCut N = ⌈↑N ^ (1 / 10)⌉₊ - 1

noncomputable def G12FineGrid.indices (ρ : ℝ) (N : ℕ) : Finset (ℕ × ℕ)

Equations

• G12FineGrid.indices ρ N = Finset.range (G12FineGrid.count ρ N) ×ˢ Finset.range (G12FineGrid.count ρ N)

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

These are coordinate boxes, not safe rectangles.

Equations

• G12FineGrid.box ρ N k = G12FineGrid.clipped ρ 0 (N - 1) k.1 ×ˢ G12FineGrid.clipped ρ (G12FineGrid.lowCut N) (G12FineGrid.highCut N) k.2

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

Equations

• G12FineGrid.motherCell ρ N ε k = {x ∈ G12FlexibleRectangle.mother N ε | x ∈ G12FineGrid.box ρ N k}

noncomputable def G12FineGrid.cutoffSlice (N : ℕ) (ε : ℝ) : Finset (ℕ × ℕ)

Equations

• G12FineGrid.cutoffSlice N ε = {p ∈ G12FlexibleRectangle.mother N ε | p.2 = G12FineGrid.lowCut N}

theorem G12FineGrid.box_unique {ρ : ℝ} (hρ : 1 < ρ) {N : ℕ} {k l p : ℕ × ℕ} (hk : p ∈ box ρ N k) (hl : p ∈ box ρ N l) : k = l

theorem G12FineGrid.box_disjoint {ρ : ℝ} (hρ : 1 < ρ) (N : ℕ) {k l : ℕ × ℕ} (hkl : k ≠ l) : Disjoint (box ρ N k) (box ρ N l)

theorem G12FineGrid.cell_disjoint {ρ : ℝ} (hρ : 1 < ρ) (N : ℕ) (ε : ℝ) {k l : ℕ × ℕ} (hkl : k ≠ l) : Disjoint (motherCell ρ N ε k) (motherCell ρ N ε l)

theorem G12FineGrid.mother_coordinates {N m r : ℕ} {ε : ℝ} (h : (m, r) ∈ G12FlexibleRectangle.mother N ε) : 1 ≤ m ∧ m < N ∧ 1 ≤ r ∧ r < N ∧ lowCut N ≤ r ∧ r ≤ highCut N

Actual mother coordinates: strict m<N and r<N, and the exact rounded cutoffs.

theorem G12FineGrid.mother_cover {ρ : ℝ} (hρ : 1 < ρ) {N : ℕ} {ε : ℝ} {p : ℕ × ℕ} (hp : p ∈ G12FlexibleRectangle.mother N ε) (hs : p.2 ≠ lowCut N) : ∃! k : ℕ × ℕ, k ∈ indices ρ N ∧ p ∈ motherCell ρ N ε k

Every nonslice mother atom is in exactly one finite coordinate box.

theorem G12FineGrid.slice_disjoint (ρ : ℝ) (N : ℕ) (ε : ℝ) (k : ℕ × ℕ) : Disjoint (cutoffSlice N ε) (motherCell ρ N ε k)

theorem G12FineGrid.mother_partition {ρ : ℝ} (hρ : 1 < ρ) (N : ℕ) (ε : ℝ) : cutoffSlice N ε ∪ (indices ρ N).biUnion (motherCell ρ N ε) = G12FlexibleRectangle.mother N ε

Exact finite decomposition, with the cutoff slice explicitly present.

theorem G12FineGrid.weighted_partition {ρ : ℝ} (hρ : 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 ∈ motherCell ρ N ε k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p

The same physical coefficient and body multiplicity 400 survive the mesh.

theorem G12FineGrid.original_low_partition {ρ : ℝ} (hρ : 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 ∈ motherCell ρ N ε k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0

Literal original low fibre count, not a replacement coefficient.