theorem G12SafeGridBudget.grid_fee (ρ : ℝ) (hρ : 1 < ρ) (B : ℕ) : ∀ᶠ (N : ℕ) in Filter.atTop, ↑(G12FineGrid.indices ρ N).card * (↑N / Real.log ↑N ^ (B + 3)) ≤ ↑N / Real.log ↑N ^ B

The actual log-squared number of grid cells costs three fixed log powers, including its rho-dependent constant. Rho is fixed before the threshold.

theorem G12SafeGridBudget.fixed_grid_paid (δ : ℝ) (hδ : 0 < δ) (e : ℝ) (he : 0 < e) (he1 : e ≤ 1) (ρ : ℝ) (hρ : 1 < ρ) (hρu : ρ ≤ 3 / 2) (B : ℕ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∑ k ∈ G12FineGrid.indices ρ N, originalOutput N (G12FineGrid.safe ρ N e k) ≤ (400 * ∑ k ∈ G12FineGrid.indices ρ N, authorMass N (G12FineGrid.safe ρ N e k) δ) * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N / Real.log ↑N + ↑N / Real.log ↑N ^ B

Fixed-grid output with arbitrary logarithmic saving, the true author weight inside the original normalized coefficient sum, and no unpaid additive remainder.

theorem G12SafeGridBudget.fixed_grid_normalized (δ τ : ℝ) (hδ : 0 < δ) (hτ : 0 < τ) (e : ℝ) (he : 0 < e) (he1 : e ≤ 1) (ρ : ℝ) (hρ : 1 < ρ) (hρu : ρ ≤ 3 / 2) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∑ k ∈ G12FineGrid.indices ρ N, originalOutput N (G12FineGrid.safe ρ N e k) ≤ (400 * ∑ k ∈ G12FineGrid.indices ρ N, authorMass N (G12FineGrid.safe ρ N e k) δ) * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N / Real.log ↑N + τ * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Final safe-grid bound at singular-series scale. The main slack and additive slack can be chosen independently; neither depends on N or the cell index.