Manuscript En05-B@1 · En05-B.tex · theorem · 8b626460
Theorem: Routing from every starting tick
A legal partition schedule under one clock · lines 726–791 · proof included or linked
En05-B@1#thm:routing, En05-B@1#eq:hubtime, En05-B@1#eq:alltime
For any starting tick and hubs at physical separation , a logical register can be delivered to the target hub in elapsed physical time at most
For arbitrary sites at physical separation , one may use
All waiting, junction transitions, initialization into a lane, and terminal delivery are included.
In particular, on journeys with ,
and the excess tends to zero uniformly.
Proof. For hubs, wait less than one frame, hence at most , for a phase-zero firing. Use the hub route of Lemma lem:hubroute. At the initial phase-zero firing, move the register from hub memory into the first outgoing port. Lemma lem:frame traverses the lane. At each intermediate phase-zero firing, move directly from the incoming port into the next outgoing port, inside the one junction block. Each complete lane consumes one frame of duration . After the last lane, the next phase-zero firing moves the register into target hub memory in one further tick. Thus
If the hubs coincide, waiting or local storage satisfies the same bound.
For an arbitrary starting site on a lane, wait until a transport frame starts. If its index is even, start forward movement at the first transport phase; if odd, start at the second. Advance to the last port, retain the register there, and move it into that hub at the next phase-zero firing. This costs at most . A register at a hub can similarly reach any specified site on one of its outgoing lanes in at most .
Choose these initial and final hubs. Each is within physical distance of its respective site. The hub-to-hub separation is at most . Applying (eq:hubtime) and adding the two endpoint costs gives
Storage is achieved by leaving the relevant memory factor unchanged, not by changing the partition schedule.
Displayed formulas in this passage
En05-B@1#eq:hubtime · line 731
En05-B@1#eq:alltime · line 737
unlabeled · line 748
unlabeled · line 767
unlabeled · line 786