CountingFromMain.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.marked_multiple_at_minimal_length line 21
Source documentation
Appending the complementary unit fraction and cleaning repetitions preserves an odd multiple.
```
theorem marked_multiple_at_minimal_length (Q : ℕ) (hQ : Odd Q) (hQone : 1 < Q) :
    ∃ n : Fin (egyptianLength (Q - 1) Q + 1) → ℕ,
      IsOneExpansion n ∧ ∃ i, Q ∣ n i := by
…
```
Mentions: OAI.Problem337.egyptianLength, OAI.Problem337.IsOneExpansion
theorem OAI.Problem337.marked_multiple_length_le_max line 44
Source documentation
The length of the cleaned marked expansion is bounded by the uniform maximum.
```
theorem marked_multiple_length_le_max (Q : ℕ) (hQ : Odd Q) (hQone : 1 < Q) :
    ∃ k : ℕ, ∃ n : Fin k → ℕ, IsOneExpansion n ∧ (∃ i, Q ∣ n i) ∧
      k ≤ maxEgyptianLength Q + 1 := by
…
```
Mentions: OAI.Problem337.IsOneExpansion, OAI.Problem337.maxEgyptianLength
theorem OAI.Problem337.divisor_branching_from_tuple line 52
Source documentation
Tuple form of divisor branching, avoiding conversion choices in the counting assembly.
```
theorem divisor_branching_from_tuple {k : ℕ} (n : Fin k → ℕ)
    (hn : IsOneExpansion n) (i : Fin k)
    (hfinite : (OneExpansions (k + 1)).Finite) :
    (n i).divisors.card ≤ F (k + 1) + 1 + 2 * (k - 1) := by
…
```
Mentions: OAI.Problem337.IsOneExpansion, OAI.Problem337.OneExpansions, OAI.Problem337.F

theorem OAI.Problem337.divisor_branching_from_odd_marker line 77

Source documentation

Branching on the marked multiple counts at least as many divisors as the marker itself.

theorem divisor_branching_from_odd_marker {Q k : ℕ} (hQ : Odd Q) (hQone : 1 < Q)
    (n : Fin k → ℕ) (hn : IsOneExpansion n) (hm : ∃ i, Q ∣ n i)
    (hfinite : (OneExpansions (k + 1)).Finite) :
    3 ≤ k ∧ Q.divisors.card ≤ F (k + 1) + 1 + 2 * (k - 1) := by
…

Mentions: OAI.Problem337.IsOneExpansion, OAI.Problem337.OneExpansions, OAI.Problem337.F

theorem OAI.Problem337.counting_from_uniform_max line 90
Source documentation
A short odd-marked expansion supplies a lower bound for the number of expansions one term longer.
```
theorem counting_from_uniform_max (Q : ℕ) (hQ : Odd Q) (hQone : 1 < Q)
    (hfinite : ∀ k, (OneExpansions k).Finite) :
    ∃ ell : ℕ, 4 ≤ ell ∧ ell ≤ maxEgyptianLength Q + 2 ∧
      Q.divisors.card ≤ F ell + 2 * ell := by
…
```
Mentions: OAI.Problem337.OneExpansions, OAI.Problem337.maxEgyptianLength, OAI.Problem337.F
theorem OAI.Problem337.eventually_collision_budget line 100
Source documentation
Exponential divisor counts eventually absorb the loss from the finitely many collisions.
```
theorem eventually_collision_budget (B : ℝ) (hB : 0 < B) :
    ∀ᶠ r : ℕ in atTop, 2 * B * Real.log (r : ℝ) ≤ (2 ^ (r - 1) : ℕ) := by
…
```

theorem OAI.Problem337.short_counting_lengths_of_uniform_upper line 120

Source documentation

Uniform logarithmic lengths and an odd many-divisor supply yield exponentially branching short lengths.

theorem short_counting_lengths_of_uniform_upper
    (hfinite : ∀ k, (OneExpansions k).Finite)
    (hupper : ∃ c : ℝ, 0 < c ∧ ∀ᶠ Q : ℕ in atTop,
      (maxEgyptianLength Q : ℝ) ≤ c * Real.log (Real.log (Q : ℝ)))
    (hsupply : ∃ C : ℝ, 0 < C ∧ ∀ᶠ r : ℕ in atTop,
      ∃ Q : ℕ, Odd Q ∧ 1 < Q ∧ 2 ^ r ≤ Q.divisors.card ∧
        Real.log (Real.log (Q : ℝ)) ≤ C * Real.log (r : ℝ)) :
    ∃ B : ℝ, 0 < B ∧ ∀ᶠ r : ℕ in atTop,
      ∃ ell : ℕ, 2 ≤ ell ∧ (ell : ℝ) ≤ B * Real.log (r : ℝ) ∧
        2 ^ (r - 1) ≤ F ell := by
…

Mentions: OAI.Problem337.OneExpansions, OAI.Problem337.maxEgyptianLength, OAI.Problem337.F

theorem OAI.Problem337.short_counting_lengths_of_main_upper line 164

Source documentation

The odd-primorial many-divisor input is unconditional, so only the main uniform upper bound remains in the short-counting-length construction.

theorem short_counting_lengths_of_main_upper
    (hupper : ∃ c : ℝ, 0 < c ∧ ∀ᶠ Q : ℕ in atTop,
      (maxEgyptianLength Q : ℝ) ≤ c * Real.log (Real.log (Q : ℝ))) :
    ∃ B : ℝ, 0 < B ∧ ∀ᶠ r : ℕ in atTop,
      ∃ ell : ℕ, 2 ≤ ell ∧ (ell : ℝ) ≤ B * Real.log (r : ℝ) ∧
        2 ^ (r - 1) ≤ F ell := by
…

Mentions: OAI.Problem337.maxEgyptianLength, OAI.Problem337.F

theorem OAI.Problem337.counting_order_of_main_upper line 182

Source documentation

The counting order theorem follows from the main uniform upper bound alone; this route does not use the quantitative prescribed-denominator construction.

theorem counting_order_of_main_upper
    (hupper : ∃ c : ℝ, 0 < c ∧ ∀ᶠ Q : ℕ in atTop,
      (maxEgyptianLength Q : ℝ) ≤ c * Real.log (Real.log (Q : ℝ))) :
    ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∃ k0 : ℕ,
      ∀ k : ℕ, k0 ≤ k →
        c * (k : ℝ) ≤ Real.log (Real.log (F k : ℝ)) ∧
        Real.log (Real.log (F k : ℝ)) ≤ C * (k : ℝ) := by
…

Mentions: OAI.Problem337.maxEgyptianLength, OAI.Problem337.F