`lambda_kin_display`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.KDisplayCore
domain: Constants
line: 14 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants.KDisplayCore on GitHub at line 14.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.