RankDecay.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The high-rank square-root saving dominates the full crude counting cost.

lemma OAI.TwoPointCorrelations.sqrt_pow_le_exp line 13

lemma OAI.TwoPointCorrelations.reciprocal_rank_base_le line 22

Source documentation

The logarithmic prime-divisor count contributes only its logarithm to the exponent; the prime lower cutoff contributes the full negative term.

lemma reciprocal_rank_base_le (V H T D : ℝ) (M : ℕ)
    (hV : 1 ≤ V) (hH : Real.exp T ≤ H)
    (hM : 1 + (Nat.log 2 M : ℝ) ≤ Real.exp D) :
    (V * H)⁻¹ * (1 + (Nat.log 2 M : ℝ)) ≤ Real.exp (D - T) := by
…

lemma OAI.TwoPointCorrelations.natLog_le_linear line 39
Source documentation
Exponentially bounded integer coefficients have only linearly many possible logarithmic prime-divisor slots.
```
lemma natLog_le_linear (M : ℕ) (A L : ℝ) (hA : 0 ≤ A) (hL : 0 ≤ L)
    (hM : (M : ℝ) ≤ Real.exp (A * L)) :
    (Nat.log 2 M : ℝ) ≤ A * L / Real.log 2 := by
…
```
lemma OAI.TwoPointCorrelations.eventually_rank_log_budget line 52

lemma OAI.TwoPointCorrelations.eventually_column_minor_size_exp line 73

Source documentation

The actual coefficient bound 2 R h Q D B is at most exp (105 L) for the manuscript padding and other-column ranges.

lemma eventually_column_minor_size_exp (h : ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ R Q D B : ℕ,
      (R : ℝ) ≤ 2 * L → (Q : ℝ) ≤ Real.exp (100 * L + 1) →
      (D : ℝ) ≤ Real.exp (2 * L) → (B : ℝ) ≤ Real.exp L →
      ((2 * R * (h * Q * D) * B : ℕ) : ℝ) ≤ Real.exp (105 * L) := by
…

lemma OAI.TwoPointCorrelations.eventually_crude_cost_small line 100

Source documentation

Quantitative form of log² L = o(L^(3/200)), multiplied by L.

lemma eventually_crude_cost_small (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, C * L * (Real.log L) ^ 2 ≤ (1 / 8 : ℝ) * L ^ (203 / 200 : ℝ) := by
…

lemma OAI.TwoPointCorrelations.eventually_rank_floor_bounds line 125
Source documentation
The floor in r = floor(L^(1/50)) loses at most half the rank once L is large; its upper bound is only L, sufficient for every overhead.
```
lemma eventually_rank_floor_bounds :
    ∀ᶠ L : ℝ in atTop,
      L ^ (1 / 50 : ℝ) / 2 ≤ (⌊L ^ (1 / 50 : ℝ)⌋₊ : ℝ) ∧
        (⌊L ^ (1 / 50 : ℝ)⌋₊ : ℝ) ≤ L := by
…
```

theorem OAI.TwoPointCorrelations.eventually_high_rank_decay line 141

Source documentation

The exact exponent 203/200 = 199/200 + 1/50 is retained. Fixed coefficients in the crude enumeration only affect the threshold.

theorem eventually_high_rank_decay (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ r : ℕ,
      L ^ (1 / 50 : ℝ) / 2 ≤ (r : ℝ) → (r : ℝ) ≤ L →
      Real.exp (C * L * (Real.log L) ^ 2) *
        Real.sqrt ((Real.exp (C * Real.log L - L ^ (199 / 200 : ℝ))) ^ r) ≤
          Real.exp (-(1 / 8 : ℝ) * L ^ (203 / 200 : ℝ)) := by
…

theorem OAI.TwoPointCorrelations.eventually_high_rank_total line 178

Source documentation

Numerical conclusion after summing the actual word records. The coefficient of the counting exponent is fixed; it does not affect the absolute decay exponent or constant.

theorem eventually_high_rank_total (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ (r M : ℕ) (V H cost total : ℝ),
      L ^ (1 / 50 : ℝ) / 2 ≤ (r : ℝ) → (r : ℝ) ≤ L →
      1 ≤ V → Real.exp (L ^ (199 / 200 : ℝ)) ≤ H →
      1 + (Nat.log 2 M : ℝ) ≤ Real.exp (C * Real.log L) →
      0 ≤ cost → cost ≤ Real.exp (C * L * (Real.log L) ^ 2) →
      total ≤ cost * Real.sqrt (((V * H)⁻¹ * (1 + (Nat.log 2 M : ℝ))) ^ r) →
      total ≤ Real.exp (-(1 / 8 : ℝ) * L ^ (203 / 200 : ℝ)) := by
…