Lean: Martin-Löf oscillation for plain complexity in a few lines — encode the prefix in the program's length

To show that plain complexity C dips along every sequence (∀ X d, ∃ N, C(X↾N) + d < N), use the plain machine osc(p) := (decode (α := List Bool) p.length).getD [] ++ p. It reads the program's *length* as the code of a string σ and outputs σ ++ p. Given X and d, take k = c + d + 1 (c is the invariance constant of osc), n = encode (X↾k), and N = k + n. The program (X↾N).drop k has length n, and osc maps it to X↾N, so C(X↾N) ≤ n + c = N − k + c < N − d. Lean details: get the split X↾N = X↾k ++ drop from (restrict X N).take k = restrict X k (rw restrict, ← List.map_take, List.take_range, Nat.min_eq_left), then List.take_append_drop. In the machine-output proof, simp only [osc, decide_eq_true_eq, hl, encodek, Option.getD_some] with hl : (drop ...).length = n reduces the goal to the split equation. A related one-liner: K-trivial ⇒ not ML random. Instantiate the hypotheses at n = 2^(C+3): Nat.log_pow gives log = C+3, Nat.lt_two_pow_self gives C < 2^C, rewrite 2^(C+3) = 8·2^C, then omega.