K_gate_tolerance

formal source

  78  rw [h.1, h.2]
  79
  80/-- Tolerance band for K-gate measurement -/
  81noncomputable def K_gate_tolerance (U : RSUnits) (σ_tau σ_ell : ℝ) : ℝ :=
  82  -- Combined uncertainty for K from τ_rec and λ_kin measurements
  83  -- σ_K = K_gate_ratio · √((σ_τ/τ)² + (σ_ℓ/ℓ)²) (error propagation)
  84  let rel_tau := σ_tau / (tau_rec_display U)
  85  let rel_ell := σ_ell / (lambda_kin_display U)
  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α']