display_speed_positive

formal source

  94/-! Advanced Display Properties -/
  95
  96/-- Display speed is positive (null cone, lightlike) -/
  97theorem display_speed_positive (U : RSUnits) (h : 0 < U.tau0) (hc : 0 < U.c) :
  98  0 < (lambda_kin_display U) / (tau_rec_display U) := by
  99  rw [display_speed_eq_c U h]
 100  exact hc
 101
 102/-- Displays scale uniformly: ratio is scale-invariant -/
 103theorem display_ratio_scale_invariant (U : RSUnits) (hτ : 0 < U.tau0) (α : ℝ) (hα : 0 < α) :
 104  let tau' := α * (tau_rec_display U)
 105  let lambda' := α * (lambda_kin_display U)
 106  lambda' / tau' = (lambda_kin_display U) / (tau_rec_display U) := by
 107  intro tau' lambda'
 108  have hα' : α ≠ 0 := ne_of_gt hα
 109  have hτ' : tau_rec_display U ≠ 0 := tau_rec_display_ne_zero U hτ
 110  simp only [tau', lambda']
 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