GoldbachSieveRemainder.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The exact finite progression error for the binary Goldbach polynomial. No prime-distribution estimate or sieve-density lower bound is assumed here.

theorem OAI.Problem337.goldbachSieveRootCount_eq_filter_card line 16
Source documentation
The local root-count definition is the cardinality of the corresponding finite set whenever the modulus is nonzero.
```
theorem goldbachSieveRootCount_eq_filter_card (u d : ℕ) [NeZero d] :
    goldbachSieveRootCount u d =
      (Finset.univ.filter (fun x : ZMod d => x * ((u : ZMod d) - x) = 0)).card := by
…
```
Mentions: OAI.Problem337.goldbachSieveRootCount
theorem OAI.Problem337.goldbach_polynomial_dvd_iff_zmod line 25
Source documentation
On the natural interval used for ordered positive prime pairs, the truncated natural subtraction agrees with subtraction in the residue ring.
```
theorem goldbach_polynomial_dvd_iff_zmod (u d n : ℕ) (hn : n ≤ u) :
    d ∣ n * (u - n) ↔
      (n : ZMod d) * ((u : ZMod d) - (n : ZMod d)) = 0 := by
…
```

theorem OAI.Problem337.goldbach_polynomial_count_discrepancy line 32

Source documentation

Sharp, uniform error for counting divisibility of n*(u-n) on 1 ≤ n < u. The formulation includes the empty intervals at u=0 and u=1.

theorem goldbach_polynomial_count_discrepancy (u d : ℕ) [NeZero d] :
    |(((Finset.Icc 1 (u - 1)).filter (fun n => d ∣ n * (u - n))).card : ℝ) -
      ((u - 1 : ℕ) : ℝ) * goldbachSieveRootCount u d / d| ≤
        goldbachSieveRootCount u d := by
…

Mentions: OAI.Problem337.goldbachSieveRootCount

theorem OAI.Problem337.goldbach_polynomial_count_density_discrepancy line 54

Source documentation

The same error with the normalized multiplicative sieve density.

theorem goldbach_polynomial_count_density_discrepancy (u d : ℕ) [NeZero d] :
    |(((Finset.Icc 1 (u - 1)).filter (fun n => d ∣ n * (u - n))).card : ℝ) -
      goldbachSieveDensity u d * ((u - 1 : ℕ) : ℝ)| ≤
        goldbachSieveRootCount u d := by
…

Mentions: OAI.Problem337.goldbachSieveDensity, OAI.Problem337.goldbachSieveRootCount