noncomputable def G12LowHighOutput.highCut (N : ℕ) : ℝ

A closed real high cut is an open cut at the preceding natural number.

Equations

• G12LowHighOutput.highCut N = ↑(⌈↑N ^ (1 / 10)⌉₊ - 1)

noncomputable def G12LowHighOutput.highLo (N : ℕ) (ε : ℝ) (m : ℕ) : ℝ

Equations

• G12LowHighOutput.highLo N ε m = min (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m) (max (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m) (G12LowHighOutput.highCut N))

noncomputable def G12LowHighOutput.highWindow (N : ℕ) (ε : ℝ) (m : ℕ) : Finset ℕ

Equations

• G12LowHighOutput.highWindow N ε m = {r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m | ↑N ^ (1 / 10) ≤ ↑r}

theorem G12LowHighOutput.highCut_lt_iff (N r : ℕ) (hr : 0 < r) : highCut N < ↑r ↔ ↑N ^ (1 / 10) ≤ ↑r

theorem G12LowHighOutput.highLo_bounds {N m : ℕ} {ε : ℝ} (hN : 2 ≤ N) (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m ≤ highLo N ε m ∧ highLo N ε m ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m

theorem G12LowHighOutput.mem_highWindow (N m r : ℕ) (ε : ℝ) : r ∈ highWindow N ε m ↔ r ∈ Finset.range (N + 1) ∧ Nat.Prime r ∧ highLo N ε m < ↑r ∧ ↑r ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m

Literal closed-high prime window, not an arbitrary filtered SW assertion.

theorem G12LowHighOutput.highAPWindow_eq_sdiff {N m : ℕ} {ε : ℝ} (d b : ℕ) (hN : 2 ≤ N) (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) : {r ∈ highWindow N ε m | m * r ≡ b [MOD d]} = Wu2004MeanValue.scaledPrimeSet (↑m * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m) d b m \ Wu2004MeanValue.scaledPrimeSet (↑m * highLo N ε m) d b m

Exact AP identity at the same modulus and product residue.

theorem G12LowHighOutput.highAPWindow_card_eq_inverse {N m : ℕ} {ε : ℝ} (d b : ℕ) (hN : 2 ≤ N) (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) (hmd : m.Coprime d) : ↑{r ∈ highWindow N ε m | m * r ≡ b [MOD d]}.card = ↑(AnalyticNumberTheory.Sieve.primesInAP ⌊MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d)) - ↑(AnalyticNumberTheory.Sieve.primesInAP ⌊highLo N ε m⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d))

Actual AP cardinality: the high window has the unchanged inverse residue.

theorem G12LowHighOutput.highAPWindow_eq_output_dvd {N m : ℕ} {ε : ℝ} (d : ℕ) (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) : {r ∈ highWindow N ε m | m * r ≡ N [MOD d]} = {r ∈ highWindow N ε m | d ∣ N - r * m}

The AP test is literally divisibility of the original output.

theorem G12LowHighOutput.high_original_fiber {N m : ℕ} (ε : ℝ) (hm : m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) : {r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m | ↑N ^ (1 / 10) ≤ ↑r} = {r ∈ highWindow N ε m | ¬r ∣ N ∧ Nat.Prime (N - r * m)}

The high original output fibres use this very window, with their original coprimality gate and primality test retained.