theorem G12ClippedWindow.choose_eight_loss (δ : ℝ) (hδ : 0 < δ) : ∃ (t : ℝ), 0 < t ∧ t ≤ 1 ∧ 8 * (1 + t) ^ 3 ≤ 8 + δ

Choose a fixed loss before every varying clipped profile.

theorem G12ClippedWindow.primeOutput_uniformEight (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (g L U : ℕ → ℝ) (ε : ℝ), Admissible N ε g L U → primeOutput N g L U ≤ (8 + δ) * 400 * mass N g L U * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N / Real.log ↑N + δ * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The second logarithm for the actual ungated clipped prime outputs. No hypothesis on epsilon's sign or fixed-window choice is required.

noncomputable def G12ClippedWindow.highPrimeOutput (N : ℕ) (ε : ℝ) : ℝ

Literal high source prime outputs; the source mass remains ungated.

Equations

• G12ClippedWindow.highPrimeOutput N ε = 400 * ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ↑{r ∈ G12LowHighOutput.highWindow N ε m | Nat.Prime (N - r * m)}.card

theorem G12ClippedWindow.highPrimeOutput_uniformEight (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (ε : ℝ), highPrimeOutput N ε ≤ (8 + δ) * 400 * highMass N ε * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N / Real.log ↑N + δ * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)