Homotopy Data for Quillen's Theorem A: Galois Connections in Lean 4

We present the first machine-checked formalization of Quillen's Theorem A for Galois connections between partial orders, as the topology discharge of the same fiber/section/obstruction architecture developed for group extensions and embedding problems. For a Galois connection (l, u) with l: P Q and u: Q P, we construct the forward and backward nerve maps together with explicit 1-simplices (closure edges p u (l (p) ) and kernel edges l (u (q) ) q) that witness the homotopy between each composition and the identity at the vertex level. We prove that the nerve of any category with a terminal object is connected with unique edges to the terminal vertex, establishing the fiber contractibility that Quillen's theorem requires. The formalization works at the simplicial set level; t