GoldbachSieveLocal.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Finite local arithmetic for a possible binary Goldbach sieve. These results count roots of the polynomial x * (u - x) and provide its multiplicative local density. They do not assert any prime-pair bound or positive density of Goldbach numbers.

def OAI.Problem337.GoldbachSieveRoot line 18
Source documentation
Residue classes removed by the binary Goldbach sieve.
```
def GoldbachSieveRoot (u d : ℕ) :=
…
```
def OAI.Problem337.goldbachSieveRootCount line 22
Source documentation
Local number of roots of x * (u - x) modulo d.
```
def goldbachSieveRootCount (u d : ℕ) : ℕ :=
…
```
def OAI.Problem337.goldbachSieveRootEquiv line 26
Source documentation
The Chinese remainder theorem separates the local root conditions.
```
def goldbachSieveRootEquiv (u a b : ℕ) (hab : a.Coprime b) :
    GoldbachSieveRoot u (a * b) ≃
      GoldbachSieveRoot u a × GoldbachSieveRoot u b := by
…
```
Mentions: OAI.Problem337.GoldbachSieveRoot
theorem OAI.Problem337.goldbachSieveRootCount_mul line 41
Source documentation
Root counts are multiplicative at coprime moduli, with no distribution hypothesis.
```
theorem goldbachSieveRootCount_mul (u a b : ℕ) (hab : a.Coprime b) :
    goldbachSieveRootCount u (a * b) =
      goldbachSieveRootCount u a * goldbachSieveRootCount u b := by
…
```
Mentions: OAI.Problem337.goldbachSieveRootCount
theorem OAI.Problem337.goldbachSieveRootCount_one line 47
theorem OAI.Problem337.goldbachSieveRootCount_prime line 55
Source documentation
At a prime, the only roots are zero and the target residue.
```
theorem goldbachSieveRootCount_prime (u p : ℕ) (hp : p.Prime) :
    goldbachSieveRootCount u p = if p ∣ u then 1 else 2 := by
…
```
Mentions: OAI.Problem337.goldbachSieveRootCount

theorem OAI.Problem337.goldbachSieveRootCount_prod_primes line 73

Source documentation

A finite product of distinct primes gives the product of the local counts.

theorem goldbachSieveRootCount_prod_primes (u : ℕ) (s : Finset ℕ)
    (hs : ∀ p ∈ s, p.Prime) :
    goldbachSieveRootCount u (∏ p ∈ s, p) =
      ∏ p ∈ s, goldbachSieveRootCount u p := by
…

Mentions: OAI.Problem337.goldbachSieveRootCount

theorem OAI.Problem337.goldbachSieveRootCount_squarefree line 93
Source documentation
Exact squarefree local factor for the binary Goldbach sieve.
```
theorem goldbachSieveRootCount_squarefree (u d : ℕ) (hd : Squarefree d) :
    goldbachSieveRootCount u d =
      ∏ p ∈ d.primeFactors, if p ∣ u then 1 else 2 := by
…
```
Mentions: OAI.Problem337.goldbachSieveRootCount
def OAI.Problem337.goldbachSieveDensity line 109
Source documentation
The exact finite local root density, normalized as an arithmetic function.
```
def goldbachSieveDensity (u : ℕ) : ArithmeticFunction ℝ where
…
```
theorem OAI.Problem337.goldbachSieveDensity_apply line 113
theorem OAI.Problem337.goldbachSieveDensity_isMultiplicative line 117
Source documentation
The finite local density has exactly the multiplicativity required by a sieve.
```
theorem goldbachSieveDensity_isMultiplicative (u : ℕ) :
    (goldbachSieveDensity u).IsMultiplicative := by
…
```
Mentions: OAI.Problem337.goldbachSieveDensity
theorem OAI.Problem337.goldbachSieveDensity_prime line 126
Source documentation
The local density at a prime is 1/p or 2/p.
```
theorem goldbachSieveDensity_prime (u p : ℕ) (hp : p.Prime) :
    goldbachSieveDensity u p = if p ∣ u then 1 / (p : ℝ) else 2 / (p : ℝ) := by
…
```
Mentions: OAI.Problem337.goldbachSieveDensity
theorem OAI.Problem337.goldbachSieveDensity_prime_pos line 132
Source documentation
All prime local root densities are positive.
```
theorem goldbachSieveDensity_prime_pos (u p : ℕ) (hp : p.Prime) :
    0 < goldbachSieveDensity u p := by
…
```
Mentions: OAI.Problem337.goldbachSieveDensity
theorem OAI.Problem337.goldbachSieveDensity_prime_lt_one line 139
Source documentation
At odd primes the sieve is nondegenerate. At two, this requires an even target.
```
theorem goldbachSieveDensity_prime_lt_one (u p : ℕ) (hp : p.Prime)
    (hparity : p = 2 → 2 ∣ u) : goldbachSieveDensity u p < 1 := by
…
```
Mentions: OAI.Problem337.goldbachSieveDensity