CountedParentJoin.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Concrete stored-mask parent join

The readers, modular keys, validity tests, signed sums, dictionary encoding and mutable snapshots below execute their counted implementations. The bound uses the counters of that same stopped run, including invalid reported tuples.

abbrev OAI.LowSpaceSubsetSum.CountedParentJoin.Child line 17
def OAI.LowSpaceSubsetSum.CountedParentJoin.cells line 19
theorem OAI.LowSpaceSubsetSum.CountedParentJoin.cells_le line 23
abbrev OAI.LowSpaceSubsetSum.CountedParentJoin.State line 33
def OAI.LowSpaceSubsetSum.CountedParentJoin.snapshot line 39
Source documentation
Deep-copy the mutable tournament; the immutable right array is shared.
```
def snapshot (I : Instance n) (F : IndexedMask n) (P : ℤ)
    (mode : FilteredStream.Mode) (right : Array (LeafRecord n)) {d : ℕ}
    (s : State I F P mode right d) : State I F P mode right d × ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.FilteredStream.Mode, OAI.LowSpaceSubsetSum.LeafRecord, OAI.LowSpaceSubsetSum.CountedParentJoin.State
theorem OAI.LowSpaceSubsetSum.CountedParentJoin.snapshot_value line 46
theorem OAI.LowSpaceSubsetSum.CountedParentJoin.snapshot_work line 52
theorem OAI.LowSpaceSubsetSum.CountedParentJoin.report_polynomial line 60
theorem OAI.LowSpaceSubsetSum.CountedParentJoin.report_work line 72
def OAI.LowSpaceSubsetSum.CountedParentJoin.run line 85
theorem OAI.LowSpaceSubsetSum.CountedParentJoin.query_polynomial line 96

theorem OAI.LowSpaceSubsetSum.CountedParentJoin.run_work line 111

Source documentation

Work is charged to the actual query/report/snapshot counters, on every run, without a successful sampling or valid-record hypothesis.

theorem run_work (I : Instance n) (F : IndexedMask n) (P t : ℤ) (C B : ℕ)
    (right₁ right₂ : Array (LeafRecord n)) {d₁ d₂ : ℕ}
    (fuel₁ fuel₂ control : ℕ) (s₁ : State I F P .direct right₁ d₁)
    (s₂ : State I F P (.complementary t) right₂ d₂)
    (hn : 10000 ≤ n) (hd₁ : d₁ ≤ n) (hd₂ : d₂ ≤ n)
    (hcopy : (12 * n + 32) * 2 ^ (d₂ + 1) ≤ B) :
    let out := run I F P t C B right₁ right₂ fuel₁ fuel₂ control s₁ s₂
…

Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.LeafRecord, OAI.LowSpaceSubsetSum.CountedParentJoin.State, OAI.LowSpaceSubsetSum.CountedParentJoin.run