is_complete_correction

formal source

  81
  82/-- A correction protocol is complete if it maps all states to ground states
  83    within a finite number of applications. -/
  84def is_complete_correction {X : Ω → ℝ} (C : CorrectionProtocol X) : Prop :=
  85  ∀ ω, ∃ n : ℕ, Jcost (X (C.correct^[n] ω)) = 0
  86
  87/-! ## Fault Tolerance Threshold -/
  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 -/