noncomputable def G12BandOutput.clipOutput (N : ℕ) (ε : ℝ) (T V : ℕ → ℝ) : ℝ

Equations

• G12BandOutput.clipOutput N ε T V = G12ClippedWindow.primeOutput N (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N) (G12ClippedWindow.clampLower N ε T V) (G12ClippedWindow.clampUpper N ε V)

noncomputable def G12BandOutput.sourceOutput (N : ℕ) (ε a : ℝ) : ℝ

Equations

• G12BandOutput.sourceOutput N ε a = G12BandOutput.clipOutput N ε (G12BandOutput.productLo N (ε / a)) (G12BandOutput.productLo N (a * ε)) + G12BandOutput.clipOutput N ε (G12BandOutput.productLo N (1 / a)) (G12BandOutput.productLo N 1) + G12BandOutput.clipOutput N ε (G12BandOutput.roughLo a) (G12BandOutput.top N)

noncomputable def G12BandOutput.boundaryOutput (ρ : ℝ) (N : ℕ) (ε : ℝ) : ℝ

Literal entire grid boundary, with the prime-output indicator.

Equations

• G12BandOutput.boundaryOutput ρ N ε = 400 * ∑ p ∈ (G12FineGrid.indices ρ N).biUnion (G12FineGrid.boundaryCell ρ N ε), G12BandOutput.atom N p

noncomputable def G12BandOutput.HN (N : ℕ) : ℝ

Equations

• G12BandOutput.HN N = MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

theorem G12BandOutput.HN_nonneg (N : ℕ) : 0 ≤ HN N

theorem G12BandOutput.boundaryOutput_le_source {ρ a ε : ℝ} {N : ℕ} (hN : 1 ≤ N) (ha : 1 < a) (he : 0 < ε) (hmesh : ∀ k ∈ G12FineGrid.indices ρ N, ↑(G12FineGrid.shortUpper ρ N k) ≤ a * ↑(G12FineGrid.shortLower ρ N k)) : boundaryOutput ρ N ε ≤ sourceOutput N ε a

The sieve is invoked on three global windows, never once for every cell.

theorem G12BandOutput.sourceOutput_uniformEight (t : ℝ) (ht : 0 < t) : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → ∀ (ε a : ℝ), sourceOutput N ε a ≤ (8 + t) * 400 * sourceMass N ε a * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N / Real.log ↑N + 3 * t * HN N

There are exactly three additive sieve errors, regardless of the grid size.

noncomputable def G12BandOutput.outputConstant : ℝ

Universal constant, chosen before all mesh and truncation parameters.

Equations

• G12BandOutput.outputConstant = 9 * G12RoughBoundary.fullConstant

theorem G12BandOutput.outputConstant_pos : 0 < outputConstant

theorem G12BandOutput.sourceOutput_budget {a ε : ℝ} (ha : 1 < a) (ha2 : a ≤ 2) (he : 0 < ε) (he2 : ε ≤ 2 / 15) (δ : ℝ) (hδ : 0 < δ) : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → sourceOutput N ε a ≤ outputConstant * (a - 1) * HN N + δ * HN N

The global source has the actual prime-output scale, not raw mother scale.

theorem G12BandOutput.boundaryOutput_budget {a ε : ℝ} (ha : 1 < a) (ha2 : a ≤ 2) (he : 0 < ε) (he2 : ε ≤ 2 / 15) (δ : ℝ) (hδ : 0 < δ) : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → ∀ (ρ : ℝ), (∀ k ∈ G12FineGrid.indices ρ N, ↑(G12FineGrid.shortUpper ρ N k) ≤ a * ↑(G12FineGrid.shortLower ρ N k)) → boundaryOutput ρ N ε ≤ outputConstant * (a - 1) * HN N + δ * HN N

A uniform geometric condition suffices; no analytic bound is assumed on the target.

theorem G12BandOutput.fixed_grid_boundaryOutput_budget {ρ a ε : ℝ} (hρ : 1 < ρ) (hρa : ρ < a) (ha2 : a ≤ 2) (he : 0 < ε) (he2 : ε ≤ 2 / 15) (δ : ℝ) (hδ : 0 < δ) : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → boundaryOutput ρ N ε ≤ outputConstant * (a - 1) * HN N + δ * HN N

Actual rounded fine grid. The cutoff precedes N and its parity proof.

theorem G12BandOutput.exists_fixed_boundaryOutput_constant : ∃ C > 0, ∀ (ρ a ε : ℝ), 1 < ρ → ρ < a → a ≤ 2 → 0 < ε → ε ≤ 2 / 15 → ∀ (δ : ℝ), 0 < δ → ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → boundaryOutput ρ N ε ≤ C * (a - 1) * HN N + δ * HN N

theorem G12BandOutput.exists_small_mesh (τ : ℝ) (hτ : 0 < τ) : ∃ (ρ : ℝ) (a : ℝ), 1 < ρ ∧ ρ < a ∧ a ≤ 2 ∧ ∀ (ε : ℝ), 0 < ε → ε ≤ 2 / 15 → ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → boundaryOutput ρ N ε ≤ τ * HN N

Mesh is selected before N: arbitrarily small actual entire-boundary output.

theorem G12BandOutput.actual_boundary_output_constant : ∃ C > 0, ∀ (ρ a ε : ℝ), 1 < ρ → ρ < a → a ≤ 2 → 0 < ε → ε ≤ 2 / 15 → ∀ (δ : ℝ), 0 < δ → ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → (400 * ∑ p ∈ (G12FineGrid.indices ρ N).biUnion (G12FineGrid.boundaryCell ρ N ε), MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0) ≤ C * (a - 1) * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) + δ * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Expanded actual-output headline: every physical atom and both logarithms are visible.