RepresentationBucketWitness.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The actual designated bucket accepts a covered surviving representation

theorem OAI.LowSpaceSubsetSum.representation_dictionary_pair_size line 13

theorem OAI.LowSpaceSubsetSum.RepresentationBucketData.check_finds_fixed_pair line 32

Source documentation

Checker completeness over opaque arrays. The stream implementation is not reduced while applying the separator's fixed-pair theorem.

theorem check_finds_fixed_pair {n g : ℕ} (D : RepresentationBucketData n g)
    (families : Fin 4 → Array (Finset (Fin g))) (left right : Array (Entry (Fin n)))
    (hsize : left.toList.length + right.toList.length ≤ 2 ^ n)
    (x y : Entry (Fin n)) (hx : x ∈ left.toList) (hy : y ∈ right.toList)
    (hw : x.value + y.value = D.target)
    (hc : SeparatorCheck.Covered families (D.coordinates.encodeEntry x)
      (D.coordinates.encodeEntry y)) : D.check families left right = true := by
…

Mentions: OAI.LowSpaceSubsetSum.RepresentationBucketData, OAI.LowSpaceSubsetSum.Entry, OAI.LowSpaceSubsetSum.SeparatorCheck.Covered

theorem OAI.LowSpaceSubsetSum.RepresentationBucketData.run_complete_of_pair line 44

Source documentation

Generic prefix completion keeps the implementation opaque while the application supplies its actual chosen records and capacity bounds.

theorem run_complete_of_pair {n g : ℕ} (D : RepresentationBucketData n g)
    (B : ℕ) (families : Fin 4 → Array (Finset (Fin g)))
    (domain : Finset (Fin n)) (x y : Entry (Fin n))
    (hleft : (D.left.collect B).state.user.keys.overflow = false)
    (hx : x ∈ (D.left.entries B).toList)
    (hfull : ({ D.right with maskRestriction :=
…

Mentions: OAI.LowSpaceSubsetSum.RepresentationBucketData, OAI.LowSpaceSubsetSum.Entry

def OAI.LowSpaceSubsetSum.RepresentationSetup.chosenBucketData line 86
Source documentation
This is one bucket visited by the real residue loop, with the designated normalized residue used only to name that iteration in the analysis.
```
def chosenBucketData (h : R.PrimeHistory) (r : R.Residues h.2) (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (q : ℕ) (hP : 0 < (prefixModulus h.2.val 0 : ℤ) * q) :
    RepresentationBucketData n (2 * blockHalf n 0) where
…
```
Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.prefixModulus, OAI.LowSpaceSubsetSum.RepresentationBucketData, OAI.LowSpaceSubsetSum.RepresentationSetup.blockHalf
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenBucketData_topOrder line 97
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenBucketData_right_restrict line 104

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenBucket_accepts line 114

Source documentation

The left collector and right prefix recursion both reach the covered chosen pair. Early completion of a right prefix is sufficient.

theorem chosenBucket_accepts (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hr : R.ResidueSuccess (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r)
    (q : ℕ) (hP : 0 < (prefixModulus h.2.val 0 : ℤ) * q) (B : ℕ)
    (families : Fin 4 → Array (Finset (Fin (2 * blockHalf n 0))))
    (hleft : (R.chosenParentBucket h r hn hlog 0 ((prefixModulus h.2.val 0 : ℤ) * q)).card ≤
      compressionDictionaryCapacity n)
    (hright : ((R.chosenParentBucket h r hn hlog 1 ((prefixModulus h.2.val 0 : ℤ) * q)).filter
      (fun e => e.mask = (R.chosenEntry h r hn hlog 1).mask)).card ≤
        compressionDictionaryCapacity n)
    (hcovered : SeparatorCheck.Covered families
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.prefixModulus, OAI.LowSpaceSubsetSum.RepresentationSetup.blockHalf, OAI.LowSpaceSubsetSum.compressionDictionaryCapacity, OAI.LowSpaceSubsetSum.SeparatorCheck.Covered

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenEntry_separator_count line 158

Source documentation

Every chosen exact key has the actual local cardinalities used by the rounded separator parameter constructor.

theorem chosenEntry_separator_count (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hr : R.ResidueSuccess (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r)
    (j : Fin 2) (i : Fin 4) :
    (SeparatorCheck.localMask i ((R.topCoordinates h.1.1.1 h.1.2).encodeEntry
      (R.chosenEntry h r hn hlog j)).mask).card =
      if j = 0 then (separatorParameters h.1.1.2 (by omega)).c i
      else (2 * blockHalf n 0) / 2 - (separatorParameters h.1.1.2 (by omega)).c i := by
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.SeparatorCheck.localMask, OAI.LowSpaceSubsetSum.RepresentationSetup.separatorParameters, OAI.LowSpaceSubsetSum.RepresentationSetup.blockHalf