Draft a CSJ liveness argument

One of the main things we have to convince ourselves is that CSJ does not reduce liveness, i.e. that CSJ does not change the property that we can not be delayed for prolonged periods from concluding we are caught up.

The goal of this ticket is to draft an argument for this, which also includes discussing how different approaches of disabling CSJ (a fixed slot before the wall clock; or when peers tell they have no more headers) affect it.