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 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
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
