Main.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Worst-case Subset Sum in one-fifth-exponential space

The threshold is chosen once from its proved existence theorem. No solution, deficiency statistic, or bit-length exponent is an input. The finite random-word experiment has one-sided correctness, success probability at least two thirds, and bounds on its operation and writable-storage counts on every outcome.

def OAI.LowSpaceSubsetSum.algorithm line 16

theorem OAI.LowSpaceSubsetSum.worst_case_subset_sum line 20

Source documentation

One-sided randomized correctness and all-outcome resource-count bounds.

theorem worst_case_subset_sum :
    (∀ (n : ℕ) (I : Instance n) (words : WordFinalDecision.Words I),
      (algorithm I words).1.1 = true → Solvable I) ∧
    (∀ (n : ℕ) (I : Instance n), Solvable I →
      (2/3 : ℝ) ≤ (FiniteLaw.uniform : FiniteLaw (WordFinalDecision.Words I)).probability
        (fun words => (algorithm I words).1.1 = true)) ∧
    (∀ c : ℕ, 0 < c → ∀ᶠ n : ℕ in Filter.atTop,
      ∀ I : Instance n, inputBits I ≤ n^c → ∀ words : WordFinalDecision.Words I,
        ((algorithm I words).1.2 : ℝ) ≤
          (4*(3 : ℝ)^624)*(n : ℝ)^(624*c)*(2 : ℝ)^((1/2 : ℝ)*n) ∧
        ((algorithm I words).2 : ℝ) ≤
          2*(inputScale I : ℝ)^15*(2 : ℝ)^((199/1000 : ℝ)*n)) :=
…

Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.WordFinalDecision.Words, OAI.LowSpaceSubsetSum.algorithm, OAI.LowSpaceSubsetSum.Solvable, OAI.LowSpaceSubsetSum.FiniteLaw.uniform, OAI.LowSpaceSubsetSum.FiniteLaw, OAI.LowSpaceSubsetSum.inputBits, OAI.LowSpaceSubsetSum.inputScale

theorem OAI.LowSpaceSubsetSum.exponential_space line 37

Source documentation

The writable-storage count has every fixed exponential rate above .199.

theorem exponential_space (rho : ℝ) (hrho : (199/1000 : ℝ) < rho) (c : ℕ) (hc : 0 < c) :
    ∀ᶠ n : ℕ in Filter.atTop, ∀ I : Instance n, inputBits I ≤ n^c →
      ∀ words : WordFinalDecision.Words I,
        ((algorithm I words).1.2 : ℝ) ≤
          (4*(3 : ℝ)^624)*(n : ℝ)^(624*c)*(2 : ℝ)^((1/2 : ℝ)*n) ∧
        ((algorithm I words).2 : ℝ) ≤ (2*(3 : ℝ)^15)*(2 : ℝ)^(rho*n) :=
…

Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.inputBits, OAI.LowSpaceSubsetSum.WordFinalDecision.Words, OAI.LowSpaceSubsetSum.algorithm

theorem OAI.LowSpaceSubsetSum.one_fifth_space line 46

Source documentation

In particular, ordinary one-fifth-exponential writable space.

theorem one_fifth_space (c : ℕ) (hc : 0 < c) :
    ∀ᶠ n : ℕ in Filter.atTop, ∀ I : Instance n, inputBits I ≤ n^c →
      ∀ words : WordFinalDecision.Words I,
        ((algorithm I words).1.2 : ℝ) ≤
          (4*(3 : ℝ)^624)*(n : ℝ)^(624*c)*(2 : ℝ)^((1/2 : ℝ)*n) ∧
        ((algorithm I words).2 : ℝ) ≤ (2*(3 : ℝ)^15)*(2 : ℝ)^((1/5 : ℝ)*n) :=
…

Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.inputBits, OAI.LowSpaceSubsetSum.WordFinalDecision.Words, OAI.LowSpaceSubsetSum.algorithm

theorem OAI.LowSpaceSubsetSum.algorithm_word_width line 54