Lean: a Π⁰₁ class of random sequences without a universal ML test (trim + Markov)

To feed basis theorems (low, hyperimmune-free, PA) with a computable tree whose paths are all random (Solovay tests: c.e. string sets with finite weight Σ 2^{-|σ|}), you don't need to formalize universal Martin-Löf tests. (1) Trim the e-th c.e. set: accept σ iff at some stage s where σ is enumerated, the scaled stage weight Σ 2^{s-|σ|} over the stage-s finset is ≤ 2^s. Computing it in ℕ keeps it primrec; |σ| ≤ encode σ < s by Encodable.length_le_encode + Code.evaln_bound. A finite subset lies inside the stage of its latest element, so the trimmed set has weight ≤ 1. Every test agrees with some trimmed set on long strings: take a finite weight-tail cut from ENNReal.tendsto_tsum_compl_atTop_zero. (2) Tree: keep τ while for every e < |τ| fewer than 2^(e+2) prefixes of τ are trimmed-in by stage |τ|. (3) Measure: N_e X = ∑' σ, (cyl σ).indicator 1 X has lintegral ≤ 1 (lintegral_tsum + lintegral_indicator_one), so mul_meas_ge_le_lintegral₀ gives μ{N_e ≥ 2^(e+2)} ≤ 2^-(e+2). Summing gives non-paths ≤ 1/2, so the tree is infinite. Primrec gotchas: there is no Primrec.nat_pow (use Primrec₂.unpaired'.1 Nat.Primrec.pow). Define counts with Finset.card and convert to List.filter length by simp [Finset.card, Multiset.range, Multiset.filter_coe].