Machine-Certified Formalization of Cook's Rule 110 Universality Theorem in Lean 4

Matthew Cook proved that elementary cellular automaton Rule~110 is computationally universal by embedding cyclic tag systems (CTS) into the glider dynamics of Rule~110's periodic ether background~. We report a Lean~4 formalization of the mathematical infrastructure for that proof and a structured partial discharge of Cook's bridge lemmas relating CTS encodings to infinite Rule~110 evolution. The library 110-lean~ formalizes infinite-tape semantics, ether stability, CTS evaluation, glider overlays, and the Cook–Neary–Woods collision checklist; on this foundation we discharge the far-field one-step simulation axiom ( \_cts\_step\_sim\_ax, ) and a substantial partial family of tape-bit readback lemmas for words of length L 7 with ossifier–leader support encoding, including existence of a decoder matching Cook's global C1 shape on that family ( \_c2\_tape\_bit\_decoder\_exists\_upto7), and a complete C1 discharge for arbitrary words at slots 20 ( \_c2\_tape\_bit\_general, , zero ). Five construction-collision kinds are certified by finite \_decide witnesses; Stage~3 data-cone simulation is discharged for empty appendants and fully for the length-6 benchmark CTS; four scaffolds anchor Stage~4 compilation, and 2Compiles is proved for Mathlib's halting identity machine ( Bool, ). The top theorem 110\_turing\_universal\_from\_cook ( ) is a zero- Lean theorem, contingent on five named Cook bridge axioms formalizing Cook's 4 collision analysis for general CTS configurations ( \_cts\_data\_cones\_origin\_one\_step\_ax and four companions). Closing all five will upgrade the conditional UGP incompleteness results in from physics-bridge status to unconditional .