the entropy compression method
The entropy compression method is a proof technique, distilled from Moser's analysis of the algorithmic Local Lemma, that bounds the running time of a randomised algorithm — and thereby proves existence — by showing that if the algorithm ran too long it would let you compress a string of random bits below its own length, which is information-theoretically impossible. It rests on the bedrock fact that a uniformly random bit string cannot, on average, be compressed: any injective encoding of n-bit strings must use at least n bits for some of them. So if a hypothetical long execution would yield a too-short encoding, that execution cannot happen. It is a counting argument disguised as a thermodynamic one.
The mechanism works as follows. Run a randomised algorithm that consumes fresh random bits and, whenever it hits a bad configuration, takes a corrective step (like Moser-Tardos resampling). Maintain a log that records, in compact form, enough about the algorithm's history to reconstruct exactly which random bits were used. The trick is to design the log so that an execution of length T is encoded by a string strictly shorter than the T random bits it consumed — typically because the structure of the corrective steps (a witness tree, a sequence of constraint indices) is highly constrained and so carries less information than raw randomness. If the encoding is injective and shorter than its input, then distinct random-bit sequences would map to fewer codewords than there are sequences, a contradiction once T is large. Hence T must be small: the algorithm terminates quickly, and a good configuration is reached. Existence is the by-product of fast termination.
Its significance is twofold. First, it gives constructive, polynomial-time proofs where earlier methods (the classical LLL) gave only non-constructive existence, and the proofs are often shorter and more transparent than the original. Second, it has become a flexible tool in its own right, used well beyond the Local Lemma — for example to prove bounds in nonrepetitive (square-free) colourings of graphs, in pattern avoidance, and in acyclic edge colouring, sometimes giving better constants than the LLL. The honest caveat is that the method requires a genuinely clever, problem-specific encoding: the whole proof hinges on showing the log is injective and short, and there is no automatic recipe — a sloppy encoding either fails to be reconstructible (not injective) or is not actually shorter, and then the argument collapses. It bounds expected or typical running time and existence; it is not a panacea and does not by itself give the sharpest possible thresholds.
Nonrepetitive colouring of a path: colour the vertices of a long path so that no two adjacent equal-length blocks have identical colour sequences (no 'square'). A greedy random algorithm recolours a block whenever a square appears. Logging which squares were fixed lets you reconstruct all the random colour choices from a description shorter than those choices themselves if the run is long — impossible — so the run is short and a square-free colouring with a bounded number of colours exists, recovering (and refining) a Local-Lemma bound.
A long run would compress its own random bits below their length — impossible — so the run is short and a good object exists.
There is no automatic recipe: the whole proof depends on a clever problem-specific log that is provably injective AND shorter than its input; a sloppy encoding is either non-reconstructible or not actually shorter, and the argument collapses.