OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationLeafSpace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.leftArray_size_le line 15
2. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.rightArray_size_le line 19
3. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.storedRight_size_le line 23
4. theorem OAI.LowSpaceSubsetSum.RepresentationPairData.reader_comparisons_le line 27
5. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_main_card line 42

   Source documentation

   The main guard absorbs the allocation's polynomial factor with strict slack below both the tie-buffer and dictionary rates. No survival or resource event is used.

   theorem rawLeaf_main_card (z : Layout n) (g : Guesses n) (f : R.Partitions z)
       (hn : 10000 ≤ n)
       (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
       (hscale : Real.logb 2 (inputScale R.input : ℝ) ≤ (n : ℝ) / 1000000000)
       (j : Fin 2) (i : Fin 4) :
       ((R.rawLeaf z g f (R.allocatedBackground z g hn hlog) j i).occurrences.card : ℝ) ≤
         (2 : ℝ) ^ ((37 / 200 : ℝ) * n) := by
   …

   Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses, OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.inputScale

6. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_pair_storage line 73

   Source documentation

   Every prefix and every full-residue counter uses leaf arrays and a tournament bounded by the same raw-leaf size, even on failed trials.

   theorem schedule_pair_storage (h : R.PrimeHistory) (r : R.Residues h.2)
       (hn : 10000 ≤ n)
       (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
       (hscale : Real.logb 2 (inputScale R.input : ℝ) ≤ (n : ℝ) / 1000000000)
       (q : ℕ) (hq : 0 < q) (z : ℕ) (side : Fin 2) (P : MaskRestriction n) (child : Fin 2) :
       let D := ({ (R.scheduleData h r hn hlog q hq).parentData side z with maskRestriction := P }).pair child
   …

   Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.MaskRestriction

7. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_pair_index_bits line 100