BudgetedScheduleAccount.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

All-outcome work bounds for the concrete residue schedule

theorem OAI.LowSpaceSubsetSum.BudgetedSchedule.account line 15
theorem OAI.LowSpaceSubsetSum.RepresentationData.zeroSetup_inputScale_le line 40

theorem OAI.LowSpaceSubsetSum.RepresentationData.schedule_account line 48

Source documentation

The capacity checks follow from the input guard on every history, not from a successful representation or a favorable resource event.

theorem schedule_account (h : D.zeroSetup.PrimeHistory) (r : D.zeroSetup.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hscale : Real.logb 2 (inputScale D.input : ℝ) ≤ (n : ℝ) / 1000000000)
    (q : ℕ) (hq : 0 < q) (F : IndexedMask n) (hF : F.semantic = h.1.1.1.2)
    (blocks : List (StoredSeparatorCheck.Block n (2 * RepresentationSetup.blockHalf n 0)))
    (budget : ℕ) :
    BudgetedSeparatorFlow.Account budget
      (BudgetedSchedule.run (D.scheduleData h r hn hlog q hq) F hF
        (representationBufferCapacity n) blocks
        (D.scheduleData h r hn hlog q hq).target budget) := by
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block, OAI.LowSpaceSubsetSum.RepresentationSetup.blockHalf, OAI.LowSpaceSubsetSum.BudgetedSeparatorFlow.Account, OAI.LowSpaceSubsetSum.BudgetedSchedule.run, OAI.LowSpaceSubsetSum.representationBufferCapacity