A product formula for the TASEP on a ring

For a random permutation sampled from the stationary distribution of the TASEP on a ring, we show that, conditioned on the event that the first entries are strictly larger than the last entries, the order of the first entries is independent of the order of the last entries. The proof uses multi-line queues as defined by Ferrari and Martin, and the theorem has an enumerative combinatorial interpretation in that setting. Finally, we present a conjecture for the case where the small and large entries are not separated.