  77It does **not** yet encode the “pulsing restores it” part; that will require
  78either richer trace fields (power/temperature) or explicit segment labels.
  79-/
  80def PhaseLockFalsifier (window : ℕ) (drop : ℝ) (tr : Trace) : Prop :=
  81  ∃ t1 t2,
  82    t1 < t2 ∧
  83    (∀ t, t1 ≤ t ∧ t < t1 + window → (tr.schedule t).pulse = true) ∧
  84    (∀ t, t2 ≤ t ∧ t < t2 + window → (tr.schedule t).pulse = true) ∧
  85    (tr.thrust t1).2.2 - (tr.thrust t2).2.2 ≥ drop
  86
  87end Falsifiers
  88end Flight
  89end IndisputableMonolith
  90

papers checked against this theorem

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