def definition def or abbrev

`validateKGate`

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

formal statement (Lean)

 193noncomputable def validateKGate (meas : KGateMeasurement) : Prop :=

proof body

Definition body.

 194  let tolerance := K_gate_tolerance meas.units meas.sigma_tau meas.sigma_lambda
 195  |meas.K_from_tau - meas.K_from_lambda| < tolerance
 196
 197/-- Falsifier: K-gate mismatch beyond tolerance -/

used by (1)

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

falsifier_K_gate_mismatch in IndisputableMonolith.Constants.KDisplay decl_use

depends on (4)

Lean names referenced from this declaration's body.

K in IndisputableMonolith.Constants decl_use
KGateMeasurement in IndisputableMonolith.Constants.KDisplay decl_use
K_gate_tolerance in IndisputableMonolith.Constants.KDisplay decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use