theorem G12SafeGridBudget.author_monotone : Monotone MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight

The original continuous clipped author weight is monotone, including its join.

noncomputable def G12SafeGridBudget.authorMass (N : ℕ) (A : Finset (ℕ × ℕ)) (δ : ℝ) : ℝ

Equations

• G12SafeGridBudget.authorMass N A δ = ∑ p ∈ A, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight (Real.log ↑p.2 / Real.log ↑N) + δ)

noncomputable def G12SafeGridBudget.originalOutput (N : ℕ) (A : Finset (ℕ × ℕ)) : ℝ

Equations

• G12SafeGridBudget.originalOutput N A = 400 * ∑ p ∈ A, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0

theorem G12SafeGridBudget.authorMass_empty (N : ℕ) (δ : ℝ) : authorMass N ∅ δ = 0

theorem G12SafeGridBudget.originalOutput_empty (N : ℕ) : originalOutput N ∅ = 0

theorem G12SafeGridBudget.endpoint_author_comparison {N T : ℕ} (hN : 4 ≤ N) (hT : 1 ≤ T) (hThi : ↑T ≤ ↑N ^ (1 / 10)) (A : Finset (ℕ × ℕ)) (δ : ℝ) (hA : ∀ p ∈ A, T ≤ p.2) : (36 / (5 * (1 - Real.log ↑T / Real.log ↑N)) + δ) * G12FlexibleWF.mass N A ≤ authorMass N A δ

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

Real safe cells, with empty cells handled separately and all occupied endpoint conditions supplied by GridAdmission. No caller-provided per-cell size hypothesis.

theorem G12SafeGridBudget.authorMass_slack (N : ℕ) (A : Finset (ℕ × ℕ)) (δ : ℝ) : authorMass N A δ = authorMass N A 0 + δ * G12FlexibleWF.mass N A

Exact slack ledger: the delta contribution is delta times the original mass.