single_inequality_audit

formal source

  72
  73    Since `(tau_rec_display U)/τ0 = (lambda_kin_display U)/ℓ0` by `K_gate_eqK`,
  74    the inequality direction is immediate. -/
  75theorem single_inequality_audit (U : RSUnits) (hτ : U.tau0 ≠ 0) (hℓ : U.ell0 ≠ 0) :
  76  (tau_rec_display U) / U.tau0 ≤ (lambda_kin_display U) / U.ell0 := by
  77  have h := K_gate_eqK U hτ hℓ
  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)