FaultToleranceThreshold

formal source

  88
  89/-- The fault tolerance threshold: below this defect density,
  90    errors can be corrected faster than they accumulate. -/
  91structure FaultToleranceThreshold where
  92  /-- The threshold value -/
  93  threshold : ℝ
  94  /-- The threshold is positive -/
  95  threshold_pos : 0 < threshold
  96
  97/-- A system is fault-tolerant if defect accumulation is bounded. -/
  98def is_fault_tolerant (sys : RecognitionSystem) (X : Ω → ℝ)
  99    (ft : FaultToleranceThreshold) : Prop :=
 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. -/
 110noncomputable def code_distance (X : Ω → ℝ) : ℝ :=
 111  ⨅ ω : { ω : Ω // Jcost (X ω) > 0 }, Jcost (X ω.val)
 112
 113/-- The φ-code distance: minimum cost at a φ-ladder step.
 114    d_φ = J(φ) = (√5 - 2)/2 ≈ 0.118 -/
 115noncomputable def phi_code_distance : ℝ :=
 116  Jcost Foundation.PhiForcing.φ
 117
 118/-- The φ-code distance is positive. -/
 119theorem phi_code_distance_pos : 0 < phi_code_distance := by
 120  unfold phi_code_distance
 121  apply Jcost_pos_of_ne_one