Resources.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Exact resource exponents

Rational arithmetic for res:tuple-exponent and res:exponent-relations in A Low-Space Algorithm for Worst-Case Subset Sum. The numerical hypotheses relate leaf, dictionary, buffer, and raw-tuple exponential rates.

def OAI.LowSpaceSubsetSum.mixerSize line 19
Source documentation
The block size is divisible by eight; n counts indices, not input bits.
```
def mixerSize (n : ℕ) : ℕ := 8 * (3 * n / 100)
```
theorem OAI.LowSpaceSubsetSum.mixerSize_bounds line 21
def OAI.LowSpaceSubsetSum.pairExponent line 36
Source documentation
Analysis scale for the number of low-filtered raw child pairs.
```
noncomputable def pairExponent (n m h fmax : ℝ) : ℝ :=
…
```
def OAI.LowSpaceSubsetSum.entryExponent line 40
Source documentation
Analysis scale for distinct valid parent entries.
```
noncomputable def entryExponent (n m hbar d f0 : ℝ) : ℝ :=
…
```
def OAI.LowSpaceSubsetSum.extraPrimeExponent line 44
Source documentation
The additional-prime exponent.
```
noncomputable def extraPrimeExponent (n m fmax : ℝ) : ℝ :=
…
```
theorem OAI.LowSpaceSubsetSum.regeneration_exponent line 48
Source documentation
Regenerating the pair streams preserves the exact half-exponential rate.
```
theorem regeneration_exponent (n m h fmax : ℝ)
    (hm : 0 ≤ m) (hh : h ≤ 4057 / 5000) :
    extraPrimeExponent n m fmax + pairExponent n m h fmax ≤ n / 2 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.extraPrimeExponent, OAI.LowSpaceSubsetSum.pairExponent
theorem OAI.LowSpaceSubsetSum.matching_exponent line 55
Source documentation
The separator occurrence factor also preserves the exact time rate.
```
theorem matching_exponent (n m h hbar d f0 : ℝ)
    (hm : 0 ≤ m) (hh : hbar ≤ h) (hf : f0 ≤ d) :
    entryExponent n m hbar d f0 + (1 - h) * m ≤ n / 2 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.entryExponent

theorem OAI.LowSpaceSubsetSum.bucket_exponent_gap line 62

Source documentation

The extra prime has a strict margin over the space-scaled entry count.

theorem bucket_exponent_gap (n m h hbar d f0 fmax : ℝ)
    (hn : 10000 ≤ n) (hm : (6 / 25) * n - 8 ≤ m)
    (hh : h ≤ 4057 / 5000) (hbar_le : hbar ≤ h)
    (hf0 : f0 ≤ d / 2) (hfmax : fmax ≤ d / 2 + n / 4000) :
    (3 / 2000) * n ≤
      extraPrimeExponent n m fmax - (entryExponent n m hbar d f0 - (199 / 1000) * n) := by
…

Mentions: OAI.LowSpaceSubsetSum.extraPrimeExponent, OAI.LowSpaceSubsetSum.entryExponent

theorem OAI.LowSpaceSubsetSum.tuple_exponent line 74

Source documentation

Raw four-leaf tuple counts fit the exact time exponent after low filtering.

theorem tuple_exponent (n m h beta f0 fj : ℝ)
    (hn : 3000 ≤ n) (hm : (6 / 25) * n - 8 ≤ m)
    (hh : h ≤ 4057 / 5000)
    (hb : beta ≤ n / 4 + (-3 / 4 + 3 / 2 * h) * m)
    (hf0 : f0 ≤ (39 / 5000) * n) (hfj : fj ≤ (39 / 5000) * n) :
    2 * beta - (m / 2 - f0) - (m / 2 - fj) ≤ n / 2 := by
…

theorem OAI.LowSpaceSubsetSum.leaf_exponent line 85

Source documentation

Every raw leaf is below the buffer and dictionary rates with fixed slack.

theorem leaf_exponent (n m h beta : ℝ)
    (hm0 : 0 ≤ m) (hm : m ≤ (6 / 25) * n)
    (hh : h ≤ 4057 / 5000)
    (hb : beta ≤ n / 4 + (-3 / 4 + 3 / 2 * h) * m) :
    beta / 2 ≤ (45263 / 250000) * n := by
…

theorem OAI.LowSpaceSubsetSum.polynomial_absorption line 94

Source documentation

A fixed polynomial is eventually absorbed by any positive base-two rate.

theorem polynomial_absorption (k : ℕ) {eps : ℝ} (heps : 0 < eps) :
    ∀ᶠ n : ℕ in atTop, (n : ℝ) ^ k ≤ (2 : ℝ) ^ (eps * n) := by
…

theorem OAI.LowSpaceSubsetSum.polynomial_bit_bound line 106
Source documentation
The polynomial-bit promise gives a polynomial bound with no input for c.
```
theorem polynomial_bit_bound {n b c : ℕ} (hn : 2 ≤ n) (hc : 0 < c)
    (hb : b ≤ n ^ c) : n + b + 2 ≤ 3 * n ^ c := by
…
```

theorem OAI.LowSpaceSubsetSum.absorb_space_polynomial line 116

Source documentation

The ordinary exponential space corollary, as a numeric bound implication.

This applies to an actual algorithm only after its intermediate space bound has been established; it is not a replacement for that main theorem.

theorem absorb_space_polynomial {rho : ℝ} (hrho : (199 / 1000 : ℝ) < rho)
    (c : ℕ) (hc : 0 < c) :
    ∀ᶠ n : ℕ in atTop, ∀ b : ℕ, b ≤ n ^ c →
      ((n + b + 2 : ℕ) : ℝ) ^ 15 * (2 : ℝ) ^ ((199 / 1000 : ℝ) * n) ≤
        (3 : ℝ) ^ 15 * (2 : ℝ) ^ (rho * n) := by
…

theorem OAI.LowSpaceSubsetSum.one_fifth_space_polynomial line 146

Source documentation

The chosen exponent 1/5 has the strict margin needed for absorption.

theorem one_fifth_space_polynomial (c : ℕ) (hc : 0 < c) :
    ∀ᶠ n : ℕ in atTop, ∀ b : ℕ, b ≤ n ^ c →
      ((n + b + 2 : ℕ) : ℝ) ^ 15 * (2 : ℝ) ^ ((199 / 1000 : ℝ) * n) ≤
        (3 : ℝ) ^ 15 * (2 : ℝ) ^ ((1 / 5 : ℝ) * n) :=
…