J_symmetric

formal source

  24noncomputable def J (x : ℝ) : ℝ := (x + x⁻¹) / 2 - 1
  25
  26/-- **J-Symmetry**: J(x) = J(1/x) for all x ≠ 0. -/
  27theorem J_symmetric {x : ℝ} (_hx : x ≠ 0) : J x = J (x⁻¹) := by
  28  simp only [J, inv_inv]; ring
  29
  30/-- J-symmetry in ratio form: J(a/b) = J(b/a). -/
  31theorem J_symmetric_ratio {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) :
  32    J (a / b) = J (b / a) := by
  33  have h1 : (a / b)⁻¹ = b / a := by field_simp
  34  rw [← h1]
  35  exact J_symmetric (div_ne_zero ha hb)
  36
  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]