pith. machine review for the scientific record. sign in
def definition def or abbrev

is_fault_tolerant

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)

  98def is_fault_tolerant (sys : RecognitionSystem) (X : Ω → ℝ)
  99    (ft : FaultToleranceThreshold) : Prop :=

proof body

Definition body.

 100  ∀ (p : ProbabilityDistribution Ω),
 101    expected_cost p.p X < ft.threshold →
 102    -- The system can be corrected back to near-equilibrium
 103    ∃ (C : CorrectionProtocol X),
 104      expected_cost (fun ω => p.p (C.correct ω)) X < expected_cost p.p X / 2
 105
 106/-! ## Code Distance and φ-Ladder -/
 107
 108/-- The code distance is the minimum cost of a non-trivial error.
 109    In RS, this is related to the φ-ladder structure. -/

depends on (19)

Lean names referenced from this declaration's body.