defect_energy

formal source

  42  is_defect : Jcost (X state) > 0
  43
  44/-- The defect energy is the J-cost. -/
  45noncomputable def defect_energy {X : Ω → ℝ} (d : RecognitionDefect X) : ℝ :=
  46  Jcost (X d.state)
  47
  48/-- Defect energy is positive by definition. -/
  49theorem defect_energy_pos {X : Ω → ℝ} (d : RecognitionDefect X) :
  50    0 < defect_energy d := d.is_defect
  51
  52/-! ## Error Syndromes -/
  53
  54/-- An error syndrome is a function that detects defects.
  55    syndrome(ω) = 0 iff ω is a ground state (J = 0). -/
  56structure ErrorSyndrome (X : Ω → ℝ) where
  57  /-- The syndrome function -/
  58  syndrome : Ω → ℝ
  59  /-- Zero syndrome iff zero cost -/
  60  zero_iff_ground : ∀ ω, syndrome ω = 0 ↔ Jcost (X ω) = 0
  61
  62/-- The natural syndrome for RS: the J-cost itself. -/
  63noncomputable def jcost_syndrome (X : Ω → ℝ) : ErrorSyndrome X where
  64  syndrome := fun ω => Jcost (X ω)
  65  zero_iff_ground := fun ω => Iff.rfl
  66
  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 -/