theorem G12FineGrid.lower_product_band {a ε N T V r m : ℝ} (ha : 1 < a) (he : 0 < ε) (hN : 0 < N) (hm : 0 ≤ m) (hr : r ≤ V) (hV : V ≤ a * T) (hlo : ε * N ≤ r * m) (hfail : T * m < ε * N) : ε / a * N < r * m ∧ r * m ≤ a * ε * N

The widened open lower endpoint retains even a closed epsilon endpoint.

theorem G12FineGrid.upper_product_band {a N T V r m : ℝ} (ha : 0 < a) (hm : 0 < m) (hr : T < r) (hV : V ≤ a * T) (hfail : N ≤ V * m) (hhi : r * m < N) : 1 / a * N < r * m ∧ r * m ≤ N

The upper-product failure lands above N/a, with its original strict top.

noncomputable def G12FineGrid.bandWindow (N : ℕ) (ε l u : ℝ) (m : ℕ) : Finset ℕ

Raw original linked-window mass restricted by a product band.

Equations

• G12FineGrid.bandWindow N ε l u m = {r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m | ¬r ∣ N ∧ l * ↑N < ↑r * ↑m ∧ ↑r * ↑m ≤ u * ↑N}

noncomputable def G12FineGrid.bandMass (N : ℕ) (ε l u : ℝ) : ℝ

Equations

• G12FineGrid.bandMass N ε l u = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ↑(G12FineGrid.bandWindow N ε l u m).card

