theorem
proved
reciprocal_inj
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.LedgerForcing on GitHub at line 64.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
reciprocal -
of -
of -
reciprocal -
reciprocal_reciprocal -
RecognitionEvent -
cost -
cost -
RecognitionEvent -
of -
of -
RecognitionEvent -
of
used by
formal source
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) : ℝ :=
90 L.events.foldl (fun acc e => acc + event_cost e) 0
91
92/-- A ledger is balanced if its event list is balanced. -/
93def balanced (L : Ledger) : Prop := balanced_list L.events
94