I continue to feel very lucky that I stumbled into working on this project; it lends itself to so many tiny more-or-less tractable sub-problems and puzzles that I get a constant trickle of new stuff to play with that gives me some feeling of forward progress, even though it's not always entirely clear towards what.
Anyway the new thing that came out of the discussion after the talk is that while you can't lift "distance sensitive comparison functions" (by which I really mean sorting-network-like compare-and-maybe-swap operations that have a type like τ * τ -o τ * τ that take two elements of τ and puts them in sorted order --- this is in contrast to the usual world where we have the luxury of being able to demand discontinuous comparison functions τ * τ -o bool) up through product types, you can lift them through sums. Because totality of partial orders is preserved by order-sum, but not lexicographic product? I think that is the essential reason anyway.
Afterwards I got a good few solid contiguous hours in the Paper Writing Zone. I am a machine for turning burritos and nilla wafers into theorems!