Prove the stored host's construction, copies, period and network in Rocq for every word width, give each unit its own window cell, and revise Section 8 with the new records
Prove self-reproduction by the dynamics for the stored host of every word width, with a sign-extending device read and the record count in closed form, check the stored hosts of widths 9 and 10 symbolically and on random states, check the extracted host family for widths 8 to 10, and remove the to-do note
Prove in Rocq that the host family computes SUBLEQ at every word width, check the stored host's startup and step records on decision diagrams, state the stored-host theorems for every stored host with their overhead, bound self-reproduction under noise, remove the neuromorphic mappings, and cut the paper to 30 pages
Consolidate the Python sources into twelve files with one-line docstrings, fold the demos into the playground, and delete the scripts that do not belong to the artifact
