Brams–Taylor–Zwicker procedure


The Brams–Taylor–Zwicker procedure is a protocol for envy-free cake-cutting among 4 partners.
The procedure uses a variation of Austin's procedure for two partners and general fractions. That procedure allows two partners to divide an entire cake to pieces, each of which is worth exactly for both of them.
The main procedure works as follows.
A. Use Austin's procedure with and partners #1 and #2. So we have 4 pieces that the first two partners believe to be of exactly identical value of 1/4.
B. Partner #3 trims one piece to create a two-way tie for the largest; the partners now choose pieces in reverse order. Either #4 or #3 must take the trimmed piece. This creates an envy-free division for the entire cake less the trimmings.
C. Now the trimmings are divided. Assume w.l.o.g. that #3 took the trimmed piece. We use Austin's procedure again with the trimmings and partners #4 and #1, to create 4 pieces each of which equals exactly 1/4 for both of them. Since partners #1 and #2 have an irrevocable advantage over whoever partner that took the trimmed piece, we can let #3 be the first to select a piece from the trimming, then #2, then #4 and #1.

Efficiency

The run-time of the procedure is, technically, infinite, since Austin's procedure involves two knives moving continuously, and this procedure cannot be discretized.
The number of cuts is bounded, though. Austin's procedure requires 2 cuts to divide a cake between 2 people with an exact value of 1/2; each of these pieces should be divided with 2 more cuts to generate the 4 pieces with exact value of 1/4. So in total, 6 cuts are needed for step A. A single cut is done in step B and 6 more cuts in step C, for a total of 13 cuts.
An advanced variant of the Brams–Taylor–Zwicker procedure uses only 11 cuts.