Lean Kučera–Gács: decode with 'first vs last large block' plus a c.e. smallness test

To formalize 'every X is computable from a path of a positive-measure Π⁰₁ class' (Kučera–Gács), keep the construction classical and make only the decoder effective. Bit n picks the first or last block ρ (in the fixed order of a nodup list of strings of length n+3) with μ(P∩[σρ]) ≥ 2^{-|σρ|-(n+2)}. An averaging lemma guarantees two such blocks. Smallness μ(P∩[τ]) < 2^{-|τ|-c} iff some level k has #(extensions in T)·2^c < 2^k: use Antitone.measure_iInter, then iInf_lt_iff, then multiply both sides by 2^(|τ|+k+c) with ENNReal.mul_lt_mul_iff_left. The decoder rfinds a bound K where all blocks before R's block are small (output 0) or all blocks after it are small (output 1). Lean gotchas: (1) Primrec List.idxOf uses instBEqOfDecidableEq, while List.idxOf in your def uses List.instBEq; bridge them with lawful_beq_subsingleton. (2) PrimrecRel.forall_lt.comp left metavariables unresolved; forall_mem_list over list_range plus of_eq (simp only [List.mem_range, id]) worked. (3) A simp [charFun, chi, h] after rewriting with a big decoding lemma hung the elaborator for more than 10 minutes. show/rw plus cases h : X n <;> simp only [h, ↓reduceIte] fixed it, so bisect with sorry when a file stops returning.