`RecognitionTracker`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.RecognitionForcing
domain: Foundation
line: 182 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.RecognitionForcing on GitHub at line 182.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 179
 180/-! ## Part 5: Ledger Forcing -/
 181
 182structure RecognitionTracker where
 183  events : List LedgerForcing.RecognitionEvent
 184
 185def PreservesJSymmetry (T : RecognitionTracker) : Prop :=
 186  LedgerForcing.balanced_list T.events
 187
 188theorem ledger_is_minimal_recognition_tracker (T : RecognitionTracker) (hSymm : PreservesJSymmetry T) :
 189    ∃ (L : LedgerForcing.Ledger), L.events = T.events :=
 190  ⟨{ events := T.events, double_entry := hSymm }, rfl⟩
 191
 192/-! ## Part 6: Complete Bridge -/
 193
 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) :=
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.