identity_persistent

formal source

  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. -/
 105theorem persistent_event_state_eq_identity
 106    (ref : RecognitionEvent) (h : IsPersistent ref) :
 107    ref.state = RecognitionEvent.identity.state := by
 108  rw [persistent_state_unique ref h]
 109  rfl
 110
 111/-! ## §4. Cooper Pairing as the Constructive Source of Persistence -/
 112
 113/-- For any positive `x`, the pair state `x · x⁻¹` collapses to the
 114    identity tick. This is the structural origin of persistence: even
 115    when no event sits at `x = 1` directly, any pair of inverse states
 116    constructs a persistent reference. -/
 117theorem cooper_pair_cost_zero (x : ℝ) (hx : 0 < x) :
 118    Cost.Jcost (x * x⁻¹) = 0 := by
 119  rw [mul_inv_cancel₀ (ne_of_gt hx)]
 120  exact Cost.Jcost_unit0
 121
 122/-- Cooper pairing constructs a persistent recognition event from any
 123    positive starting state. -/