RepresentationPrefixWork.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Prefix work for the actual representation schedule

The bounds apply to every lifted residue and every prefix, without requiring a surviving solution. The check list is fixed before separator families are drawn, including all reuse of the retained left array.

theorem OAI.LowSpaceSubsetSum.RepresentationBucketData.checkInputSize_le line 22
theorem OAI.LowSpaceSubsetSum.RepresentationBucketData.checkList_arrays line 51

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_top_disjoint line 75

Source documentation

The four actual top blocks are disjoint at every task.

theorem schedule_top_disjoint (z : ℕ) (side : Fin 2) :
    ∀ i j, i ≠ j →
      Disjoint (((R.scheduleData h r hn hlog q hq).parentData side z).leaves i).top
        (((R.scheduleData h r hn hlog q hq).parentData side z).leaves j).top := by
…

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_topOrder_length line 82
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_topOrder_mem line 87
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_rawEntries_valid line 100
Source documentation
Any emitted entry comes from the actual valid four-leaf universe.
```
theorem schedule_rawEntries_valid (z : ℕ) (side : Fin 2) (P : MaskRestriction n)
    (e : Entry (Fin n))
    (he : e ∈ ({ (R.scheduleData h r hn hlog q hq).parentData side z with
      maskRestriction := P }).rawEntries) :
…
```
Mentions: OAI.LowSpaceSubsetSum.MaskRestriction, OAI.LowSpaceSubsetSum.Entry
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_rawEntries_bounded line 117
Source documentation
Fixed-width keys are injective on every actual prefix's emitted entries.
```
theorem schedule_rawEntries_bounded (z : ℕ) (side : Fin 2) (P : MaskRestriction n)
    (e : Entry (Fin n))
    (he : e ∈ ({ (R.scheduleData h r hn hlog q hq).parentData side z with
      maskRestriction := P }).rawEntries) :
…
```
Mentions: OAI.LowSpaceSubsetSum.MaskRestriction, OAI.LowSpaceSubsetSum.Entry

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_taskStarts_bound line 126

Source documentation

Every actual prefix task is charged to the distinct unrestricted bucket.

theorem schedule_taskStarts_bound (z : ℕ) (B : ℕ) (side : Fin 2) :
    compressionDictionaryCapacity n *
      ((R.scheduleData h r hn hlog q hq).parentData side z).taskStarts B
        (R.scheduleData h r hn hlog q hq).topOrder MaskRestriction.empty ≤
      compressionDictionaryCapacity n + 2 * (mixerSize n + 1) *
        ((R.scheduleData h r hn hlog q hq).parentData side z).entryUniverse.card := by
…

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

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_checkInputSize_bound line 142

Source documentation

The concrete check list accounts for the left array each time it is reused.

theorem schedule_checkInputSize_bound (z B : ℕ) :
    TopCoordinates.checkInputSize (((R.scheduleData h r hn hlog q hq).bucket z).checkList B) ≤
      ((R.scheduleData h r hn hlog q hq).parentData 0 z).entryUniverse.card +
        (2 * mixerSize n + 3) *
          ((R.scheduleData h r hn hlog q hq).parentData 1 z).entryUniverse.card := by
…

Mentions: OAI.LowSpaceSubsetSum.TopCoordinates.checkInputSize, OAI.LowSpaceSubsetSum.mixerSize

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_checkList_counts line 159

Source documentation

All actual completed checks have the local counts required by the rounded separator parameters, regardless of the visited prefix.

theorem schedule_checkList_counts (z B : ℕ) :
    ∀ p ∈ ((R.scheduleData h r hn hlog q hq).bucket z).checkList B,
      (∀ x ∈ p.1.toList, ∀ i,
        (SeparatorCheck.localMask i
          ((R.topCoordinates h.1.1.1 h.1.2).encodeEntry x).mask).card =
            (separatorParameters h.1.1.2 (by omega)).c i) ∧
      (∀ x ∈ p.2.toList, ∀ i,
        (SeparatorCheck.localMask i
          ((R.topCoordinates h.1.1.1 h.1.2).encodeEntry x).mask).card =
            (2 * blockHalf n 0) / 2 - (separatorParameters h.1.1.2 (by omega)).c i) := by
…

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

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_mean_totalScans line 182