Observable

formal source

  81
  82/-! ## Part 1: Observable Extraction = Recognition -/
  83
  84structure Observable (S : Type) where
  85  value : S → ℝ
  86
  87structure ObservableExtractionMechanism (S : Type) where
  88  extract : S → ℝ
  89  nonconstant : ∃ s₁ s₂ : S, extract s₁ ≠ extract s₂
  90
  91structure RecognitionStructure (S : Type) where
  92  recognizes : S → S → Prop
  93  self_recognition : ∀ s, recognizes s s
  94  symmetric : ∀ s₁ s₂, recognizes s₁ s₂ → recognizes s₂ s₁
  95
  96def recognition_from_extraction {S : Type} (M : ObservableExtractionMechanism S) :
  97    RecognitionStructure S := {
  98  recognizes := fun s₁ s₂ => M.extract s₁ = M.extract s₂
  99  self_recognition := fun _ => rfl
 100  symmetric := fun _ _ h => h.symm
 101}
 102
 103/-- Recognition is unique extraction mechanism. -/
 104theorem recognition_unique {S : Type} (M : ObservableExtractionMechanism S) :
 105    ∃ R : RecognitionStructure S,
 106    (∀ s₁ s₂, M.extract s₁ = M.extract s₂ ↔ R.recognizes s₁ s₂) :=
 107  ⟨recognition_from_extraction M, fun _ _ => Iff.rfl⟩
 108
 109/-! ## Part 2: Cost Minima = Recognition -/
 110
 111structure Configuration where
 112  value : ℝ
 113  pos : 0 < value
 114