theorem G12FineGrid.product_bands_integral_budget {a ε : ℝ} (ha : 1 < a) (ha2 : a ≤ 2) (he : 0 < ε) (he2 : ε ≤ 2 / 15) (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Real.log ↑N / ↑N * ((MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ThinSum N (fun (x : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label) => ε / a) fun (x : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label) => a * ε) + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ThinSum N (fun (x : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label) => 1 / a) fun (x : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label) => 1) ≤ (564383 / 1000000 * (3 * (a - 1)) * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral fun (x : ℝ) => 1) + δ

Both bands use the actual uniform thin-count producer. The quantifier on all label-dependent endpoints remains after the common large-N threshold.

theorem G12FineGrid.bandMass_le_thinSum {N : ℕ} (ε l u : ℝ) (hlu : l ≤ u) : 400 * bandMass N ε l u ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ThinSum N (fun (x : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label) => l) fun (x : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label) => u

Injection of actual body/prime pairs into the two real-endpoint rough counts. The factor 400 restores all original body multiplicities.

theorem G12FineGrid.pairMass_le_bandMass (N : ℕ) (ε l u : ℝ) (S : Finset (ℕ × ℕ)) (hS : ∀ p ∈ S, p.1 ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N ∧ p.2 ∈ bandWindow N ε l u p.1) : ∑ p ∈ S, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 ≤ bandMass N ε l u

Weighted domination for any literal set of physical pairs.

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

Only the two product failures; the roughness failure is not paid here.

Equations

• G12FineGrid.productBoundary ρ N ε = (G12FineGrid.indices ρ N).biUnion fun (k : ℕ × ℕ) => {p ∈ G12FineGrid.motherCell ρ N ε k | ↑(G12FineGrid.shortLower ρ N k) * ↑p.1 < ε * ↑N ∨ N ≤ G12FineGrid.shortUpper ρ N k * p.1}

theorem G12FineGrid.productBoundary_in_bands {ρ a ε : ℝ} {N : ℕ} (hN : 1 ≤ N) (ha : 1 < a) (he : 0 < ε) (hmesh : ∀ k ∈ indices ρ N, ↑(shortUpper ρ N k) ≤ a * ↑(shortLower ρ N k)) {p : ℕ × ℕ} (hp : p ∈ productBoundary ρ N ε) : p.1 ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N ∧ (p.2 ∈ bandWindow N ε (ε / a) (a * ε) p.1 ∨ p.2 ∈ bandWindow N ε (1 / a) 1 p.1)

theorem G12FineGrid.productBoundary_mass_le_bands {ρ a ε : ℝ} {N : ℕ} (hN : 1 ≤ N) (ha : 1 < a) (he : 0 < ε) (hmesh : ∀ k ∈ indices ρ N, ↑(shortUpper ρ N k) ≤ a * ↑(shortLower ρ N k)) : ∑ p ∈ productBoundary ρ N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 ≤ bandMass N ε (ε / a) (a * ε) + bandMass N ε (1 / a) 1

No cell-count loss: union first, then pay the two physical bands once.

theorem G12FineGrid.productBoundary_integral_budget {a ε : ℝ} (ha : 1 < a) (ha2 : a ≤ 2) (he : 0 < ε) (he2 : ε ≤ 2 / 15) (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ρ : ℝ), (∀ k ∈ indices ρ N, ↑(shortUpper ρ N k) ≤ a * ↑(shortLower ρ N k)) → Real.log ↑N / ↑N * (400 * ∑ p ∈ productBoundary ρ N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1) ≤ (564383 / 1000000 * (3 * (a - 1)) * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral fun (x : ℝ) => 1) + δ

Actual fine-grid product-boundary payment at raw-mother normalization. The roughness boundary and the output-prime second logarithm remain separate.

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

The remaining roughness branch, retained as a literal physical set.

Equations

• G12FineGrid.roughBoundary ρ N ε = (G12FineGrid.indices ρ N).biUnion fun (k : ℕ × ℕ) => {p ∈ G12FineGrid.motherCell ρ N ε k | p.1.minFac < G12FineGrid.shortUpper ρ N k}

theorem G12FineGrid.boundary_union_decomposition (ρ : ℝ) (N : ℕ) (ε : ℝ) : (indices ρ N).biUnion (boundaryCell ρ N ε) = productBoundary ρ N ε ∪ roughBoundary ρ N ε

The complete original boundary is exactly the paid product branch union an explicitly unpaid roughness branch; overlap is harmless.

theorem G12FineGrid.productBoundary_sum_cells {ρ : ℝ} (hρ : 1 < ρ) (N : ℕ) (ε : ℝ) (f : ℕ × ℕ → ℝ) : ∑ p ∈ productBoundary ρ N ε, f p = ∑ k ∈ indices ρ N, ∑ p ∈ motherCell ρ N ε k with ↑(shortLower ρ N k) * ↑p.1 < ε * ↑N ∨ N ≤ shortUpper ρ N k * p.1, f p

The union budget is also exactly the sum over the original disjoint cells.

theorem G12FineGrid.short_ratio_of_rounding {ρ a : ℝ} (hρ : 1 < ρ) (hρa : ρ ≤ a) (N : ℕ) (hscale : ρ ≤ (a - ρ) * ↑(lowCut N)) (k : ℕ × ℕ) : ↑(shortUpper ρ N k) ≤ a * ↑(shortLower ρ N k)

Explicit rounding allowance discharges every clipped short-cell ratio.

theorem G12FineGrid.active_minFac_body_witness {N m : ℕ} (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) : ∃ v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12GoodCrossBodies N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)), MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd v = m ∧ m.minFac = v.snd.snd.fst

A source-level body witness identifies minFac; no arbitrary new q is postulated.

theorem G12FineGrid.fixed_grid_productBoundary_integral_budget {ρ a ε : ℝ} (hρ : 1 < ρ) (hρa : ρ < a) (ha2 : a ≤ 2) (he : 0 < ε) (he2 : ε ≤ 2 / 15) (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Real.log ↑N / ↑N * (400 * ∑ p ∈ productBoundary ρ N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1) ≤ (564383 / 1000000 * (3 * (a - 1)) * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral fun (x : ℝ) => 1) + δ

Fully discharged rounded-grid budget for any fixed finer ratio rho<a. No cellwise analytic hypothesis remains; the cutoff precedes N.