theorem G12FineGrid.original_total_high_normalized (δ : ℝ) (hδ : 0 < δ) : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → ∀ (ρ : ℝ), 1 < ρ → ∀ (ε : ℝ), ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductPrimeTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) ≤ ((8 + δ / 2) * 400 * G12ClippedWindow.highMass N ε * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N / Real.log ↑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 ((indices ρ N).biUnion (boundaryCell ρ N ε)) + δ * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Original total count with the actual high source normalized and the cutoff slice paid. The entire boundary remains a literal output count, not a raw mass.