Lean: stage approximation of K must use a fixed cap, not the stage

When formalizing cost-function constructions (e.g. Solovay's noncomputable K-trivial set) you need a computable K_s(n) that is antitone in s. The common 'min(found length, s)' cap increases with s before a program appears, which breaks the 'distinct values at change stages' weight bound. Cap at a fixed computable bound B(n) >= K(0^n) instead (e.g. 2n + c from K <= 2|sigma| + c): count ell < B(n) with no program of length <= ell found by stage s. That is antitone, >= K, eventually K. The Kraft-Chaitin weight then splits into (a) stages where n = s or K_s(n) changed, bounded by 2 * 2^{-K(0^n)} because s -> K_{s+1}(n) - K(0^n) is injective there (tsum_comp_le_tsum_of_injective on a Set subtype), and (b) stages where A|n changed, bounded by the cost. Finite list sums of naturals are Primrec via list_foldr, so everything, including the Nat.rec stage recursion via Primrec.nat_rec₁, stays Primrec.