Lean: coding theorem K ≤ -log m + c via threshold requests indexed by pairs

To formalize Levin's coding theorem on top of a Kraft–Chaitin-for-K lemma (requests rq : ℕ → Option (σ, length), computable, partial weight sums ≤ 1), present the c.e. semimeasure as computable *pieces* ws : ℕ → Option (List Bool × ℕ) (piece (σ,d) adds 2^-d to σ). Request index r = ⟨n,k⟩ (Nat.unpair): emit (σ_n, k+1) iff piece n makes mass(σ_n) cross 2^-k, i.e. cross(n+1) ∧ ¬cross(n). Pairing lets one piece cross several thresholds without computing a minimum level. Weight proof: (1) Σ_{r<R} F(unpair r) ≤ Σ_{n<R}Σ_{k<R} F (sum_image with injectivity from Nat.pair_unpair, then subset of range×range). (2) Rewrite each stage term as Σ_{σ∈S} h n σ k with Finset.sum_eq_single (h vanishes for σ ≠ σ_n because the mass doesn't change), swap sums, telescope in n to [2^-k < mass N σ]·2^-(k+1). (3) Σ_k [2^-k < x] 2^-(k+1) ≤ x, by induction with the invariant ≤ max 0 (x − 2^-K). For decidability, compare in ℕ after scaling by 2^M with M = k + (sum of all exponents so far): a crude common denominator, so there are no max computations. Gotchas: simp turns (1/2)^k into (2^k)⁻¹ and breaks the if-conditions, so use simp only [h1, h2, ↓reduceIte]. simp also unfolds encode (a,b,c) into Nat.pair, so rw with a pieces_encode lemma instead. Finset.sum_image needs an explicit (f := ...) when the summand is f (g n). For algorithmic probability of a machine, index pieces by decode₂ (not decode) of (stage, p, σ) and keep only the first stage, so each program is counted once.