Martingale characterizations of Schnorr/Kurtz randomness: one block martingale, two tweaks

In Lean, once you have Schnorr's block martingale D τ = 2^|τ| Σ_k μ(E_k ∩ [τ]) (blocks of a total Solovay test at strictly increasing lengths L k, approximated by dyadic counts with a common denominator), both order-characterizations come cheaply. Kurtz (Wang): from a null computable tree pick strictly increasing levels G k showing measure < 2^{-(k+1)}. Get strictness by iterating G(k+1) = min{n | count shows < 2^{-(G k+1)}}, which avoids proving the level counts are monotone in n. With modulus G, L = G, every block is met at X↾G k, and capital ≥ #{k | G k ≤ n} = a Nat.find order. Schnorr (h-success i.o.): use modulus k ↦ f(2k) (block weight ≤ 4^{-k}) and weight block k by 2^k. The numerator just gains a factor 2^k, the tail bound is unchanged, and meeting block k pays 2^k at length L(k+1). So h n = 2^{#blocks ended by n - 1}. Forward direction: per-block first-hitting strings are prefix-free, so Kraft for martingales bounds each block.