persistent_event_state_eq_identity

formal source

 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. -/
 124theorem cooper_pairing_yields_persistent
 125    (x : ℝ) (hx : 0 < x) :
 126    ∃ e : RecognitionEvent, IsPersistent e := by
 127  refine ⟨{
 128    state := x * x⁻¹,
 129    state_pos := by
 130      rw [mul_inv_cancel₀ (ne_of_gt hx)]; norm_num
 131  }, ?_⟩
 132  show Cost.Jcost (x * x⁻¹) = 0
 133  exact cooper_pair_cost_zero x hx
 134
 135/-! ## §5. The Observer -/