CorrectionProtocol

formal source

  67/-! ## Correction Dynamics -/
  68
  69/-- An error correction protocol is a map that reduces defects. -/
  70structure CorrectionProtocol (X : Ω → ℝ) where
  71  /-- The correction map -/
  72  correct : Ω → Ω
  73  /-- Correction reduces or preserves cost -/
  74  cost_decreasing : ∀ ω, Jcost (X (correct ω)) ≤ Jcost (X ω)
  75  /-- Ground states are fixed points -/
  76  ground_fixed : ∀ ω, Jcost (X ω) = 0 → correct ω = ω
  77
  78/-- The 8-tick correction cycle.
  79    After 8 ticks, the system has had a full opportunity to correct errors. -/
  80def eight_tick_cycle : ℕ := 8
  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 Ω),