K_gate_check

formal source

  86  K_gate_ratio * Real.sqrt (rel_tau^2 + rel_ell^2)
  87
  88/-- K-gate passes if measured values agree within tolerance -/
  89noncomputable def K_gate_check (tau_meas lambda_meas : ℝ) (U : RSUnits) (tolerance : ℝ) : Prop :=
  90  let K_tau := tau_meas / U.tau0
  91  let K_lambda := lambda_meas / U.ell0
  92  |K_tau - K_lambda| < tolerance
  93
  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