pith. machine review for the scientific record. sign in
theorem proved term proof

recognition_forcing_complete

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 161theorem recognition_forcing_complete :
 162    (∀ (S : Type) (obs : Observable S),
 163      (∃ s₁ s₂, obs.value s₁ ≠ obs.value s₂) →
 164      ∃ (R₁ R₂ : Type), Nonempty (Recognition.Recognize R₁ R₂)) ∧
 165    (∀ (S : Type) (M : ObservableExtractionMechanism S),
 166      ∃ R : RecognitionStructure S, True) ∧
 167    (∀ (e : LedgerForcing.RecognitionEvent),
 168      (e.ratio = 1 ↔ recognition_cost e = 0) ∧
 169      (e.ratio ≠ 1 → recognition_cost e > 0)) ∧
 170    (∀ (c : Configuration),
 171      ∃ (e : LedgerForcing.RecognitionEvent), e.ratio = c.value) ∧
 172    (∀ (S : JStableStructure),
 173      ∃ (R : RecognitionLikeStructure), R.carrier = S.carrier) :=

proof body

Term-mode proof.

 174  ⟨recognition_necessary,
 175   fun _ M => ⟨recognition_from_extraction M, trivial⟩,
 176   recognition_is_cost_structure,
 177   cost_minima_are_recognition,
 178   stability_forces_recognition⟩
 179
 180/-! ## Part 5: Ledger Forcing -/
 181

depends on (30)

Lean names referenced from this declaration's body.