IndisputableMonolith.Constants.KDisplayCore

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace Constants
   6
   7namespace RSUnits
   8
   9/-- Clock-side display definition: τ_rec(display) = (2π·τ₀) / (8 ln φ). -/
  10@[simp] noncomputable def tau_rec_display (U : RSUnits) : ℝ :=
  11  (2 * Real.pi * U.tau0) / (8 * Real.log phi)
  12
  13/-- Length-side (kinematic) display definition: λ_kin(display) = (2π·ℓ₀) / (8 ln φ). -/
  14@[simp] noncomputable def lambda_kin_display (U : RSUnits) : ℝ :=
  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
  49end Constants
  50end IndisputableMonolith
  51