RecognitionDefect

formal source

  35
  36/-- A recognition defect is a state with J > 0.
  37    The defect "energy" is the J-cost itself. -/
  38structure RecognitionDefect (X : Ω → ℝ) where
  39  /-- The state carrying the defect -/
  40  state : Ω
  41  /-- The state has positive cost (is a defect) -/
  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