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 Cook2004,Cook2009. 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 rule110-lean rule110-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 (cook\_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 (cook\_c2\_tape\_bit\_decoder\_exists\_upto7), and a complete C1 discharge for arbitrary words at slots 20 (cook\_c2\_tape\_bit\_general, , zero sorry). Five construction-collision kinds are certified by finite native\_decide witnesses; Stage 3 data-cone simulation is discharged for empty appendants and fully for the length-6 benchmark CTS; four TMCompilesStep scaffolds anchor Stage 4 compilation, and CookFinTM2Compiles is proved for Mathlib's halting identity machine (idComputer Bool, ). The top theorem rule110\_turing\_universal\_from\_cook (CookUniversalityTop) is a zero-sorry Lean theorem, contingent on five named Cook bridge axioms formalizing Cook's 4 collision analysis for general CTS configurations (cook\_cts\_data\_cones\_origin\_one\_step\_ax and four companions). Closing all five will upgrade the conditional UGP incompleteness results in SpivackCompUniversality from physics-bridge status to unconditional .