`reciprocal`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.LedgerForcing
domain: Foundation
line: 48 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.LedgerForcing on GitHub at line 48.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  45  deriving DecidableEq
  46
  47/-- The reciprocal event: B recognizes A with inverse ratio. -/
  48noncomputable def reciprocal (e : RecognitionEvent) : RecognitionEvent := {
  49  source := e.target
  50  target := e.source
  51  ratio := e.ratio⁻¹
  52  ratio_pos := inv_pos.mpr e.ratio_pos
  53}
  54
  55/-- The reciprocal of a reciprocal is the original event. -/
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.