def G12FineGrid.boundaryMask (ρ : ℝ) (N : ℕ) (ε : ℝ) (k : ℕ × ℕ) (m : ℕ) : Prop

The actual boundary mask depends only on the long coordinate.

Equations

• G12FineGrid.boundaryMask ρ N ε k m = (m ∈ Finset.Ioc (G12FineGrid.longLower ρ k) (G12FineGrid.longUpper ρ N k) ∧ ¬G12FlexibleRectangle.longOK N ε (G12FineGrid.shortLower ρ N k) (G12FineGrid.shortUpper ρ N k) m)

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

The original normalized coefficient, with only a long-variable mask.

Equations

• G12FineGrid.boundaryCoefficient ρ N ε k m = if G12FineGrid.boundaryMask ρ N ε k m then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m else 0

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

Original PiLi endpoints clipped at the actual short-cell endpoints. Coprimality is retained on the short side, never asserted to inherit SW.

Equations

• G12FineGrid.boundaryWindow ρ N ε k m = {r ∈ Finset.range (N + 1) | Nat.Prime r ∧ r.Coprime N ∧ max (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m) ↑(G12FineGrid.shortLower ρ N k) < ↑r ∧ ↑r ≤ min (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m) ↑(G12FineGrid.shortUpper ρ N k)}

theorem G12FineGrid.boundaryMask_iff (ρ : ℝ) (N : ℕ) (ε : ℝ) (k : ℕ × ℕ) (m r : ℕ) (hp : (m, r) ∈ motherCell ρ N ε k) : (m, r) ∈ boundaryCell ρ N ε k ↔ boundaryMask ρ N ε k m

theorem G12FineGrid.boundaryCoefficient_bounds (ρ : ℝ) (N : ℕ) (ε : ℝ) (k : ℕ × ℕ) (m : ℕ) : 0 ≤ boundaryCoefficient ρ N ε k m ∧ boundaryCoefficient ρ N ε k m ≤ 1

theorem G12FineGrid.motherCell_window_iff (ρ : ℝ) {N : ℕ} (hN : 1 ≤ N) (ε : ℝ) (k : ℕ × ℕ) {m r : ℕ} (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) : (m, r) ∈ motherCell ρ N ε k ↔ m ∈ Finset.Ioc (longLower ρ k) (longUpper ρ N k) ∧ r ∈ boundaryWindow ρ N ε k m

Coprimality removes the apparent closed product endpoint in PiLiHi.

theorem G12FineGrid.boundaryCell_eq_masked_window (ρ : ℝ) {N : ℕ} (hN : 1 ≤ N) (ε : ℝ) (k : ℕ × ℕ) : boundaryCell ρ N ε k = {p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N ×ˢ Finset.range (N + 1) | boundaryMask ρ N ε k p.1 ∧ p.2 ∈ boundaryWindow ρ N ε k p.1}

Literal finite-set representation, with the original active support.

theorem G12FineGrid.boundaryCell_weighted_window (ρ : ℝ) {N : ℕ} (hN : 1 ≤ N) (ε : ℝ) (k : ℕ × ℕ) (f : ℕ → ℕ → ℝ) : ∑ 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 ∈ boundaryWindow ρ N ε k m, boundaryCoefficient ρ N ε k m * f m r

Exact weighted identity for any test: AP, coprimality, or output-prime. No cancellation is lost and the physical coefficient is unchanged.