display_rate_matches_structural_rate

formal source

 111  rw [mul_div_mul_left _ _ hα']
 112
 113/-- Display derivatives (for rate transformations) -/
 114theorem display_rate_matches_structural_rate (U : RSUnits) :
 115  (lambda_kin_display U) / (tau_rec_display U) = U.ell0 / U.tau0 := by
 116  -- λ_kin / τ_rec = (2π·ℓ₀/(8 log φ)) / (2π·τ₀/(8 log φ)) = ℓ₀/τ₀
 117  simp only [lambda_kin_display, tau_rec_display]
 118  have hlog : 0 < Real.log phi := Real.log_pos one_lt_phi
 119  have h8log : 8 * Real.log phi ≠ 0 := by linarith
 120  have hpi : 2 * Real.pi ≠ 0 := by linarith [Real.pi_pos]
 121  have h2pi_ell : 2 * Real.pi * U.ell0 / (8 * Real.log phi) =
 122                  U.ell0 * (2 * Real.pi / (8 * Real.log phi)) := by ring
 123  have h2pi_tau : 2 * Real.pi * U.tau0 / (8 * Real.log phi) =
 124                  U.tau0 * (2 * Real.pi / (8 * Real.log phi)) := by ring
 125  rw [h2pi_ell, h2pi_tau]
 126  have h_factor : 2 * Real.pi / (8 * Real.log phi) ≠ 0 := by
 127    apply div_ne_zero hpi h8log
 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