RepresentationChosenCollector.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Chosen entries in the completed arrays on the actual prefix path

theorem OAI.LowSpaceSubsetSum.MaskRestriction.mem_follow_ones line 16
theorem OAI.LowSpaceSubsetSum.MaskRestriction.mem_follow_zeros line 29
theorem OAI.LowSpaceSubsetSum.MaskRestriction.follow_compatible_eq line 44
Source documentation
After all domain coordinates have been forced, a compatible mask is exactly the mask defining the path. Repeated coordinates cause no problem.
```
theorem follow_compatible_eq (P : MaskRestriction n) (order : List (Fin n))
    (A S T : Finset (Fin n)) (hcover : ∀ i ∈ A, i ∈ order)
    (hS : S ⊆ A) (hT : T ⊆ A) (hc : (P.follow order S).Compatible A T) : T = S := by
…
```
Mentions: OAI.LowSpaceSubsetSum.MaskRestriction, OAI.LowSpaceSubsetSum.MaskRestriction.Compatible
theorem OAI.LowSpaceSubsetSum.MaskRestriction.follow_compatible line 57
Source documentation
Following the membership bits of a mask preserves its compatibility.
```
theorem follow_compatible (P : MaskRestriction n) (order : List (Fin n))
    (A S : Finset (Fin n)) (hP : P.Compatible A S) :
    (P.follow order S).Compatible A S := by
…
```
Mentions: OAI.LowSpaceSubsetSum.MaskRestriction, OAI.LowSpaceSubsetSum.MaskRestriction.Compatible
def OAI.LowSpaceSubsetSum.RepresentationSetup.chosenEntry line 71
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenEntry_mask_subset line 76

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenEntry_mem_completed line 85

Source documentation

Completion, rather than any unproved universe-cardinality estimate, suffices for exact membership at an intermediate compatible prefix.

theorem chosenEntry_mem_completed (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) (P : ℤ) (hP : 0 < P) (B : ℕ) (restriction : MaskRestriction n)
    (hcompat : restriction.Compatible (R.orderedMixers h.1.1.1 0)
      (R.chosenEntry h r hn hlog j).mask)
    (hc : ((R.chosenParentData h r hn hlog j P hP (compressionDictionaryCapacity n)
      restriction).collect B).state.user.keys.overflow = false) :
    R.chosenEntry h r hn hlog j ∈ ((R.chosenParentData h r hn hlog j P hP
      (compressionDictionaryCapacity n) restriction).entries B).toList := by
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.MaskRestriction, OAI.LowSpaceSubsetSum.compressionDictionaryCapacity, OAI.collect

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenRight_full_follow_fits line 107

Source documentation

The fully forced right task emits only the designated full mask, so its capacity is bounded by the actual full-mask bucket from the extra-prime lemma.

theorem chosenRight_full_follow_fits (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 : ℕ)
    (order : List (Fin n)) (hcover : ∀ i ∈ R.orderedMixers h.1.1.1 0, i ∈ order)
    (hcap : ((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) :
    ((R.chosenParentData h r hn hlog 1 ((prefixModulus h.2.val 0 : ℤ) * q) hP
      (compressionDictionaryCapacity n)
      (MaskRestriction.empty.follow order (R.chosenEntry h r hn hlog 1).mask)).collect B).state.user.keys.overflow = false := by
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.prefixModulus, OAI.LowSpaceSubsetSum.compressionDictionaryCapacity, OAI.collect