  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`
  85    itself depended on the comparison context. The only invariant
  86    cost across arbitrary recognition events is `c = 0`, since
  87    `Jcost = 0` is the unique global minimum (`Cost.Jcost_eq_zero_iff`).
  88    A reference at any other cost is not a fixed frame; it is itself
  89    in motion. -/
  90def IsPersistent (ref : RecognitionEvent) : Prop := ref.cost = 0
  91
  92/-- The identity event is persistent. -/
  93theorem identity_persistent : IsPersistent RecognitionEvent.identity :=

papers checked against this theorem

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