theorem G12BandOutput.prime_indicator_nonneg (N m r : ℕ) : 0 ≤ if Nat.Prime (N - r * m) then 1 else 0

The output-prime indicator is nonnegative, including repeated representations.

noncomputable def G12BandOutput.badMass (N : ℕ) (g L U : ℕ → ℝ) : ℝ

Ungated source loss from the first-prime coprimality gate.

Equations

• G12BandOutput.badMass N g L U = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, g m * ↑{r ∈ G12ClippedWindow.window N L U m | ¬r.Coprime N}.card

noncomputable def G12BandOutput.goodMass (N : ℕ) (g L U : ℕ → ℝ) : ℝ

Physical mass retains short-prime coprimality, unlike the sieve source.

Equations

• G12BandOutput.goodMass N g L U = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, g m * ↑{r ∈ G12ClippedWindow.window N L U m | r.Coprime N}.card

theorem G12BandOutput.mass_split (N : ℕ) (g L U : ℕ → ℝ) : G12ClippedWindow.mass N g L U = goodMass N g L U + badMass N g L U

theorem G12BandOutput.badMass_le {N : ℕ} (hN : 4 ≤ N) {ε : ℝ} {g L U : ℕ → ℝ} (had : G12ClippedWindow.Admissible N ε g L U) : badMass N g L U ≤ 21 * ↑N / ↑N ^ (4 / 53)

Uniform transport for arbitrary admissible windows, not a cellwise estimate.

theorem G12BandOutput.clamp_admissible {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (T V : ℕ → ℝ) : G12ClippedWindow.Admissible N ε (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N) (G12ClippedWindow.clampLower N ε T V) (G12ClippedWindow.clampUpper N ε V)

Clamp without masking the original body coefficient.