CoherentRecognition

formal source

  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 :=
  94  RecognitionEvent.identity_cost
  95
  96/-- Any persistent reference has state exactly `x = 1`. -/
  97theorem persistent_state_unique
  98    (ref : RecognitionEvent) (h : IsPersistent ref) :
  99    ref.state = 1 :=
 100  (Cost.Jcost_eq_zero_iff ref.state ref.state_pos).mp h
 101
 102/-- Persistence is preserved under definitional substitution: any
 103    persistent reference event has the same state as the canonical
 104    identity event. -/