OAI/Combinatorics/LowSpaceSubsetSum/Search/PreparedParentExecution.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Parent execution with shared prepared arrays

Both arrays and both initial tournaments are built once. The two contexts are then passed by value to the counted join. Its returned dictionary and counters have a type independent of the hidden tournament depths.

  1. structure OAI.LowSpaceSubsetSum.PreparedParentExecution.Result line 16
  2. def OAI.LowSpaceSubsetSum.PreparedParentExecution.project line 23
  3. def OAI.LowSpaceSubsetSum.PreparedParentExecution.runContexts line 27
  4. def OAI.LowSpaceSubsetSum.PreparedParentExecution.collect line 35
  5. theorem OAI.LowSpaceSubsetSum.PreparedParentExecution.runContexts_source line 43
  6. theorem OAI.LowSpaceSubsetSum.PreparedParentExecution.collect_value line 53

    Source documentation

    Exact stored dictionary, counters and termination flag, after setup.

    theorem collect_value (D : RepresentationParentData n) (F : IndexedMask n)
    (P : StoredRestriction n) (hF : F.semantic = D.signs) (B fuel₀ fuel₁ control : ℕ)
    (h₀ : fuel₀ = (D.pair 0).lengthBound) (h₁ : fuel₁ = (D.pair 1).lengthBound)
    (hcontrol : control = fuel₀ + fuel₁ + 1) :
    (collect D F P hF B fuel₀ fuel₁ control).1 =
      project (StoredParentExecution.collect {D with maskRestriction := P.semantic} F hF B).1 := by
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationParentData, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.StoredRestriction, OAI.LowSpaceSubsetSum.PreparedParentExecution.collect, OAI.LowSpaceSubsetSum.PreparedParentExecution.project, OAI.LowSpaceSubsetSum.StoredParentExecution.collect

  7. theorem OAI.LowSpaceSubsetSum.PreparedParentExecution.collect_work line 66

    Source documentation

    Setup is charged once per child stream, followed by the exact join ledger.

    theorem collect_work (D : RepresentationParentData n) (F : IndexedMask n)
    (P : StoredRestriction n) (hF : F.semantic = D.signs) (B fuel₀ fuel₁ control C : ℕ)
    (h₀ : fuel₀ = (D.pair 0).lengthBound) (h₁ : fuel₁ = (D.pair 1).lengthBound)
    (hcontrol : control = fuel₀ + fuel₁ + 1) (hn : 10000 ≤ n)
    (hl : ∀ j, (D.pair j).left.occurrences.card ≤ C)
    (hr : ∀ j, (D.pair j).right.occurrences.card ≤ C) (hC : C ≤ 2 ^ n)
    (hd₀ : Nat.clog 2 ({D with maskRestriction := P.semantic}.pair 0).leftArray.size ≤ n)
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationParentData, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.StoredRestriction