CompressionTrialLedger.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

A complete compression-join ledger and its live data structures

The counters retain the actual compact-test and overflow branches. The storage bound describes the arrays, current cursors, replay snapshots, tie buffer and bounded trie.

structure OAI.LowSpaceSubsetSum.CompressionLedger line 18
def OAI.LowSpaceSubsetSum.CompressionData.residueLedger line 30
Source documentation
No right-hand work is counted after dictionary overflow. The control count includes even the unused fuel suffix of the original run loop.
```
def residueLedger (B : ℕ) (e : Equiv.Perm (Fin n)) (q : CompressionSetup.PrimeSpace n)
    (z : Fin q.val) : CompressionLedger :=
…
```
Mentions: OAI.LowSpaceSubsetSum.CompressionSetup.PrimeSpace, OAI.LowSpaceSubsetSum.CompressionLedger
def OAI.LowSpaceSubsetSum.CompressionData.trialLedger line 44
theorem OAI.LowSpaceSubsetSum.CompressionData.residueLedger_queries line 51
theorem OAI.LowSpaceSubsetSum.CompressionData.residueLedger_bounds line 59
theorem OAI.LowSpaceSubsetSum.CompressionData.trialLedger_reports_copies line 77

theorem OAI.LowSpaceSubsetSum.CompressionData.trialLedger_half_exponential line 100

Source documentation

A compact bound for all measured join activity in one compression trial. Copy work is measured in units of a full B-word snapshot.

theorem trialLedger_half_exponential (B : ℕ) (e : Equiv.Perm (Fin n))
    (q : CompressionSetup.PrimeSpace n) (hn : 2000 ≤ n) :
    ((D.trialLedger B e q).queries : ℝ) ≤ 30 * (2 : ℝ) ^ ((n : ℝ) / 2) ∧
    ((D.trialLedger B e q).reports : ℝ) ≤ 2 * (2 : ℝ) ^ ((n : ℝ) / 2) ∧
    (B * (D.trialLedger B e q).copies : ℕ) ≤ 4 * (2 : ℝ) ^ ((n : ℝ) / 2) ∧
    ((D.trialLedger B e q).controls : ℝ) ≤ 6 * (2 : ℝ) ^ ((n : ℝ) / 2) := by
…

Mentions: OAI.LowSpaceSubsetSum.CompressionSetup.PrimeSpace

def OAI.LowSpaceSubsetSum.CompressionData.snapshotCells line 148
Source documentation
Only the mutable tournament and its cached cursors are copied. The immutable stored arrays are shared by every replay snapshot.
```
def snapshotCells (e : Equiv.Perm (Fin n)) (q : CompressionSetup.PrimeSpace n)
    (i : Fin 4) (mode : FilteredStream.Mode) (s : D.GroupState e q i mode) : ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.CompressionSetup.PrimeSpace, OAI.LowSpaceSubsetSum.FilteredStream.Mode
theorem OAI.LowSpaceSubsetSum.CompressionData.snapshotCells_le_buffer line 152
def OAI.LowSpaceSubsetSum.CompressionData.storageCells line 180
Source documentation
A conservative simultaneous footprint, including the preliminary single-block enumeration and three copies of every group state.
```
def storageCells (B : ℕ) (e : Equiv.Perm (Fin n)) (q : CompressionSetup.PrimeSpace n)
    (z : Fin q.val) (fuel : ℕ) (mode : Fin 4 → FilteredStream.Mode)
    (states : ∀ i, D.GroupState e q i (mode i)) : ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.CompressionSetup.PrimeSpace, OAI.LowSpaceSubsetSum.FilteredStream.Mode
theorem OAI.LowSpaceSubsetSum.CompressionData.storageCells_bound line 187