Break or provably defend a published LLM watermark

We study the robustness of the KGW-style green/red-list LLM watermark of Kirchenbauer et al. (2023) under adversarial post-generation editing. Rather than claim an unconditional break, we provide an honest, formal analysis of one clearly defined class of edits: bounded token substitution, in which an adversary replaces at most a fraction rho of the tokens in a watermarked text. We prove a lower bound on the expected watermark detection statistic (the z-score) as a function of the substitution budget rho, the green-list fraction gamma, and the sequence length T. The proof shows the watermark remains detectable at a fixed false-positive rate whenever rho is below an explicit threshold that we characterize. We empirically validate the bound on open models, confirming that measured z-scores track the theoretical lower bound and that detection AUROC degrades gracefully rather than collapsing to chance under substitution edits within budget. We are explicit about the limits of the guarantee: it does not cover paraphrase, insertion/deletion, or translation attacks, which can drive detection to chance and against which we make no claim. Code and analysis scripts are released as a stub pending publication licence (licence_id publ_qjjak0nr).