StableIntegerLedgerBudget

formal source

  19open scoped BigOperators
  20
  21/-- A stable ledger budget bounds all finite unresolved phase-cost sums. -/
  22structure StableIntegerLedgerBudget (n : ℕ) (costOf : ℕ → ℝ) where
  23  budget : ℝ
  24  budget_nonneg : 0 ≤ budget
  25  bounds_all_finite_failures :
  26    ∀ S : Finset ℕ, cumulativeFailureCost n costOf S ≤ budget
  27
  28/-- A stable budget rules out unbounded unresolved finite-phase cost. -/
  29theorem no_unbounded_unresolved_phase_cost
  30    {n : ℕ} {costOf : ℕ → ℝ}
  31    (stable : StableIntegerLedgerBudget n costOf) :
  32    ¬ (∀ B : ℝ, ∃ S : Finset ℕ, B < cumulativeFailureCost n costOf S) := by
  33  intro hunbounded
  34  rcases hunbounded stable.budget with ⟨S, hS⟩
  35  exact not_lt_of_ge (stable.bounds_all_finite_failures S) hS
  36
  37/-- A uniform positive floor for failed gates in a finite set. -/
  38def UniformFailureFloor (n : ℕ) (costOf : ℕ → ℝ) (S : Finset ℕ) (δ : ℝ) : Prop :=
  39  0 < δ ∧
  40  (∀ c ∈ S, GateFails n c) ∧
  41  (∀ c ∈ S, δ ≤ costOf c)
  42
  43/-- If all gates in `S` fail with a uniform floor `δ`, the stable budget bounds
  44the size of `S`. -/
  45theorem failed_gate_count_bounded_by_budget
  46    {n : ℕ} {costOf : ℕ → ℝ} {S : Finset ℕ} {δ : ℝ}
  47    (stable : StableIntegerLedgerBudget n costOf)
  48    (floor : UniformFailureFloor n costOf S δ) :
  49    δ * (S.card : ℝ) ≤ stable.budget := by
  50  have hlower :=
  51    phase_failure_cost_lower_bound
  52      (n := n) (S := S) (costOf := costOf) (δ := δ)