reciprocal_eq_iff

formal source

  56theorem reciprocal_reciprocal (e : RecognitionEvent) : reciprocal (reciprocal e) = e := by
  57  simp only [reciprocal, inv_inv]
  58
  59theorem reciprocal_eq_iff (x e : RecognitionEvent) : reciprocal x = e ↔ x = reciprocal e := by
  60  constructor
  61  · intro h; rw [← h, reciprocal_reciprocal]
  62  · intro h; rw [h, reciprocal_reciprocal]
  63
  64theorem reciprocal_inj (x e : RecognitionEvent) : reciprocal x = reciprocal e ↔ x = e := by
  65  constructor
  66  · intro h; rw [← reciprocal_reciprocal x, h, reciprocal_reciprocal]
  67  · intro h; rw [h]
  68
  69/-- The cost of a recognition event. -/
  70noncomputable def event_cost (e : RecognitionEvent) : ℝ := J e.ratio
  71
  72/-- **Reciprocity**: Cost of event equals cost of reciprocal. -/
  73theorem reciprocity (e : RecognitionEvent) : event_cost e = event_cost (reciprocal e) := by
  74  simp only [event_cost, reciprocal]
  75  exact J_symmetric e.ratio_pos.ne'
  76
  77/-! ## Ledger Structure -/
  78
  79/-- A list of events is balanced if every event is paired with its reciprocal. -/
  80def balanced_list (l : List RecognitionEvent) : Prop :=
  81  ∀ e, l.count e = l.count (reciprocal e)
  82
  83/-- A ledger is a collection of recognition events with double-entry constraint. -/
  84structure Ledger where
  85  events : List RecognitionEvent
  86  double_entry : balanced_list events
  87
  88/-- The total cost of a ledger. -/
  89noncomputable def ledger_cost (L : Ledger) : ℝ :=