theorem G12ClippedWindow.primeOutput_eq_indicator (N : ℕ) (g L U : ℕ → ℝ) : primeOutput N g L U = 400 * ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, g m * ∑ r ∈ window N L U m, if Nat.Prime (N - r * m) then 1 else 0

The literal indicator sum, including all repeated output representations.

noncomputable def G12ClippedWindow.coprimePrimeOutput (N : ℕ) (g L U : ℕ → ℝ) : ℝ

Coprime-r physical subcount. The common source mass is deliberately not renamed.

Equations

• G12ClippedWindow.coprimePrimeOutput N g L U = 400 * ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, g m * ↑{r ∈ G12ClippedWindow.window N L U m | r.Coprime N ∧ Nat.Prime (N - r * m)}.card

noncomputable def G12ClippedWindow.noncoprimePrimeOutput (N : ℕ) (g L U : ℕ → ℝ) : ℝ

Retained r|N contribution; it is included in the ungated sieve, not silently deleted.

Equations

• G12ClippedWindow.noncoprimePrimeOutput N g L U = 400 * ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, g m * ↑{r ∈ G12ClippedWindow.window N L U m | ¬r.Coprime N ∧ Nat.Prime (N - r * m)}.card

theorem G12ClippedWindow.primeOutput_split_coprime (N : ℕ) (g L U : ℕ → ℝ) : primeOutput N g L U = coprimePrimeOutput N g L U + noncoprimePrimeOutput N g L U

theorem G12ClippedWindow.coprimePrimeOutput_le {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (h : Admissible N ε g L U) : coprimePrimeOutput N g L U ≤ primeOutput N g L U

theorem G12ClippedWindow.equal_endpoints_empty (N : ℕ) (L : ℕ → ℝ) (m : ℕ) : window N L L m = ∅

theorem G12ClippedWindow.equal_endpoints_zero (N : ℕ) (g L : ℕ → ℝ) : primeOutput N g L L = 0 ∧ mass N g L L = 0

theorem G12ClippedWindow.physical_high_le_source (N : ℕ) (ε : ℝ) : G12LowHighOutput.outputCount N (G12LowHighOutput.high N ε) ≤ highPrimeOutput N ε

The original physical high count embeds in the actual ungated high source. The common mass on the right is highMass, not a coprime physical mass.

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

Original high output theorem, with no subtraction of upper bounds.

theorem G12ClippedWindow.actual_output_uniformEight (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (g L U : ℕ → ℝ) (ε : ℝ), Admissible N ε g L U → (400 * ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, g m * ∑ r ∈ window N L U m, if Nat.Prime (N - r * m) then 1 else 0) ≤ ((8 + δ) * 400 * ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, g m * ↑(window N L U m).card) * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N / Real.log ↑N + δ * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Expanded publication-facing endpoint: the exact indicator sum, not a proxy.