theorem
proved
term proof
recognition_unique
show as:
view Lean formalization →
formal statement (Lean)
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₂) :=
proof body
Term-mode proof.
107 ⟨recognition_from_extraction M, fun _ _ => Iff.rfl⟩
108
109/-! ## Part 2: Cost Minima = Recognition -/
110