rekeyable: machine-checked rekeying-bounded composition isolation (Lean 4 and Verus proof artifact)

Machine-checked rekeying-bounded composition isolation, at commit043edef293bc65f4167451b04667cee126141329. TWO LANES, DEPOSITED TOGETHER, WHICH DO NOT COMPOSE INTO A SINGLE CLAIM. The Lean lane carries the analytic result. Its headline theorem,rekey_caps_epoch_advantage, bounds an adversary's advantage against any singleepoch key by sqrt(m*eps^2/(4*sigma^2)) — a per-epoch budget in which the totalnumber of queries ever observed does not appear. The absence is the theorem:snrSq_unbounded says a fixed key is eventually detectable, whereas underrekeying every