pith. machine review for the scientific record. sign in
theorem proved term proof

phase_failure_accumulates_packaged

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  56theorem phase_failure_accumulates_packaged
  57    {n : ℕ} {S : Finset ℕ} {failure : ∀ c : ℕ, GateFailureCost n c}
  58    (hS : S.Nonempty)
  59    (hfails : ∀ c ∈ S, GateFails n c) :
  60    0 < cumulativeFailureCost n (fun c => (failure c).cost) S := by

proof body

Term-mode proof.

  61  apply phase_failure_accumulates hS hfails
  62  intro c hc
  63  exact (failure c).positive_of_failure (hfails c hc)
  64
  65end PhaseFailureCost
  66end NumberTheory
  67end IndisputableMonolith

depends on (7)

Lean names referenced from this declaration's body.