CompressionSurvival.lean`

60 declarations, 0 contain sorry, 0 declared as axioms

The compressed-block trial's actual solution bucket

The seven compacted blocks and three raw domains are consecutive intervals of one uniform permutation. The only subsequent random draw is a prime. The residue of the fixed solution is enumerated by the program, not sampled.

def OAI.LowSpaceSubsetSum.compressionHalfSize line 24
def OAI.LowSpaceSubsetSum.compressionRightRawSize line 25
def OAI.LowSpaceSubsetSum.compressionLeftRawSize line 26
def OAI.LowSpaceSubsetSum.compressionPrimeExponent line 27
def OAI.LowSpaceSubsetSum.compressionDictionaryCapacity line 28
def OAI.LowSpaceSubsetSum.indexInterval line 30
theorem OAI.LowSpaceSubsetSum.indexInterval_card line 33
def OAI.LowSpaceSubsetSum.compressionBlock line 52
def OAI.LowSpaceSubsetSum.compressionLeftRaw line 55
def OAI.LowSpaceSubsetSum.compressionRightRaw line 58
theorem OAI.LowSpaceSubsetSum.compressionHalfSize_eq line 64
theorem OAI.LowSpaceSubsetSum.compression_layout_feasible line 68
theorem OAI.LowSpaceSubsetSum.compressionBlock_card line 74
theorem OAI.LowSpaceSubsetSum.compressionLeftRaw_card line 81
theorem OAI.LowSpaceSubsetSum.compressionBlock_disjoint line 88
theorem OAI.LowSpaceSubsetSum.compressionBlock_leftRaw_disjoint line 105
def OAI.LowSpaceSubsetSum.compressionBaseLeft line 117
def OAI.LowSpaceSubsetSum.compressionBaseRight line 120
theorem OAI.LowSpaceSubsetSum.compressionBaseLeft_interval line 124
theorem OAI.LowSpaceSubsetSum.compressionBaseRight_intervals line 134
theorem OAI.LowSpaceSubsetSum.compressionBaseRight_complement line 146
theorem OAI.LowSpaceSubsetSum.compression_left_exponent line 160
theorem OAI.LowSpaceSubsetSum.compression_prime_floor line 188
theorem OAI.LowSpaceSubsetSum.compression_capacity_lower line 196
theorem OAI.LowSpaceSubsetSum.compression_bucket_loss_le_half line 206
structure OAI.LowSpaceSubsetSum.CompressionSetup line 250
def OAI.LowSpaceSubsetSum.CompressionSetup.weights line 259
def OAI.LowSpaceSubsetSum.CompressionSetup.block line 260
def OAI.LowSpaceSubsetSum.CompressionSetup.leftRaw line 262
def OAI.LowSpaceSubsetSum.CompressionSetup.leftDomain line 264
def OAI.LowSpaceSubsetSum.CompressionSetup.rightDomain line 266
def OAI.LowSpaceSubsetSum.CompressionSetup.rightRaw line 269
def OAI.LowSpaceSubsetSum.CompressionSetup.groupDomain line 273
Source documentation
The four rows in the compression table, with their actual index domains.
```
def groupDomain (e : Equiv.Perm (Fin n)) : Fin 4 → Finset (Fin n) :=
…
```
def OAI.LowSpaceSubsetSum.CompressionSetup.groupWeights line 278
theorem OAI.LowSpaceSubsetSum.CompressionSetup.leftDomain_eq_groups line 281
theorem OAI.LowSpaceSubsetSum.CompressionSetup.rightDomain_eq_groups line 286
def OAI.LowSpaceSubsetSum.CompressionSetup.blockWeights line 299
def OAI.LowSpaceSubsetSum.CompressionSetup.leftWeights line 301
def OAI.LowSpaceSubsetSum.CompressionSetup.rightWeights line 303
def OAI.LowSpaceSubsetSum.CompressionSetup.solutionLeft line 305
def OAI.LowSpaceSubsetSum.CompressionSetup.solutionRight line 306
def OAI.LowSpaceSubsetSum.CompressionSetup.leftWeight line 307
def OAI.LowSpaceSubsetSum.CompressionSetup.rightWeight line 308
def OAI.LowSpaceSubsetSum.CompressionSetup.Passing line 310
theorem OAI.LowSpaceSubsetSum.CompressionSetup.leftWeight_mem line 313
theorem OAI.LowSpaceSubsetSum.CompressionSetup.rightWeight_mem line 316
theorem OAI.LowSpaceSubsetSum.CompressionSetup.solution_split line 320
theorem OAI.LowSpaceSubsetSum.CompressionSetup.four_group_solution line 331
theorem OAI.LowSpaceSubsetSum.CompressionSetup.passing_probability line 352
theorem OAI.LowSpaceSubsetSum.CompressionSetup.leftWeights_card line 359
abbrev OAI.LowSpaceSubsetSum.CompressionSetup.PrimeSpace line 376
def OAI.LowSpaceSubsetSum.CompressionSetup.BucketFits line 378
theorem OAI.LowSpaceSubsetSum.CompressionSetup.leftWeights_magnitude line 382
theorem OAI.LowSpaceSubsetSum.CompressionSetup.bucketFits_probability line 389
abbrev OAI.LowSpaceSubsetSum.CompressionSetup.TrialHistory line 438
def OAI.LowSpaceSubsetSum.CompressionSetup.primeLaw line 440
def OAI.LowSpaceSubsetSum.CompressionSetup.trialLaw line 446
def OAI.LowSpaceSubsetSum.CompressionSetup.Successful line 450
theorem OAI.LowSpaceSubsetSum.CompressionSetup.successful_probability line 455
Source documentation
A passing partition has probability at least one half, and conditional on every such actual partition its fixed solution bucket fits with probability at least one half. No uniform residue guess appears in this experiment.
```
theorem successful_probability (hn : 168000000 ≤ n)
    (hmean : (153 / 20000 : ℝ) * n ≤
      meanDeficiency R.weights Finset.univ (compressionHalfSize n))
    (hlog : Real.logb 2 (inputScale R.input) ≤ (n : ℝ) / 1000000000) :
    (1 / 4 : ℝ) ≤ (R.trialLaw hn).probability R.Successful := by
…
```
Mentions: OAI.LowSpaceSubsetSum.meanDeficiency, OAI.LowSpaceSubsetSum.compressionHalfSize, OAI.LowSpaceSubsetSum.inputScale

theorem OAI.LowSpaceSubsetSum.CompressionSetup.designated_bucket_witness line 475

Source documentation

The loop scans this residue among all 0,…,q−1. Its dictionary is small enough and contains the fixed solution's left weight.

theorem designated_bucket_witness (e : Equiv.Perm (Fin n)) (q : PrimeSpace n)
    (hq : R.BucketFits e q) :
    ∃ z : Fin q.val, ∃ x : Fin 4 → ℤ,
      (∀ i, x i ∈ R.groupWeights e i) ∧
      x 0 + x 1 + (x 2 + x 3) = R.input.target ∧
      x 0 + x 1 ≡ (z.val : ℤ) [ZMOD (q.val : ℤ)] ∧
      x 2 + x 3 ≡ (R.input.target : ℤ) - z.val [ZMOD (q.val : ℤ)] ∧
      (R.leftWeights e |>.filter (fun w => w % (q.val : ℤ) = z.val)).card ≤
        compressionDictionaryCapacity n := by
…

Mentions: OAI.LowSpaceSubsetSum.CompressionSetup.PrimeSpace, OAI.LowSpaceSubsetSum.compressionDictionaryCapacity