Manuscript En03-A@1 · En03-A.tex · theorem · 5398614e
Theorem: Retiming invariance
Kinematics and causal cuts on a prescribed schedule › Retiming fixed gates · lines 872–885 · proof included or linked
En03-A@1#thm:retiming
All legal executions of an admissibly ordered labelled gate set have the same total channel.
Proof. Incomparable gates act on disjoint factors and commute. Any two linear extensions are connected by adjacent swaps of incomparable elements: move the first desired differing element leftwards; every crossed element must be incomparable, since either comparability would contradict one of the extensions. Repeat.