theorem G12FineGrid.boundary_sum_le_branches {ρ : ℝ} (hρ : 1 < ρ) (N : ℕ) (ε : ℝ) (f : ℕ × ℕ → ℝ) (hf : ∀ (p : ℕ × ℕ), 0 ≤ f p) : ∑ k ∈ indices ρ N, ∑ p ∈ boundaryCell ρ N ε k, f p ≤ ∑ p ∈ productBoundary ρ N ε, f p + ∑ p ∈ roughBoundary ρ N ε, f p

The two boundary branches may overlap. This is an upper bound for a nonnegative physical test, never a subtraction of signed distribution terms.

theorem G12FineGrid.original_total_paid_grid (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ρ ε : ℝ), 1 < ρ → ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductPrimeTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) ≤ (G12LowHighOutput.outputCount N (G12LowHighOutput.high N ε) + 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) + G12LowHighOutput.outputCount N (productBoundary ρ N ε) + G12LowHighOutput.outputCount N (roughBoundary ρ N ε) + δ * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The retained prime cutoff slice is actually paid in the complete original count. Safe, product-boundary and roughness outputs all remain explicit.