  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.
  82
  83    Justification: if the reference cost were `c > 0`, then the
  84    comparison `J(eᵢ) − c` against this reference would shift if `c`

papers checked against this theorem

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