theorem G12ClippedWindow.high_admissible {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) : Admissible N ε (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N) (G12LowHighOutput.highLo N ε) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N)

The high specialization retains the original normalized product coefficient.

theorem G12ClippedWindow.high_window (N m : ℕ) (ε : ℝ) : window N (G12LowHighOutput.highLo N ε) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N) m = G12LowHighOutput.highWindow N ε m

noncomputable def G12ClippedWindow.highAPResidual (N : ℕ) (ε : ℝ) (d b : ℕ) : ℝ

This is the actual high AP count, not a residual defined by subtraction from low.

Equations

• G12ClippedWindow.highAPResidual N ε d b = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N with m.Coprime d, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * (↑{r ∈ G12LowHighOutput.highWindow N ε m | m * r ≡ b [MOD d]}.card - ↑(G12LowHighOutput.highWindow N ε m).card / ↑d.totient)

theorem G12ClippedWindow.highAPResidual_eq {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (d b : ℕ) : highAPResidual N ε d b = residual N (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N) (G12LowHighOutput.highLo N ε) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N) d b

The actual high AP producer is consumed at the unchanged inverse residue.

theorem G12ClippedWindow.highAPResidual_weighted (A : ℝ) (hA : 0 < A) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ) (Q : ℕ) (b : ℕ → ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ B → (∀ d ∈ Finset.Icc 1 Q, (b d).Coprime d) → ∑ d ∈ Finset.Icc 1 Q, Wu2004MeanValue.wuModulusWeight d * |highAPResidual N ε d (b d)| ≤ C * ↑N / Real.log ↑N ^ A

A weighted estimate for the literal high AP residual with one common source.

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

The actual high mass is independent of d.

Equations

• G12ClippedWindow.highMass N ε = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ↑(G12LowHighOutput.highWindow N ε m).card

noncomputable def G12ClippedWindow.highCommonResidual (N : ℕ) (ε : ℝ) (d : ℕ) : ℝ

Equations

• G12ClippedWindow.highCommonResidual N ε d = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ↑{r ∈ G12LowHighOutput.highWindow N ε m | d ∣ N - r * m}.card - G12ClippedWindow.highMass N ε / ↑d.totient

theorem G12ClippedWindow.highCommonResidual_eq (N : ℕ) (ε : ℝ) (d : ℕ) : highCommonResidual N ε d = commonResidual N (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N) (G12LowHighOutput.highLo N ε) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N) d

theorem G12ClippedWindow.highCommonResidual_eq_AP {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (d : ℕ) (hNd : N.Coprime d) : highCommonResidual N ε d = highAPResidual N ε d N - gateLoss N (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N) (G12LowHighOutput.highLo N ε) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N) d

Exact bridge from the actual high AP consumer to its common mass.

theorem G12ClippedWindow.highCommonResidual_log_saving (A : ℝ) (hA : 0 < A) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ) (Q : ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ B → ∑ d ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedModuli N Q, |highCommonResidual N ε d| ≤ C * ↑N / Real.log ↑N ^ A

Paid high common-mass distribution. It is not full upper bound minus low upper bound.

noncomputable def G12ClippedWindow.longMask (N : ℕ) (cellLong longOK : ℕ → Prop) (m : ℕ) : ℝ

Only the long cofactor is masked; no short-prime selection is hidden here.

Equations

• G12ClippedWindow.longMask N cellLong longOK m = if cellLong m ∧ ¬longOK m then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m else 0

noncomputable def G12ClippedWindow.clampUpper (N : ℕ) (ε : ℝ) (V : ℕ → ℝ) (m : ℕ) : ℝ

Normalize an empty upper window to oldLo, rather than asserting an unchecked endpoint ≥ 2.

Equations

• G12ClippedWindow.clampUpper N ε V m = max (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m) (min (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m) (V m))

noncomputable def G12ClippedWindow.clampLower (N : ℕ) (ε : ℝ) (T V : ℕ → ℝ) (m : ℕ) : ℝ

Equations

• G12ClippedWindow.clampLower N ε T V m = min (G12ClippedWindow.clampUpper N ε V m) (max (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m) (T m))

theorem G12ClippedWindow.clamp_admissible {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (cellLong longOK : ℕ → Prop) (T V : ℕ → ℝ) : Admissible N ε (longMask N cellLong longOK) (clampLower N ε T V) (clampUpper N ε V)

theorem G12ClippedWindow.clampUpper_eq_raw {N m : ℕ} {ε : ℝ} {V : ℕ → ℝ} (hN : 2 ≤ N) (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) (hV : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m ≤ V m) : clampUpper N ε V m = min (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m) (V m)

theorem G12ClippedWindow.clamp_empty_below_oldLo {N m : ℕ} {ε : ℝ} {T V : ℕ → ℝ} (hV : V m ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m) : clampLower N ε T V m = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m ∧ clampUpper N ε V m = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m

theorem G12ClippedWindow.clamp_endpoints_two {N : ℕ} (hN : 2 ≤ N) (hz : 2 ≤ ↑N ^ (4 / 53)) (ε : ℝ) (T V : ℕ → ℝ) {m : ℕ} (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) : 2 ≤ clampLower N ε T V m ∧ 2 ≤ clampUpper N ε V m

Even the empty-window endpoints meet the producer's lower endpoint requirement.

theorem G12ClippedWindow.longMask_common_log_saving (A : ℝ) (hA : 0 < A) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (cellLong longOK : ℕ → Prop) (T V : ℕ → ℝ) (ε : ℝ) (Q : ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ B → ∑ d ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedModuli N Q, |commonResidual N (longMask N cellLong longOK) (clampLower N ε T V) (clampUpper N ε V) d| ≤ C * ↑N / Real.log ↑N ^ A

The generic common-mass estimate applies uniformly to every pure long mask and cell.