CompositeSupplySize.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Size of the fourth-power supply for cube-free moduli

The fourth-power auxiliary integer has a controlled logarithmic size.

def OAI.Problem337.CompositeSupply.primeCount line 17
Source documentation
The global divisor pool uses twice the binary logarithm of its range.
```
def primeCount (u : ℕ) : ℕ := ⌈2 * Real.log (u : ℝ) / Real.log 2⌉₊
```
def OAI.Problem337.CompositeSupply.base line 20
Source documentation
The product of the first primeCount u primes.
```
def base (u : ℕ) : ℕ := primePrefixProduct (primeCount u)
```
Mentions: OAI.Problem337.primePrefixProduct, OAI.Problem337.CompositeSupply.primeCount
def OAI.Problem337.CompositeSupply.multiplier line 24
Source documentation
Two powers allow the bilinear products and two powers allow stripping all small-prime factors of a cube-free modulus.
```
def multiplier (m : ℕ) : ℕ := base (m ^ 4) ^ 4
```
Mentions: OAI.Problem337.CompositeSupply.base
lemma OAI.Problem337.CompositeSupply.base_pos line 26
lemma OAI.Problem337.CompositeSupply.multiplier_pos line 28
lemma OAI.Problem337.CompositeSupply.primeCount_eq_supplyPrimeCount line 30
lemma OAI.Problem337.CompositeSupply.base_fourth_power line 36
lemma OAI.Problem337.CompositeSupply.base_dvd_mono line 43
lemma OAI.Problem337.CompositeSupply.primeCount_le_of_not_dvd line 51
Source documentation
A prime not dividing the initial prime product is beyond its index cutoff.
```
lemma primeCount_le_of_not_dvd (u p : ℕ) (hp : p.Prime) (hnot : ¬ p ∣ base u) :
    primeCount u ≤ p := by
…
```
Mentions: OAI.Problem337.CompositeSupply.base, OAI.Problem337.CompositeSupply.primeCount
lemma OAI.Problem337.CompositeSupply.log_le_primeCount line 62
lemma OAI.Problem337.CompositeSupply.log_le_prime_of_not_dvd line 73
Source documentation
Every residual prime after removing the global pool is genuinely rough.
```
lemma log_le_prime_of_not_dvd (u p : ℕ) (hp : p.Prime) (hnot : ¬ p ∣ base u) :
    Real.log (u : ℝ) ≤ (p : ℝ) :=
…
```
Mentions: OAI.Problem337.CompositeSupply.base
lemma OAI.Problem337.CompositeSupply.scaled_log_le_prime_of_not_dvd line 79
Source documentation
The full cutoff coefficient is available when a dyadic shell requires roughness at log (2*u) rather than just log u.
```
lemma scaled_log_le_prime_of_not_dvd (u p : ℕ) (hp : p.Prime)
    (hnot : ¬ p ∣ base u) :
    2 * Real.log (u : ℝ) / Real.log 2 ≤ (p : ℝ) :=
…
```
Mentions: OAI.Problem337.CompositeSupply.base
lemma OAI.Problem337.CompositeSupply.log_double_le_prime_of_not_dvd line 84
lemma OAI.Problem337.CompositeSupply.base_squarefree line 101
lemma OAI.Problem337.CompositeSupply.square_le_divisors_card line 112
Source documentation
The divisor pool has the required quadratic cardinality.
```
lemma square_le_divisors_card (u : ℕ) : u ^ 2 ≤ (base u).divisors.card := by
…
```
Mentions: OAI.Problem337.CompositeSupply.base
lemma OAI.Problem337.CompositeSupply.square_le_base line 130
lemma OAI.Problem337.CompositeSupply.marker_lt_multiplier line 135
lemma OAI.Problem337.CompositeSupply.base_pow_dvd_multiplier line 147
Source documentation
Every variable smaller pool nests in the one global pool, including its fourth power.
```
lemma base_pow_dvd_multiplier {u m : ℕ} (hu : 0 < u) (hum : u ≤ m ^ 4) :
    base u ^ 4 ∣ multiplier m := pow_dvd_pow_of_dvd (base_dvd_mono hu hum) 4
```
Mentions: OAI.Problem337.CompositeSupply.base, OAI.Problem337.CompositeSupply.multiplier, OAI.Problem337.CompositeSupply.base_dvd_mono

theorem OAI.Problem337.CompositeSupply.eventually_log_base_le line 151

Source documentation

Uniform growth bound for the variable global divisor pool.

theorem eventually_log_base_le (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ u : ℕ in atTop,
      Real.log (base u : ℝ) ≤
        (2 / Real.log 2 + ε) * Real.log (u : ℝ) *
          Real.log (Real.log (u : ℝ)) := by
…

Mentions: OAI.Problem337.CompositeSupply.base

theorem OAI.Problem337.CompositeSupply.eventually_log_multiplier_le line 165
Source documentation
The sharp leading logarithmic size coefficient is the same as in the original marked construction. No prime-distribution theorem is assumed.
```
theorem eventually_log_multiplier_le (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ m : ℕ in atTop,
      Real.log (multiplier m : ℝ) ≤
        (32 / Real.log 2 + ε) * Real.log (m : ℝ) *
          Real.log (Real.log (m : ℝ)) := by
…
```
Mentions: OAI.Problem337.CompositeSupply.multiplier