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

cost_to_recognition_bridge

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)

 194theorem cost_to_recognition_bridge :
 195    (∀ x : ℝ, x ≠ 0 → LedgerForcing.J x = LedgerForcing.J x⁻¹) ∧
 196    (∃ e : LedgerForcing.RecognitionEvent, e.ratio = 1 ∧ recognition_cost e = 0) ∧
 197    (∀ (S : Type) (M : ObservableExtractionMechanism S), ∃ R : RecognitionStructure S, True) ∧
 198    (∀ (S : JStableStructure), ∃ (R : RecognitionLikeStructure), R.carrier = S.carrier) :=

proof body

Term-mode proof.

 199  ⟨fun x hx => LedgerForcing.J_symmetric hx,
 200   global_minimum_is_self_recognition,
 201   fun _ M => ⟨recognition_from_extraction M, trivial⟩,
 202   stability_forces_recognition⟩
 203
 204end RecognitionForcing
 205end Foundation
 206end IndisputableMonolith

depends on (23)

Lean names referenced from this declaration's body.