Theorem: Scheduling and complete-output induction

Every legal schedule returns complete accepted ${\mathsf{Ein}}_0$ and valid original-name locations after every command. Geometric commands preserve the currently installed packet and reference-frame signature. A source command returns the complete newly installed packet and signature.

Under ass:control, two aligned legal executions with equal initial geometric/controller inputs, resources, permissions, declared accessible inputs, and original matter reductions have equal geometric outputs, controller outputs, and original-name transports. Their original matter reductions remain equal. Inaccessible spectator extensions do not change geometric decisions.

At every command boundary, the incomplete outputs of prop:complete-output are rejected. This conclusion is not restricted to the initial reference packet.

Proof. Proceed by induction from the certified initial configuration. A flow output is complete by Theorem C1. An incidence output is complete by the appropriate realization/germ interface and Theorem C2, and uses the certified transport in sec:locations.

At ${\mathsf{S}}_{\mathrm{tab}}$, the regular parameter remains $s=-1/2$. Evaluation of the particle constructor at the promised table entry returns the full new realization, including new rays, seam, charts, collar, and matching data. Persistent incoming labels remain valid. Only the source permission and source stage change in addition to the installed geometric data. Legality places this complete output in the next command's domain. This proves certificate and location induction.

For paired executions, deterministic control selects equal commands, guards, geometric outputs, transports, and successor controller states from equal declared inputs. Every T0 command is the identity on internal matter. For a spectator extension $\tilde{\rho }$ with original reduction $\rho$,

for each accessible original observable $B$. Equal original reductions thus give equal accessible functionals. The classical tokens are separately required to agree and satisfy their promises; no extraction step is used. Separately reserved spectator storage prevents a spectator-number capacity guard.

Finally, acceptance includes the complete obligations after each command. The local calculations in prop:complete-output apply at the packet installed at that boundary, including after a source replacement.