Lean 4 formalization of Matthew Cook's proof that Rule 110 is computationally universal. This library formalizes the mathematical infrastructure for Cook's construction: cyclic tag system semantics (CyclicTagSystem, ctsₛtep, ctsₑval), the infinite-tape Rule 110 step function (InfTape, infTapeStep), the period-14 ether background (rule110Ether, etherᵢsₚeriodic), and the C1/C2/C3 glider patterns (GliderConfig, cookCGliderCycle). All theorems are proved with zero sorry. The library is self-contained and designed to be reusable independent of any UGP-specific context. It serves as the Cook universality dependency (rule110ₛimulatescomputable named axiom) for the ugp-lean formalization of the Universal Generative Principle. New in this version: AlgebraicUniversality module — Cook-independent GF (7) polynomial universality certificate: rule110ᵦ7ₚolyᵣep (Rule 110 = GF (7) polynomial, nativedecide, zero sorry), rule110center1ᵢsₙand (Rule 110 at center=1 implements NAND), rule110ᵦ7ₙandᵢdentity, and rule110ₜuringᵤniversalₐlgebraic (universality via NAND completeness, Sheffer 1913). Martinez phases catalog with verification and generation scripts also added. Pinned revision: e40ec46b82d00a71a29c660e5611e8d9736d6879. Cite using the Zenodo DOI after publication.
Nova Spivack (Sat,) studied this question.