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
Store the host in a two-head machine of 4096 cells so that it reproduces itself by the dynamics, prove the machine's netlist for every window size, add figures and the layouts behind the digests, and remove the interpreter tower and the verification tiers
Replace the interpreter sections with the two-head machine and translating organism proved in Rocq, prove the hosted constructor in full, compute the restoration bound in C, add independent reproductions of the paper's constructions and measurements, and cut the paper to 36 pages
