RepresentationTaskSpace.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Storage of the concrete parent-task data structures

The footprint counts indexed masks bit by bit, as well as array records, tournament nodes, the tie buffer, dictionary records and trie nodes. The bound includes these concrete structures; their simultaneous lifetimes and the prefix stack require a separate bound.

def OAI.LowSpaceSubsetSum.RepresentationPairData.footprint line 26
Source documentation
A conservative flat-cell accounting for the two raw-leaf arrays and the mutable tournament, including its cached indexed occurrence and cursor.
```
def footprint (s : D.State) : ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.RepresentationPairData.footprint_le line 29
def OAI.LowSpaceSubsetSum.RepresentationParentData.footprint line 44
Source documentation
Two current readers, two replay snapshots, and a mutable tie buffer; dictionary masks and trie links are accounted for separately.
```
def footprint (B : ℕ) : ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.RepresentationParentData.footprint_le line 49
def OAI.LowSpaceSubsetSum.representationBufferCapacity line 73
Source documentation
The mutable tie buffer chosen by the manuscript.
```
def representationBufferCapacity (n : ℕ) : ℕ := 2 ^ (19 * n / 100)
```
theorem OAI.LowSpaceSubsetSum.representationBufferCapacity_le line 75
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.main_leaf_rate_le_capacity line 84

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_pair_capacity line 94

Source documentation

The array capacity is valid for every residue and prefix, on every outcome. In particular no resource or successful-solution event is assumed.

theorem schedule_pair_capacity (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hscale : Real.logb 2 (inputScale R.input : ℝ) ≤ (n : ℝ) / 1000000000)
    (q : ℕ) (hq : 0 < q) (z : ℕ) (side : Fin 2) (P : MaskRestriction n) (child : Fin 2) :
    let D := ({ (R.scheduleData h r hn hlog q hq).parentData side z with maskRestriction := P }).pair child
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.MaskRestriction

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_task_footprint line 107