units_quotient_preserves_K

formal source

  61  rw [tau_rec_display_ratio U hτ', tau_rec_display_ratio U' (mul_ne_zero hα' hτ')]
  62
  63/-- Units quotient functoriality: K-gate commutes with units transformations -/
  64theorem units_quotient_preserves_K (U : RSUnits) (hτ : U.tau0 ≠ 0) (hℓ : U.ell0 ≠ 0) :
  65  ∀ (α : ℝ), α ≠ 0 →
  66    -- Under rescaling (τ0, ℓ0) → (α·τ0, α·ℓ0), K_gate_ratio remains invariant
  67    (tau_rec_display U) / U.tau0 = K_gate_ratio := by
  68  intro α _hα
  69  exact tau_rec_display_ratio U hτ
  70
  71/-- Single-inequality audit: checking one route inequality suffices (routes equal).
  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 -/