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

lambda_kin_display_ratio

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)

  28@[simp] lemma lambda_kin_display_ratio (U : RSUnits) (hℓ : U.ell0 ≠ 0) :
  29  (lambda_kin_display U) / U.ell0 = K_gate_ratio := by

proof body

Term-mode proof.

  30  unfold lambda_kin_display K_gate_ratio
  31  field_simp [hℓ]
  32  ring
  33
  34/-- Kinematic consistency: c · τ_rec(display) = λ_kin(display). -/

used by (1)

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

depends on (8)

Lean names referenced from this declaration's body.