BudgetedParentJoin.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Concrete parent collection under a prepaid watchdog

All six per-operation charges are fixed from the input scale. The executable never evaluates a reference run or its ledger to decide whether to continue.

def OAI.LowSpaceSubsetSum.BudgetedParentJoin.run line 18
theorem OAI.LowSpaceSubsetSum.BudgetedParentJoin.charge_bound line 31

theorem OAI.LowSpaceSubsetSum.BudgetedParentJoin.run_work line 45

Source documentation

Every outcome, including interrupted ties, is covered by the input budget.

theorem run_work (I : Instance n) (F : IndexedMask n) (P t : ℤ) (C B : ℕ)
    (right₁ right₂ : Array (LeafRecord n)) {d₁ d₂ : ℕ}
    (fuel₁ fuel₂ control : ℕ) (s₁ : State I F P .direct right₁ d₁)
    (s₂ : State I F P (.complementary t) right₂ d₂) (budget : ℕ)
    (hn : 10000 ≤ n) (hd₁ : d₁ ≤ n) (hd₂ : d₂ ≤ n)
    (hcopy : (12 * n + 32) * 2 ^ (d₂ + 1) ≤ B) :
    (run I F P t C B right₁ right₂ fuel₁ fuel₂ control s₁ s₂ budget).2 ≤ budget + 1 := by
…

Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.LeafRecord, OAI.LowSpaceSubsetSum.BudgetedParentJoin.run

theorem OAI.LowSpaceSubsetSum.BudgetedParentJoin.run_value line 76

theorem OAI.LowSpaceSubsetSum.BudgetedParentJoin.run_complete line 88

Source documentation

The favorable-run bound pays for this real execution, without traversing unused fuel.

theorem run_complete (I : Instance n) (F : IndexedMask n) (P t : ℤ) (C B : ℕ)
    (right₁ right₂ : Array (LeafRecord n)) {d₁ d₂ : ℕ}
    (fuel₁ fuel₂ control : ℕ) (s₁ : State I F P .direct right₁ d₁)
    (s₂ : State I F P (.complementary t) right₂ d₂) (budget : ℕ) (hn : 10000 ≤ n)
    (hb : let out := (CountedParentJoin.run I F P t C B right₁ right₂ fuel₁ fuel₂ control s₁ s₂).1
…

Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.LeafRecord, OAI.LowSpaceSubsetSum.CountedParentJoin.run