PrimeSupply.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TreeEdit.BinaryLower.PrimeSupply.prime_counting_lower line 12

Source documentation

The elementary Chebyshev lower bound in the form used by the manuscript.

theorem prime_counting_lower :
    ∃ c : ℝ, 0 < c ∧ ∃ x₀ : ℝ, ∀ x : ℝ, x₀ ≤ x →
      c * x / Real.log x ≤ (Nat.primeCounting ⌊x⌋₊ : ℝ) := by
…

theorem OAI.TreeEdit.BinaryLower.PrimeSupply.prime_counting_pow_lower line 37
Source documentation
At polynomial arguments, the prime count eventually dominates twice the preceding power. This is a convenient intermediate form for interval counts.
```
theorem prime_counting_pow_lower (e : ℕ) :
    ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
      2 * k ^ e ≤ Nat.primeCounting (k ^ (e + 1)) := by
…
```
theorem OAI.TreeEdit.BinaryLower.PrimeSupply.primeCounting_le_interval_card_add line 84
Source documentation
Removing all integers below a from the primes at most b loses at most a primes. The inclusive lower endpoint matches the source interval convention.
```
theorem primeCounting_le_interval_card_add (a b : ℕ) :
    Nat.primeCounting b ≤ ((Finset.Icc a b).filter Nat.Prime).card + a := by
…
```
theorem OAI.TreeEdit.BinaryLower.PrimeSupply.primes_in_power_interval line 102
Source documentation
Consecutive polynomial powers contain at least the lower power in primes, for all sufficiently large bases.
```
theorem primes_in_power_interval (e : ℕ) :
    ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
      k ^ e ≤ ((Finset.Icc (k ^ e) (k ^ (e + 1))).filter Nat.Prime).card := by
…
```

theorem OAI.TreeEdit.BinaryLower.PrimeSupply.prime_supply line 113

Source documentation

Prime supply in the exact two intervals required by the manuscript.

theorem prime_supply :
    ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
      20 * k ^ 2 ≤ ((Finset.Icc (k ^ 4) (k ^ 5)).filter Nat.Prime).card ∧
      1600 * k < ((Finset.Icc (k ^ 2) (k ^ 3)).filter Nat.Prime).card := by
…

theorem OAI.TreeEdit.BinaryLower.PrimeSupply.finite_tree_prime_family line 134
Source documentation
The globally distinct prime family indexed by depth and child, as used in finite-tree.tex. An embedding makes distinctness over all pairs explicit.
```
theorem finite_tree_prime_family :
    ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
      ∃ p : (Fin k × Fin (20 * k)) ↪ ℕ,
        ∀ ji, Nat.Prime (p ji) ∧ k ^ 4 ≤ p ji ∧ p ji ≤ k ^ 5 := by
…
```
theorem OAI.TreeEdit.BinaryLower.PrimeSupply.finite_tree_odd_prime_family line 154
Source documentation
Strengthened finite-tree data: every selected prime is odd (expressed as strictly greater than two), uniformly over the entire depth/child index set.
```
theorem finite_tree_odd_prime_family :
    ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
      2 ≤ k ∧ ∃ p : (Fin k × Fin (20 * k)) ↪ ℕ,
        ∀ ji, Nat.Prime (p ji) ∧ 2 < p ji ∧ k ^ 4 ≤ p ji ∧ p ji ≤ k ^ 5 := by
…
```

theorem OAI.TreeEdit.BinaryLower.PrimeSupply.torus_prime_family line 174

Source documentation

The torus construction can sample an ordered list of 16*k distinct primes, since its prime pool has size strictly greater than 100*(16*k).

theorem torus_prime_family :
    ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
      100 * (16 * k) < ((Finset.Icc (k ^ 2) (k ^ 3)).filter Nat.Prime).card ∧
      ∃ p : Fin (16 * k) ↪ ℕ,
        ∀ i, Nat.Prime (p i) ∧ k ^ 2 ≤ p i ∧ p i ≤ k ^ 3 := by
…