noncomputable def G12FineGrid.boundarySourceLo (ρ : ℝ) (N : ℕ) (ε : ℝ) (k : ℕ × ℕ) : ℕ → ℝ

Equations

• G12FineGrid.boundarySourceLo ρ N ε k = G12ClippedWindow.clampLower N ε (fun (x : ℕ) => ↑(G12FineGrid.shortLower ρ N k)) fun (x : ℕ) => ↑(G12FineGrid.shortUpper ρ N k)

noncomputable def G12FineGrid.boundarySourceHi (ρ : ℝ) (N : ℕ) (ε : ℝ) (k : ℕ × ℕ) : ℕ → ℝ

Equations

• G12FineGrid.boundarySourceHi ρ N ε k = G12ClippedWindow.clampUpper N ε fun (x : ℕ) => ↑(G12FineGrid.shortUpper ρ N k)

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

Equations

• G12FineGrid.boundarySourceWindow ρ N ε k m = G12ClippedWindow.window N (G12FineGrid.boundarySourceLo ρ N ε k) (G12FineGrid.boundarySourceHi ρ N ε k) m

theorem G12FineGrid.boundaryWindow_eq_source_filter (ρ : ℝ) (N : ℕ) (ε : ℝ) (k : ℕ × ℕ) (m : ℕ) : boundaryWindow ρ N ε k m = {r ∈ boundarySourceWindow ρ N ε k m | r.Coprime N}

The physical coprimality gate is retained; the analytic source is ungated.

theorem G12FineGrid.boundaryCoefficient_eq_longMask (ρ : ℝ) (N : ℕ) (ε : ℝ) (k : ℕ × ℕ) : boundaryCoefficient ρ N ε k = G12ClippedWindow.longMask N (fun (m : ℕ) => m ∈ Finset.Ioc (longLower ρ k) (longUpper ρ N k)) (G12FlexibleRectangle.longOK N ε (shortLower ρ N k) (shortUpper ρ N k))

theorem G12FineGrid.boundarySource_admissible (ρ : ℝ) {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (k : ℕ × ℕ) : G12ClippedWindow.Admissible N ε (boundaryCoefficient ρ N ε k) (boundarySourceLo ρ N ε k) (boundarySourceHi ρ N ε k)

The actual boundary long mask, with the normalized empty-window endpoints.

theorem G12FineGrid.boundarySource_common_log_saving (A : ℝ) (hA : 0 < A) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ρ ε : ℝ) (k : ℕ × ℕ) (Q : ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ B → ∑ d ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedModuli N Q, |G12ClippedWindow.commonResidual N (boundaryCoefficient ρ N ε k) (boundarySourceLo ρ N ε k) (boundarySourceHi ρ N ε k) d| ≤ C * ↑N / Real.log ↑N ^ A

This is the real source residual of the boundary mask, not a claim that its short coprimality filter inherits SW. Its common mass is still ungated.

theorem G12FineGrid.boundary_sum_le_source (ρ : ℝ) {N : ℕ} (hN : 1 ≤ N) (ε : ℝ) (k : ℕ × ℕ) (f : ℕ → ℕ → ℝ) (hf : ∀ (m r : ℕ), 0 ≤ f m r) : ∑ p ∈ boundaryCell ρ N ε k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p.1 p.2 ≤ ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, ∑ r ∈ boundarySourceWindow ρ N ε k m, boundaryCoefficient ρ N ε k m * f m r

theorem G12FineGrid.boundary_output_le_source (ρ : ℝ) {N : ℕ} (hN : 1 ≤ N) (ε : ℝ) (k : ℕ × ℕ) : (400 * ∑ p ∈ boundaryCell ρ N ε k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0) ≤ 400 * ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, ∑ r ∈ boundarySourceWindow ρ N ε k m, boundaryCoefficient ρ N ε k m * if Nat.Prime (N - r * m) then 1 else 0

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

The first-prime coprimality transport is an explicit nonnegative residual mass.

Equations

• G12FineGrid.boundarySourceBadMass ρ N ε k = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, ∑ _r ∈ G12FineGrid.boundarySourceWindow ρ N ε k m with ¬_r.Coprime N, G12FineGrid.boundaryCoefficient ρ N ε k m

theorem G12FineGrid.boundary_source_mass_split (ρ : ℝ) {N : ℕ} (hN : 1 ≤ N) (ε : ℝ) (k : ℕ × ℕ) : G12ClippedWindow.mass N (boundaryCoefficient ρ N ε k) (boundarySourceLo ρ N ε k) (boundarySourceHi ρ N ε k) = ∑ p ∈ boundaryCell ρ N ε k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 + boundarySourceBadMass ρ N ε k

theorem G12FineGrid.boundarySourceBadMass_le (ρ : ℝ) {N : ℕ} (hN : 4 ≤ N) (ε : ℝ) (k : ℕ × ℕ) : boundarySourceBadMass ρ N ε k ≤ 21 * ↑N / ↑N ^ (4 / 53)

The discarded first-prime mass is dominated by the already paid original bad-prime transport, uniformly over all clipped cells and long masks.

theorem G12FineGrid.boundary_source_mass_le (ρ : ℝ) {N : ℕ} (hN : 4 ≤ N) (ε : ℝ) (k : ℕ × ℕ) : G12ClippedWindow.mass N (boundaryCoefficient ρ N ε k) (boundarySourceLo ρ N ε k) (boundarySourceHi ρ N ε k) ≤ ∑ p ∈ boundaryCell ρ N ε k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 + 21 * ↑N / ↑N ^ (4 / 53)

theorem G12FineGrid.boundarySourceBadMass_log_saving (B : ℝ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ρ ε : ℝ) (k : ℕ × ℕ), 400 * boundarySourceBadMass ρ N ε k ≤ ↑N / Real.log ↑N ^ B

This is payment of the physical/source coprimality transport, not payment of the roughness boundary or of the ordinary output sieve.