K_gate_ratio

formal source

  15  (2 * Real.pi * U.ell0) / (8 * Real.log phi)
  16
  17/-- The K-gate ratio constant. -/
  18noncomputable def K_gate_ratio : ℝ := Real.pi / (4 * Real.log phi)
  19
  20/-- Clock-side ratio equals K_gate_ratio. -/
  21@[simp] lemma tau_rec_display_ratio (U : RSUnits) (hτ : U.tau0 ≠ 0) :
  22  (tau_rec_display U) / U.tau0 = K_gate_ratio := by
  23  unfold tau_rec_display K_gate_ratio
  24  field_simp [hτ]
  25  ring
  26
  27/-- Length-side ratio equals K_gate_ratio. -/
  28@[simp] lemma lambda_kin_display_ratio (U : RSUnits) (hℓ : U.ell0 ≠ 0) :
  29  (lambda_kin_display U) / U.ell0 = K_gate_ratio := by
  30  unfold lambda_kin_display K_gate_ratio
  31  field_simp [hℓ]
  32  ring
  33
  34/-- Kinematic consistency: c · τ_rec(display) = λ_kin(display). -/
  35lemma lambda_kin_from_tau_rec (U : RSUnits) : U.c * tau_rec_display U = lambda_kin_display U := by
  36  simp only [tau_rec_display, lambda_kin_display]
  37  -- Goal: U.c * (2 * π * τ₀ / (8 * log φ)) = 2 * π * ℓ₀ / (8 * log φ)
  38  have h : U.c * U.tau0 = U.ell0 := U.c_ell0_tau0
  39  calc U.c * (2 * Real.pi * U.tau0 / (8 * Real.log phi))
  40      = (2 * Real.pi * (U.c * U.tau0)) / (8 * Real.log phi) := by ring
  41    _ = (2 * Real.pi * U.ell0) / (8 * Real.log phi) := by rw [h]
  42
  43/-- Canonical K-gate: both route ratios equal K_gate_ratio. -/
  44theorem K_gate_eqK (U : RSUnits) (hτ : U.tau0 ≠ 0) (hℓ : U.ell0 ≠ 0) :
  45  ((tau_rec_display U) / U.tau0 = K_gate_ratio) ∧ ((lambda_kin_display U) / U.ell0 = K_gate_ratio) := by
  46  exact ⟨tau_rec_display_ratio U hτ, lambda_kin_display_ratio U hℓ⟩
  47
  48end RSUnits