display_null_condition

formal source

 128  rw [mul_div_mul_right _ _ h_factor]
 129
 130/-- Display-level Lorentz structure: (λ/τ)² - c² = 0 (null) -/
 131theorem display_null_condition (U : RSUnits) (h : 0 < U.tau0) :
 132  ((lambda_kin_display U) / (tau_rec_display U))^2 = U.c^2 := by
 133  simp only [display_speed_eq_c U h]
 134
 135/-! Bridge Coherence and Categorical Structure -/
 136
 137/-- Units equivalence class: two units packs are equivalent if they have same c -/
 138def UnitsEquivalent (U1 U2 : RSUnits) : Prop :=
 139  U1.c = U2.c ∧ ∃ α : ℝ, α ≠ 0 ∧ U2.tau0 = α * U1.tau0 ∧ U2.ell0 = α * U1.ell0
 140
 141/-- Units equivalence is an equivalence relation -/
 142theorem UnitsEquivalent.refl (U : RSUnits) : UnitsEquivalent U U := by
 143  exact ⟨rfl, 1, by norm_num, by norm_num, by norm_num⟩
 144
 145theorem UnitsEquivalent.symm {U1 U2 : RSUnits} (h : UnitsEquivalent U1 U2) :
 146    UnitsEquivalent U2 U1 := by
 147  obtain ⟨hc, α, hα, hτ, hℓ⟩ := h
 148  refine ⟨hc.symm, α⁻¹, inv_ne_zero hα, ?_, ?_⟩
 149  · calc U1.tau0 = α⁻¹ * (α * U1.tau0) := by field_simp [hα]
 150      _ = α⁻¹ * U2.tau0 := by rw [hτ]
 151  · calc U1.ell0 = α⁻¹ * (α * U1.ell0) := by field_simp [hα]
 152      _ = α⁻¹ * U2.ell0 := by rw [hℓ]
 153
 154theorem UnitsEquivalent.trans {U1 U2 U3 : RSUnits}
 155    (h12 : UnitsEquivalent U1 U2) (h23 : UnitsEquivalent U2 U3) :
 156    UnitsEquivalent U1 U3 := by
 157  obtain ⟨hc12, α, hα, hτ12, hℓ12⟩ := h12
 158  obtain ⟨hc23, β, hβ, hτ23, hℓ23⟩ := h23
 159  refine ⟨hc12.trans hc23, α * β, mul_ne_zero hα hβ, ?_, ?_⟩
 160  · calc U3.tau0 = β * U2.tau0 := hτ23
 161      _ = β * (α * U1.tau0) := by rw [hτ12]