GreedTok is a Constant-Factor Approximation for Partition-Cover Tokenization

GreedTok (Lim, Tan, Choo and Lauw, NeurIPS 2025) builds a tokenizer vocabulary greedily for the partition-cover objective: choose k tokens so as to maximize the number of adjacent character pairs merged when the corpus is segmented optimally. The objective is neither submodular nor supermodular, so the classical 1 − 1/e analysis does not apply, and a worst-case guarantee was left open. We prove that GreedTok is a constant-factor approximation: on every corpus and for every budget k it achieves at least 0.2752 of the optimum, and it is optimal for k = 1. The bound holds for both the exact greedy loop and the lazy priority-queue loop of the published algorithm and its code. The key ingredient is a shift lemma: if two occurrences of a not-yet-chosen token overlap and both are still usable, they offer exactly the same gain, so GreedTok's left-to-right scoring loses nothing when occurrences collide. A per-occurrence charging argument, with window distributions certified in exact arithmetic or given in closed form, completes the proof. In the other direction, we construct corpora on which GreedTok, with adversarial tie-breaking, achieves at most a fraction of the optimum tending to (7 − ln 2)/12 ≈ 0.5256 (below 0.5380 when every greedy choice is unique). Finally, we show that the objective is NP-hard to approximate within 1 − 1/31580, to our knowledge the first inapproximability result for it. The supplementary archive (greedtok-ratio-supplement.zip) contains the code, exact certificates, and result files needed to reproduce every computer-assisted step; see its README. Code is released under the MIT license.