theorem
proved
tactic proof
display_rate_matches_structural_rate
show as:
view Lean formalization →
formal statement (Lean)
114theorem display_rate_matches_structural_rate (U : RSUnits) :
115 (lambda_kin_display U) / (tau_rec_display U) = U.ell0 / U.tau0 := by
proof body
Tactic-mode proof.
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) -/