Quantile cycles

Quantile-based distributional RL represents each action’s return distribution by a few quantiles and acts greedily on their mean. For evaluating a fixed policy, hard quantile-projected Bellman updates converge. I asked whether they also converge for control, when the greedy action can change—and whether a failure survives sampled Huber learning.

I constructed one-state, two-action problems and checked their exact Bellman backups in rational arithmetic. The paper proof covers a corresponding problem for every quantile count K ≥ 2. I separately formalized the smallest rational instance in Lean.

I then compared hard projection, pinball and Huber updates with a paired scalar learner. The sampled test used 32 seeds, 100,000 updates and batches of 32 target pairs per action. I fixed the methods, endpoint and rule for continuing to replay/network experiments before the run.

The exact operator does not converge. For every K ≥ 2 there is a one-state, two-action problem with no fixed point. Every finite real starting table approaches a strict two-cycle, modulo phase. The greedy choices on the cycle alternate between the unique optimal action and a worse one; no greedy tie is needed.

The smallest case uses two quantiles and discount 1/4. A always pays 91/128. B pays 0, 1/2 or 1 with probabilities 3/16, 1/2 and 5/16. A’s true mean-reward advantage is 19/128, and always choosing B loses 19/96 in discounted value. The projected means instead favor A by 3/128 in one phase and B by 3/128 in the next (exact certificates, phase diagram).

A delay-chain construction keeps the discount fixed at 0.9. These instances have local attraction, not a claim that all starts approach one common phase:

Quantiles K	States	Cycle length
2	14	28
3	18	36
8	27	54
16	33	66
32	40	80

The state counts and cycle lengths above are in the same certificates.

Lean’s kernel checks the specific rational K=2, discount-1/4 cycle: the actual target laws, all eight generalized-inverse quantiles, strict greedy choices and both exact backups. There is no sorry. The proof uses only Lean’s standard axioms, propext, Classical.choice and Quot.sound (axiom listings, build record). The general real-valued theorem is not formalized.

The specified material Huber failure did not appear in the sampled test. All four required comparisons missed the rule for continuing, so I did not run replay/network training. With K=32 and constant steps, Huber’s normalized regret was 0.0043 versus 0.0783 for the scalar learner; the paired difference was −0.0740, with a 95% interval of [−0.0766, −0.0713]. In this comparison Huber did better, not worse.

The general theorem is not Lean-checked or externally peer-reviewed. The finite Lean cycle does not exclude other fixed points; attraction, the arbitrary-K theorem and the delay construction remain paper proofs. The exact verifier separately checks 18 one-state instances, five delay instances and 18 zero-start trajectories (verification record).

The sampled study is tabular and synthetic, with a generative sampler: no exploration, replay or neural network. The family changes with K. Hard projection, pinball and Huber are different operators. Finite runs neither prove convergence nor rule out rare failing seeds, and noisy switches do not prove an exact cycle. The hard-operator counterexample is not evidence of a QR-DQN training failure.