`cost`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.ObserverForcing
domain: Foundation
line: 51 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ObserverForcing on GitHub at line 51.

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

  48namespace RecognitionEvent
  49
  50/-- The cost of a recognition event is its J-cost. -/
  51noncomputable def cost (e : RecognitionEvent) : ℝ := Cost.Jcost e.state
  52
  53/-- The cost of any recognition event is non-negative. -/
  54theorem cost_nonneg (e : RecognitionEvent) : 0 ≤ e.cost :=
  55  Cost.Jcost_nonneg e.state_pos
  56
  57/-- The canonical identity event sits at the J-cost minimum (`x = 1`). -/
  58def identity : RecognitionEvent where
  59  state := 1
  60  state_pos := by norm_num
  61
  62/-- The identity event has zero cost. -/
  63theorem identity_cost : identity.cost = 0 := by
  64  show Cost.Jcost 1 = 0
  65  exact Cost.Jcost_unit0
  66
  67end RecognitionEvent
  68
  69/-! ## §2. Coherent Recognition Structures -/
  70
  71/-- A coherent recognition structure: a sequence of recognition events
  72    with at least two distinguishable states, plus a reference event
  73    used for comparison. -/
  74structure CoherentRecognition where
  75  events : ℕ → RecognitionEvent
  76  reference : RecognitionEvent
  77  nontrivial : ∃ n m : ℕ, (events n).state ≠ (events m).state
  78
  79/-! ## §3. The Persistent Reference -/
  80
  81/-- A reference is *persistent* if its J-cost is zero.

papers checked against this theorem

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