WordMain.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Time and space guarantees for the bounded randomized decision procedure

main_resources bounds the work and storage counters with fixed threshold T. space_corollary absorbs the polynomial storage factor for every rate above .199. All resource quantifiers range over every random-word outcome, while the procedure and threshold are independent of the polynomial-bit exponent.

theorem OAI.LowSpaceSubsetSum.WordMain.double_time line 18
theorem OAI.LowSpaceSubsetSum.WordMain.main_resources line 20
theorem OAI.LowSpaceSubsetSum.WordMain.space_corollary line 46

theorem OAI.LowSpaceSubsetSum.WordMain.conditional_main line 62

Source documentation

One-sided correctness and one-fifth-exponential storage for any fixed threshold satisfying the large-input conditions.

theorem conditional_main (T : DecisionThreshold) :
    (∀ (n : ℕ) (I : Instance n) (words : WordFinalDecision.Words I),
      (WordFinalDecision.run T I words).1.1 = true → Solvable I) ∧
    (∀ (n : ℕ) (I : Instance n), Solvable I →
      (2/3 : ℝ) ≤ (FiniteLaw.uniform : FiniteLaw (WordFinalDecision.Words I)).probability
        (fun words => (WordFinalDecision.run T I words).1.1 = true)) ∧
    (∀ c : ℕ, 0 < c → ∀ᶠ n : ℕ in atTop,
      ∀ I : Instance n, inputBits I ≤ n^c → ∀ words : WordFinalDecision.Words I,
        ((WordFinalDecision.run T I words).1.2 : ℝ) ≤
          (4*(3 : ℝ)^624)*(n : ℝ)^(624*c)*(2 : ℝ)^((1/2 : ℝ)*n) ∧
        ((WordFinalDecision.run T I words).2 : ℝ) ≤
          (2*(3 : ℝ)^15)*(2 : ℝ)^((1/5 : ℝ)*n)) := by
…

Mentions: OAI.LowSpaceSubsetSum.DecisionThreshold, OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.WordFinalDecision.Words, OAI.LowSpaceSubsetSum.WordFinalDecision.run, OAI.LowSpaceSubsetSum.Solvable, OAI.LowSpaceSubsetSum.FiniteLaw.uniform, OAI.LowSpaceSubsetSum.FiniteLaw, OAI.LowSpaceSubsetSum.inputBits