noncomputable def G12RoughBoundary.roughConstant : ℝ

Chosen before all mesh, truncation and error parameters.

Equations

• G12RoughBoundary.roughConstant = 53 / 2 * G12RoughBoundary.harmonicBound ^ 3

theorem G12RoughBoundary.roughConstant_pos : 0 < roughConstant

theorem G12RoughBoundary.nearMass_uniform : ∃ (K : ℕ), 4 ≤ K ∧ ∀ (N : ℕ), K ≤ N → ∀ (a : ℝ), 1 ≤ a → Real.log ↑N / ↑N * nearMass N a ≤ roughConstant * (a - 1 + 1 / ↑N ^ (4 / 53))

One common threshold works for every a≥1; the lattice endpoint is explicit.

theorem G12RoughBoundary.nearMass_budget (δ : ℝ) (hδ : 0 < δ) : ∃ (K : ℕ), 4 ≤ K ∧ ∀ (N : ℕ), K ≤ N → ∀ (a : ℝ), 1 ≤ a → Real.log ↑N / ↑N * nearMass N a ≤ roughConstant * (a - 1) + δ

Error cutoff is independent of a, rho and epsilon.

theorem G12RoughBoundary.roughBoundary_budget (δ : ℝ) (hδ : 0 < δ) : ∃ (K : ℕ), 4 ≤ K ∧ ∀ (N : ℕ), K ≤ N → ∀ (ρ a ε : ℝ), 1 ≤ a → (∀ k ∈ G12FineGrid.indices ρ N, ↑(G12FineGrid.shortUpper ρ N k) ≤ a * ↑(G12FineGrid.shortLower ρ N k)) → Real.log ↑N / ↑N * (400 * ∑ p ∈ G12FineGrid.roughBoundary ρ N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1) ≤ roughConstant * (a - 1) + δ

Literal rough-boundary payment, uniform in epsilon and any grid satisfying the ratio.

theorem G12RoughBoundary.fixed_grid_roughBoundary_budget {ρ a : ℝ} (hρ : 1 < ρ) (hρa : ρ < a) (δ : ℝ) (hδ : 0 < δ) : ∃ (K : ℕ), 4 ≤ K ∧ ∀ (N : ℕ), K ≤ N → ∀ (ε : ℝ), Real.log ↑N / ↑N * (400 * ∑ p ∈ G12FineGrid.roughBoundary ρ N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1) ≤ roughConstant * (a - 1) + δ

Actual rounded grid; cutoff precedes epsilon, which is unrestricted here.

theorem G12RoughBoundary.exists_fixed_roughBoundary_constant : ∃ C > 0, ∀ (ρ a : ℝ), 1 < ρ → ρ < a → ∀ (δ : ℝ), 0 < δ → ∃ (K : ℕ), 4 ≤ K ∧ ∀ (N : ℕ), K ≤ N → ∀ (ε : ℝ), Real.log ↑N / ↑N * (400 * ∑ p ∈ G12FineGrid.roughBoundary ρ N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1) ≤ C * (a - 1) + δ

The roughness constant itself is fixed before all grid parameters.

theorem G12RoughBoundary.fullBoundary_sum_cells {ρ : ℝ} (hρ : 1 < ρ) (N : ℕ) (ε : ℝ) (f : ℕ × ℕ → ℝ) : ∑ p ∈ (G12FineGrid.indices ρ N).biUnion (G12FineGrid.boundaryCell ρ N ε), f p = ∑ k ∈ G12FineGrid.indices ρ N, ∑ p ∈ G12FineGrid.boundaryCell ρ N ε k, f p

No physical pair is charged once per overlapping cell: the cells are disjoint.

theorem G12RoughBoundary.fullBoundary_mass_le (ρ : ℝ) (N : ℕ) (ε : ℝ) : ∑ p ∈ (G12FineGrid.indices ρ N).biUnion (G12FineGrid.boundaryCell ρ N ε), MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 ≤ ∑ p ∈ G12FineGrid.productBoundary ρ N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 + ∑ p ∈ G12FineGrid.roughBoundary ρ N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1

Nonnegative union domination: no signed inclusion-exclusion is erased.

noncomputable def G12RoughBoundary.fullConstant : ℝ

Fixed universal constant includes the already paid product-boundary coefficient.

Equations

• G12RoughBoundary.fullConstant = G12RoughBoundary.roughConstant + |564383 / 1000000 * 3 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral fun (x : ℝ) => 1|

theorem G12RoughBoundary.fullConstant_pos : 0 < fullConstant

theorem G12RoughBoundary.fixed_grid_fullBoundary_budget {ρ a ε : ℝ} (hρ : 1 < ρ) (hρa : ρ < a) (ha2 : a ≤ 2) (he : 0 < ε) (he2 : ε ≤ 2 / 15) (δ : ℝ) (hδ : 0 < δ) : ∃ (K : ℕ), 4 ≤ K ∧ ∀ (N : ℕ), K ≤ N → Real.log ↑N / ↑N * (400 * ∑ p ∈ (G12FineGrid.indices ρ N).biUnion (G12FineGrid.boundaryCell ρ N ε), MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1) ≤ fullConstant * (a - 1) + δ

Full original raw boundary, not the output-prime weighted/signed remainder.

theorem G12RoughBoundary.exists_fixed_fullBoundary_constant : ∃ C > 0, ∀ (ρ a ε : ℝ), 1 < ρ → ρ < a → a ≤ 2 → 0 < ε → ε ≤ 2 / 15 → ∀ (δ : ℝ), 0 < δ → ∃ (K : ℕ), 4 ≤ K ∧ ∀ (N : ℕ), K ≤ N → Real.log ↑N / ↑N * (400 * ∑ p ∈ (G12FineGrid.indices ρ N).biUnion (G12FineGrid.boundaryCell ρ N ε), MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1) ≤ C * (a - 1) + δ

Headline quantifier order: the positive C is chosen before rho,a,epsilon,delta.