RepresentationReaderWork.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

Counted primitive structure operations of the representation reader

Replacement follows a single root-to-leaf path. Copying a snapshot instead visits every mutable tree node. The immutable occurrence arrays are shared. Counters below distinguish structural work from the cost of evaluating an arbitrary supplied key; concrete indexed-mask key evaluation is charged by the caller.

def OAI.LowSpaceSubsetSum.Tournament.countedReplace line 22

Source documentation

Rebuild one path, counting touched nodes.

def countedReplace (key : α → ℤ) : {d : ℕ} → Tree α d →
    (Fin d → Bool) → Option α → Tree α d × ℕ
  | 0, .leaf _, _, v => (.leaf v, 1)
  | _d + 1, .node _ l r, path, v =>
    if path 0 then
      let s := countedReplace key r (fun i => path i.succ) v
…

Mentions: OAI.LowSpaceSubsetSum.Tournament.Tree, OAI.LowSpaceSubsetSum.Tournament.node

theorem OAI.LowSpaceSubsetSum.Tournament.countedReplace_value line 33
theorem OAI.LowSpaceSubsetSum.Tournament.countedReplace_nodes line 42
def OAI.LowSpaceSubsetSum.Tournament.countedCopy line 52
Source documentation
A full snapshot copy, charged by the size of one node record.
```
def countedCopy (recordCells : ℕ) : {d : ℕ} → Tree α d → Tree α d × ℕ
  | 0, .leaf v => (.leaf v, recordCells)
  | _d + 1, .node w l r =>
    let a := countedCopy recordCells l
…
```
Mentions: OAI.LowSpaceSubsetSum.Tournament.Tree, OAI.LowSpaceSubsetSum.Tournament.node
theorem OAI.LowSpaceSubsetSum.Tournament.countedCopy_value line 59
theorem OAI.LowSpaceSubsetSum.Tournament.countedCopy_cells line 65
def OAI.LowSpaceSubsetSum.SliceCursor.countedNext line 81
Source documentation
The three reader branches use no traversal of the backing array. The nonempty branch performs one indexed load and one cyclic cursor update.
```
def countedNext (xs : Array α) (s : State xs.size) :
    Option (α × State xs.size) × ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.SliceCursor.State
theorem OAI.LowSpaceSubsetSum.SliceCursor.countedNext_value line 91
theorem OAI.LowSpaceSubsetSum.SliceCursor.countedNext_work line 97
def OAI.LowSpaceSubsetSum.PairCursor.countedNext line 110
theorem OAI.LowSpaceSubsetSum.PairCursor.countedNext_value line 115
theorem OAI.LowSpaceSubsetSum.PairCursor.countedNext_work line 119
def OAI.LowSpaceSubsetSum.FilteredStream.countedRead line 131
theorem OAI.LowSpaceSubsetSum.FilteredStream.countedRead_value line 138
theorem OAI.LowSpaceSubsetSum.FilteredStream.countedRead_work line 142
def OAI.LowSpaceSubsetSum.RowMerge.countedAdvance line 160
Source documentation
The same winning-row advance, with one counted row call and a counted root path replacement. Eight units per visited node cover field access, path tests, rebuilding and a cached comparison; key evaluation is separate.
```
def countedAdvance (key : α → ℤ) (read : σ → Option (α × σ) × ℕ)
    (t : Tournament.Tree (Front d α σ) d) :
    Option (α × Tournament.Tree (Front d α σ) d) × ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.Tournament.Tree, OAI.LowSpaceSubsetSum.RowMerge.Front
theorem OAI.LowSpaceSubsetSum.RowMerge.countedAdvance_value line 171
theorem OAI.LowSpaceSubsetSum.RowMerge.countedAdvance_work line 180
def OAI.LowSpaceSubsetSum.MergedReader.countedNext line 197
theorem OAI.LowSpaceSubsetSum.MergedReader.countedNext_value line 211
theorem OAI.LowSpaceSubsetSum.MergedReader.countedNext_work line 226
def OAI.LowSpaceSubsetSum.RepresentationPairData.countedRead line 242
theorem OAI.LowSpaceSubsetSum.RepresentationPairData.countedRead_value line 250
theorem OAI.LowSpaceSubsetSum.RepresentationPairData.countedRead_work line 253
def OAI.LowSpaceSubsetSum.RepresentationPairData.countedSnapshot line 267
Source documentation
Deep-copy the mutable reader tree while retaining the immutable array parameters. The extra record allowance in snapshotCells covers the root.
```
def countedSnapshot (s : D.State) : D.State × ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.RepresentationPairData.countedSnapshot_value line 272
theorem OAI.LowSpaceSubsetSum.RepresentationPairData.countedSnapshot_cells line 276