RepresentationScheduleUniverse.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Distinct-entry accounting over the lifted residue loop

Every prefix bucket lies in the actual low-residue entry universe. Different loop counters have disjoint full-residue buckets, so their total distinct entry count is bounded by one low-residue universe, without a factor q.

def OAI.LowSpaceSubsetSum.RepresentationScheduleData.lowEntryUniverse line 22
theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.leftResidue_low line 28
theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.parentResidue_low line 32
theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.entryUniverse_subset_low line 44
Source documentation
The actual raw emitted key is in the low-residue envelope, including when its task has a nonempty prefix restriction.
```
theorem entryUniverse_subset_low (side : Fin 2) (z : ℕ) (P : MaskRestriction n) :
    ({ D.parentData side z with maskRestriction := P }).entryUniverse ⊆
…
```
Mentions: OAI.LowSpaceSubsetSum.MaskRestriction
theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.leftResidue_range line 68
theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.parentResidue_injective line 82
Source documentation
Distinct counters specify distinct parent residues on either side.
```
theorem parentResidue_injective (side : Fin 2) :
    Function.Injective (fun z : Fin D.q =>
      (D.parentData side z.val).parentResidue % D.modulus) := by
…
```
theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.parentUniverses_disjoint line 104
theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.sum_parentUniverse_card line 116
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_lowEntryUniverse_card line 139

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_taskStarts_sum_bound line 170

Source documentation

Over the entire residue loop the prefix account uses one low-entry universe, rather than charging it once per extra-prime residue.

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

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

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_checkInputSize_sum_bound line 191

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_lowEntryUniverse_resource line 214

Source documentation

The resource event was sampled before the extra prime and bounds every full-loop universe, without assuming that the representation survives.

theorem schedule_lowEntryUniverse_resource (hlarge : 20000 ≤ n)
    (hgood : R.AllocatedResourceGood hlarge hlog ⟨h, r⟩) (side : Fin 2) :
    (((R.scheduleData h r hn hlog q hq).lowEntryUniverse side).card : ℝ) ≤
      (inputScale R.input : ℝ) ^ 200 * (2 : ℝ) ^ R.resourceLambda h.1.1.1 h.1.1.2 := by
…

Mentions: OAI.LowSpaceSubsetSum.inputScale

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_mean_allScans line 223