一句话：在 Isabelle/HOL 中形式化序论不动点定理，将完备序结果推广到仅需反对称性或吸引性的非传递关系。
论文针对经典序论不动点定理通常依赖传递性（或偏序）的局限，在 Isabelle/HOL 中建立一套尽可能一般的序论不动点定理库。作者以完备关系为框架，仅假设反对称性或吸引性——一种由二者之一蕴含的温和条件——重新证明若干关于完备序的著名结果。核心贡献是将保证单调映射存在拟不动点的系列定理推广到非传递关系，并证明（拟）不动点集合自身也是完备的。该工作统一并加强了 Knaster-Tarski、Bourbaki-Witt、Kleene、Markowsky、Pataraia、Mashburn、Bhatta-George 及 Stouti-Maaden 等定理，所有结果均在 Isabelle/HOL 中机器验证。
In this paper, we develop an Isabelle/HOL library of order-theoretic fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often with only antisymmetry or attractivity, a mild condition implied by either antisymmetry or transitivity. In particular, we generalize various theorems ensuring the existence of a quasi-fixed point of monotone maps over complete relations, and show that the set of (quasi-)fixed points is itself complete. This result generalizes and strengthens theorems of Knaster-Tarski, Bourbaki-Witt, Kleene, Markowsky, Pataraia, Mashburn, Bhatta-George, and Stouti-Maaden.