RepresentationLifetime.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous representation workspace

The prefix control stack contains no collectors. During a right task the left dictionary is retained; separator recursion uses filtered buffers only after that task completes. The conservative bound below may even count the task and checker workspaces simultaneously. Separator table storage is shared throughout the trial.

theorem OAI.LowSpaceSubsetSum.SeparatorCheck.family_depth_le line 23
theorem OAI.LowSpaceSubsetSum.SeparatorCheck.blocks_depth_sum_le line 31

theorem OAI.LowSpaceSubsetSum.SeparatorCheck.run_peak_small line 44

Source documentation

The live separator buffers are bounded on all family outcomes.

theorem run_peak_small (n C : ℕ) (families : Fin 4 → Array (Finset (Fin g)))
    (target : ℤ) (xs ys : List (Record g)) (hg : g ≤ n)
    (hsize : xs.length + ys.length ≤ 2 * (C + 1))
    (hC : 2 * (C + 1) ≤ 2 ^ n)
    (hfamily : ∀ i, (families i).size ≤ 11 * 2 ^ g) :
    (run n families target xs ys).peak ≤ 100 * (n + 5) * (C + 1) := by
…

Mentions: OAI.LowSpaceSubsetSum.SeparatorCheck.Record, OAI.LowSpaceSubsetSum.SeparatorCheck.run

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.doubled_capacity_fits line 64
def OAI.LowSpaceSubsetSum.RepresentationSetup.separatorWorkingCells line 80
Source documentation
A cell count for every indexed bit of each live separator record, including a conservative node/header multiplier.
```
def separatorWorkingCells (h : R.PrimeHistory) (hn : 2200 ≤ n)
    (draws : R.SeparatorDraws h hn) (target : ℤ)
    (xs ys : List (SeparatorCheck.Record (2 * blockHalf n 0))) : ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.SeparatorCheck.Record, OAI.LowSpaceSubsetSum.RepresentationSetup.blockHalf
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.separatorWorkingCells_bound line 85
def OAI.LowSpaceSubsetSum.RepresentationSetup.liveCells line 121
Source documentation
All simultaneously allowed representation structures, with one retained left dictionary, one task arena and the scalar prefix continuation stack.
```
def liveCells (task tables checker stack : ℕ) : ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.liveCells_bound line 125