display_speed_eq_c

formal source

  42lemma tau_rec_display_ne_zero (U : RSUnits) (h : 0 < U.tau0) : tau_rec_display U ≠ 0 := by
  43  exact ne_of_gt (tau_rec_display_pos U h)
  44
  45lemma display_speed_eq_c (U : RSUnits) (h : 0 < U.tau0) :
  46  (lambda_kin_display U) / (tau_rec_display U) = RSUnits.c U := by
  47  have hτ : tau_rec_display U ≠ 0 := tau_rec_display_ne_zero U h
  48  exact display_speed_eq_c_of_nonzero U hτ
  49
  50/-! Strengthened K-Gate Lemmas (Consolidation) -/
  51
  52/-- K-gate is independent of units rescaling -/
  53theorem K_gate_units_invariant (U : RSUnits) (α : ℝ) (hα : 0 < α) (hτ : 0 < U.tau0) :
  54  let U' : RSUnits := { tau0 := α * U.tau0, ell0 := α * U.ell0, c := U.c,
  55                        c_ell0_tau0 := by calc U.c * (α * U.tau0) = α * (U.c * U.tau0) := by ring
  56                                              _ = α * U.ell0 := by rw [U.c_ell0_tau0] }
  57  (tau_rec_display U') / U'.tau0 = (tau_rec_display U) / U.tau0 := by
  58  intro U'
  59  have hα' : α ≠ 0 := ne_of_gt hα
  60  have hτ' : U.tau0 ≠ 0 := ne_of_gt hτ
  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) :