OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationSnapshots.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Full mutable reader snapshots fit the replay buffer

Immutable leaf arrays are shared. A snapshot copies the tournament, its cached occurrences and cursor fields. This bound holds for every reader state, prefix and residue, independently of the resource event.

  1. theorem OAI.LowSpaceSubsetSum.guarded_power_rate line 17
  2. theorem OAI.LowSpaceSubsetSum.representationBufferCapacity_lower line 29
  3. def OAI.LowSpaceSubsetSum.RepresentationPairData.snapshotCells line 42
  4. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_snapshotCells_le_buffer line 50