`RecognitionEvent`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.LedgerForcing on GitHub at line 40.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  37/-! ## Recognition Events -/
  38
  39/-- A recognition event between two agents. -/
  40structure RecognitionEvent where
  41  source : ℕ
  42  target : ℕ
  43  ratio : ℝ
  44  ratio_pos : 0 < ratio
  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

papers checked against this theorem

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