CompressionTrial.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The compressed trial at its designated solution residue

Both joins below use the concrete shared-array modular streams. Fuel comes from products of stored-list lengths, so computing it does not enumerate a Cartesian product. The ideal experiment still uses the proved uniform permutation and prime law; bounded-sampler and watchdog losses are separate.

def OAI.LowSpaceSubsetSum.CompressionSetup.streamLength line 18
theorem OAI.LowSpaceSubsetSum.CompressionSetup.initial_output_length line 21
def OAI.LowSpaceSubsetSum.CompressionSetup.actualLeftDictionary line 27
theorem OAI.LowSpaceSubsetSum.CompressionSetup.actualLeftDictionary_fits line 37
def OAI.LowSpaceSubsetSum.CompressionSetup.actualRightHit line 57
theorem OAI.LowSpaceSubsetSum.CompressionSetup.actualRightHit_true line 67
def OAI.LowSpaceSubsetSum.CompressionSetup.executableCapExponent line 88
Source documentation
Integer division computes the rational floor used by the size test.
```
def executableCapExponent (n : ℕ) : ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.CompressionSetup.executableCapExponent_eq line 91
def OAI.LowSpaceSubsetSum.CompressionSetup.compactTests line 103
theorem OAI.LowSpaceSubsetSum.CompressionSetup.compactTests_iff line 107
def OAI.LowSpaceSubsetSum.CompressionSetup.residuePass line 113
Source documentation
One explicitly selected residue pass, using concrete streams and tries.
```
def residuePass (B : ℕ) (e : Equiv.Perm (Fin n)) (q : PrimeSpace n)
    (z : Fin q.val) : Bool :=
…
```
Mentions: OAI.LowSpaceSubsetSum.CompressionSetup.PrimeSpace
def OAI.LowSpaceSubsetSum.CompressionSetup.designatedPass line 121
Source documentation
The fixed solution chooses this residue only in the success analysis.
```
def designatedPass (B : ℕ) (e : Equiv.Perm (Fin n)) (q : PrimeSpace n) : Bool :=
…
```
Mentions: OAI.LowSpaceSubsetSum.CompressionSetup.PrimeSpace
theorem OAI.LowSpaceSubsetSum.CompressionSetup.designatedPass_true line 124
theorem OAI.LowSpaceSubsetSum.CompressionSetup.designatedPass_probability line 131

def OAI.LowSpaceSubsetSum.CompressionSetup.residueLoop line 142

Source documentation

Tail-recursive, constant-state enumeration of a consecutive residue range.

def residueLoop (test : ℕ → Bool) : ℕ → ℕ → Bool
  | 0, _ => false
  | fuel + 1, start => if test start then true else residueLoop test fuel (start + 1)

theorem OAI.LowSpaceSubsetSum.CompressionSetup.residueLoop_true_iff line 146
def OAI.LowSpaceSubsetSum.CompressionSetup.compressionTrial line 170
Source documentation
The actual compression trial scans every residue; it never uses the solution.
```
def compressionTrial (B : ℕ) (e : Equiv.Perm (Fin n)) (q : PrimeSpace n) : Bool :=
…
```
Mentions: OAI.LowSpaceSubsetSum.CompressionSetup.PrimeSpace
theorem OAI.LowSpaceSubsetSum.CompressionSetup.compressionTrial_true_iff line 174
theorem OAI.LowSpaceSubsetSum.CompressionSetup.compressionTrial_true line 184
theorem OAI.LowSpaceSubsetSum.CompressionSetup.compressionTrial_probability line 189