theorem G12ClippedWindow.output_upperErrSum_le {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (hEven : Even N) (h : Admissible N ε g L U) (Z : ℝ) (D Q : ℕ) (hDQ : D ≤ Q + 1) : have S := outputSieve N hEven g L U ε h Z (mass N g L U); have P := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z; MathlibNt.SieveTheory.LinearSieve.upperErrSum S D (MathlibNt.SieveTheory.LinearSieve.upperRosserWeight P D) ≤ ∑ d ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedModuli N Q, |commonResidual N g L U d|

Full ordinary Rosser support, including d=1; no depth or weight modification.

theorem G12ClippedWindow.siftedMass_le_rosserFactor (ρ : ℝ) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), ∀ (N : ℕ) (hEven : Even N) (g L U : ℕ → ℝ) (ε : ℝ) (h : Admissible N ε g L U) (Z Δ s : ℝ), z₀ ≤ Z → 2 ≤ Z → 0 < Δ → s = Real.log Δ / Real.log Z → 3 / 2 ≤ s → s ≤ 4 → have X := mass N g L U; have S := outputSieve N hEven g L U ε h Z X; have P := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z; siftedMass N g L U Z ≤ X * (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PrimeProduct N Z + MathlibNt.SieveTheory.LinearSieve.upperErrSum S (⌊Δ⌋₊ + 1) (MathlibNt.SieveTheory.LinearSieve.upperRosserWeight P (⌊Δ⌋₊ + 1))

The density theorem sees exactly the inherited product and multiplicative density.

theorem G12ClippedWindow.primeOutput_le_paidRosser (A ρ : ℝ) (hA : 0 < A) (hρ : 0 < ρ) : ∃ (B : ℝ) (C : ℝ) (z₀ : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (g L U : ℕ → ℝ) (ε Z Δ s : ℝ), Admissible N ε g L U → z₀ ≤ Z → 2 ≤ Z → 0 < Δ → s = Real.log Δ / Real.log Z → 3 / 2 ≤ s → s ≤ 4 → Δ ≤ √↑N / Real.log ↑N ^ B → primeOutput N g L U ≤ 400 * mass N g L U * (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PrimeProduct N Z + 400 * C * ↑N / Real.log ↑N ^ A + 8000 * ↑⌈Z⌉₊

Actual ungated output count with common source mass and fully paid distribution. The witnesses precede all long weights, endpoints, and epsilon.