IndisputableMonolith.Masses.Exponent.Gauge

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Masses
   5namespace Exponent
   6
   7def GaugeEq (m₁ m₂ : ℝ) : Prop := ∃ c : ℝ, c ≠ 0 ∧ m₁ = c * m₂
   8
   9@[simp] lemma gauge_refl (m : ℝ) : GaugeEq m m := ⟨1, by norm_num, by simp⟩
  10
  11@[simp] lemma gauge_symm {a b : ℝ} : GaugeEq a b → GaugeEq b a := by
  12  intro h; rcases h with ⟨c, hc, h⟩
  13  refine ⟨c⁻¹, inv_ne_zero hc, ?_⟩
  14  have h1 : c⁻¹ * a = b := by
  15    have : c⁻¹ * a = (c⁻¹ * c) * b := by simpa [mul_assoc, h]
  16    simpa [inv_mul_cancel hc] using this
  17  simpa [mul_comm] using h1.symm
  18
  19@[simp] lemma gauge_trans {a b c : ℝ} : GaugeEq a b → GaugeEq b c → GaugeEq a c := by
  20  intro h₁ h₂; rcases h₁ with ⟨x, hx, hxEq⟩; rcases h₂ with ⟨y, hy, hyEq⟩
  21  refine ⟨x*y, mul_ne_zero hx hy, ?_⟩
  22  simpa [hxEq, hyEq, mul_comm, mul_left_comm, mul_assoc]
  23
  24end Exponent
  25end Masses
  26end IndisputableMonolith
  27