pith. machine review for the scientific record. sign in
lemma proved tactic proof

lambda_kin_from_tau_rec

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  35lemma lambda_kin_from_tau_rec (U : RSUnits) : U.c * tau_rec_display U = lambda_kin_display U := by

proof body

Tactic-mode proof.

  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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (15)

Lean names referenced from this declaration's body.