OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationScheduleLedger.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Full-residue representation setup, reports, copies and controls

These counters follow the concrete parent joins and all their overflowing prefixes. Clearing a task's workspace is included in the capacity-times-task term. Conversion from these units to machine operations is separate.

  1. def OAI.LowSpaceSubsetSum.RepresentationScheduleData.taskCount line 25
  2. def OAI.LowSpaceSubsetSum.RepresentationScheduleData.matchingCount line 29
  3. def OAI.LowSpaceSubsetSum.RepresentationScheduleData.joinLedger line 33
  4. theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.joinLedger_queries line 43
  5. theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.joinLedger_bounds line 46
  6. def OAI.LowSpaceSubsetSum.RepresentationScheduleData.setupUnits line 63
  7. def OAI.LowSpaceSubsetSum.RepresentationScheduleData.coreUnits line 65
  8. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_matchingCount_resource line 78
  9. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrime_times_capacity_half line 111
  10. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_setupUnits_resource line 130
  11. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_coreUnits_half line 171

    Source documentation

    A favorable resource/scan history has enough slack for every charged setup, callback, snapshot and control unit in the full residue schedule.

    theorem schedule_coreUnits_half (B : ℕ)
    (families : Fin 4 → Array (Finset (Fin (2 * blockHalf n 0))))
    (hgood : R.AllocatedResourceGood hn hlog ⟨h, r⟩)
    (hspread : mixerSpreadTest (R.signedWeights h.1.1.1) (R.orderedMixers h.1.1.1) n)
    (hprime : q ∈ primeRange (R.extraPrimeParameter h.1.1.1))
    (hscan : (R.scheduleData h r (by omega) hlog q hq).scanCount B families ≤
      inputScale R.input ^ 328 * 2 ^ ((n + 1) / 2)) :
    ((R.scheduleData h r (by omega) hlog q hq).coreUnits B families : ℝ) ≤
      (inputScale R.input : ℝ) ^ 410 * (2 : ℝ) ^ ((n + 1) / 2) := by
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.blockHalf, OAI.LowSpaceSubsetSum.mixerSpreadTest, OAI.LowSpaceSubsetSum.primeRange, OAI.LowSpaceSubsetSum.inputScale