noncomputable def G12SafeGridBudget.safeUnion (ρ : ℝ) (N : ℕ) (e : ℝ) : Finset (ℕ × ℕ)

The literal union of all actual safe cells in the original finite grid.

Equations

• G12SafeGridBudget.safeUnion ρ N e = (G12FineGrid.indices ρ N).biUnion (G12FineGrid.safe ρ N e)

theorem G12SafeGridBudget.safe_pairwise {ρ : ℝ} (hρ : 1 < ρ) {N : ℕ} (hN : 1 ≤ N) (e : ℝ) : (↑(G12FineGrid.indices ρ N)).PairwiseDisjoint (G12FineGrid.safe ρ N e)

theorem G12SafeGridBudget.safe_union_sum {ρ : ℝ} (hρ : 1 < ρ) {N : ℕ} (hN : 1 ≤ N) (e : ℝ) (f : ℕ × ℕ → ℝ) : ∑ p ∈ safeUnion ρ N e, f p = ∑ k ∈ G12FineGrid.indices ρ N, ∑ p ∈ G12FineGrid.safe ρ N e k, f p

theorem G12SafeGridBudget.safe_union_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 → (400 * ∑ p ∈ safeUnion ρ N e, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0) ≤ (400 * ∑ p ∈ safeUnion ρ N e, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight (Real.log ↑p.2 / Real.log ↑N) + δ)) * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N / Real.log ↑N + τ * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Literal safe-set terminal: no duplicated grid atoms, no artificial weights, no unbound additive fees, and independent fixed main/additive slacks.