Certified Infinite Descent Criteria in Isabelle/HOL
A reusable, locale-based framework of sloped graphs is developed that defines Infinite Descent at an abstract level, independently of any concrete graph encoding, and formalize tool-facing sufficient criteria, prove their soundness, and certify incompleteness where appropriate via verified counterexamples.