theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_curve_eventually (ρ h : ℝ) (hρ : 1 < ρ) (hh : 0 < h) : ∀ᶠ (N : ℕ) in Filter.atTop, 1 + 3 * Real.log ρ / Real.log ↑N ≤ 1 + h

A fixed boundary strip absorbs the moving curve for every sufficiently large N.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_kernel_le_upperSum_eventually (n : ℕ) (hn : 0 < n) (ρ h δ η : ℝ) (hρ : 1 < ρ) (hh : 0 < h) (hhsmall : h ≤ 1 / 20) (hδ : δ ≤ 1 / 4) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → fouvryG9RelaxedPairKernel N ρ δ ≤ fouvryG9RelaxedIntegralUpperSum n h δ + η

Eventual bound by a genuinely fixed finite upper sum. n, h and δ are all chosen before the threshold, and the only analytic input is the proved prime reciprocal rectangle limit.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_corner_delta {n : ℕ} (hn : 0 < n) {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ : δ ≤ 1 / 8) (q : Fin n × Fin n) : fouvryG9RelaxedIntegralCorner n δ q ≤ (1 + 6 * δ) * fouvryG9RelaxedIntegralCorner n 0 q

Uniform small-δ control on every corner, independently of grid size.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedIntegral_upperSum_delta {n : ℕ} (hn : 0 < n) (h : ℝ) {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ : δ ≤ 1 / 8) : fouvryG9RelaxedIntegralUpperSum n h δ ≤ (1 + 6 * δ) * fouvryG9RelaxedIntegralUpperSum n h 0

Uniform corner perturbations propagate through the actual logarithmic masses.