pith. machine review for the scientific record. sign in
def definition def or abbrev

K_gate_check

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)

  89noncomputable def K_gate_check (tau_meas lambda_meas : ℝ) (U : RSUnits) (tolerance : ℝ) : Prop :=

proof body

Definition body.

  90  let K_tau := tau_meas / U.tau0
  91  let K_lambda := lambda_meas / U.ell0
  92  |K_tau - K_lambda| < tolerance
  93
  94/-! Advanced Display Properties -/
  95
  96/-- Display speed is positive (null cone, lightlike) -/

depends on (13)

Lean names referenced from this declaration's body.