In 2009, Moser published a breakthrough [paper](https://dl.acm.org/citation.cfm?id=1536462) constructifying the Lovász Local Lemma (LLL). His talk at STOC was described in a [blog post](https://blog.computationalcomplexity.org/2009/06/kolmogorov-complexity-proof-of-lov.html) by Fortnow that proves a slightly weakened result using Kolmogorov complexity. This led to a great [write-up](https://terrytao.wordpress.com/2009/08/05/mosers-entropy-compression-argument/) by Terry Tao that coined the term entropy compression, and this method has since been extended to various combinatorial problems.


Both Fortnow and Tao describe how Moser's algorithm takes a (Kolmogorov or statistically) random bit string $r$ and produces a final assignment $x$ and a history record $h$ (essentially the witness tree of Moser's paper). Since $r$ can be reconstructed exactly from $x$ and $h$, they claim that, in expectation or with high probability, $|x| + |h| \geq |r|$, because you can't compress a random string beyond its Shannon entropy or compress a Kolmogorov random string at all. From this sort of inequality, you can deduce that Moser's algorithm runs efficiently.


I found both of these explanations quite elegant at first but am now struggling to see their correctness as stated (though I in no way doubt the correctness of the proof in Moser's paper). My problem with Tao's entropy argument is that the source coding theorem applies to compression protocols, but Moser's algorithm doesn't seem to fall into this category exactly. It's not as if each string $r$ (or each $r$ of some fixed size) corresponds to an $x,h$ pair; for some $r$, the algorithm will terminate after seeing just a prefix of the bits, and only this prefix will be in correspondence with the final $x,h$ pair.


With the Kolmogorov complexity argument, Fortnow starts by fixing a Kolmogorov random $r$ of proper length, but this length depends on the run time of the algorithm, which in turn depends on the selected string. I can't work my way out of this circularity.


Any insight here? Specifically, I would be very interested in a formal description of an entropy compression principle guaranteeing that, for an algorithm $\mathcal{A}$ similar to Moser's, $$|\mathcal{A}(r)| \geq |r|,$$
in expectation or with high probability, where $r$ denotes the random bit string used by the algorithm if it is provided with fair coin flips until termination (that is, we are not sampling $r$ uniformly from all strings of a fixed size, but rather from the random process determined by the algorithm when provided with a fair coin).



Formalizing Entropy Compression (as used to constructify the Lovász Local Lemma)
In my formulation of the argument, the length of the string $r$ (which I call $R$) *is* fixed: one does indeed only read a prefix of this string, but the remaining unread bits of the string are saved as part of the output (and referred to in my writeup as $R'$). The precise length of $r$ is not terribly relevant (it cancels out on both sides of the entropy inequality) so long as it is longer than any possible number of bits read from it through the algorithm; in my writeup I choose the fixed length of $r$ to be $Mk$ (in my notation).


Fortnow's argument is similar; the random string $r$ (which he calls $x$) has a fixed length (which in his notation is $n+sk$), and any bits not read by the "Fix" algorithm are appended to the output string.


