Six Birds Verified XI: Self-Carried Closure

Abstract

Self-maintaining systems, such as cells, compilers and repair crews, were still started by something else. We make this exact for finite rule systems in which every rule names the capability that executes it, and capabilities wear out. A target carried forever by such a system must lie in the largest self-renewing part of its seed's closure. With unbounded capacity this suffices once the seed outlasts the build of that closure by one round, a bound that is attained, and a single run, which fires every enabled rule, decides the question exactly. With one firing per round, carrying self-renewing capabilities seeded in full is pinwheel scheduling, so density five sixths is the best universal threshold. Nothing is generated from the empty seed, and the minimal starting provisions are the minimal transversals of the siphons meeting the target, the sets that cannot be refilled once empty. Finally, completing the records of what the rules could produce is not producing it, and when every auditor must rank above what it audits, the highest records are never audited from within. The question is PSPACE-complete. All results are formalized in Lean 4, except that completeness and one application of a cited scheduling theorem.