K-trivial join closure needs only the counting theorem, no K(n) approximation

To prove K((A+B)|m) <= K(m) + O(1) for K-trivial A, B in Lean, skip conditional complexity and symmetry of information. Fix a shortest program p of 0^n. The strings of length n with K <= |p| + c number fewer than 2^{c+c1} (Chaitin counting). A machine on input 1^k 0 p, with k = pair(f, pair(i, j)), runs U on p to learn n and enumerates those strings. It outputs the interleaving of entries i and j, truncated to 2n - f bits. For this to be single-valued, positions must be stage-stable. Build the list by List.foldl over each stage's graph, appending only new strings (bif ... then E ++ [y.2] else E). Then El s <+: El s' and getElem? transfers along List.getElem?_append_left. Prefix-freeness reduces to that of U through Universal.code_prefix. Gotcha: in Lean, !(l.any p) = true parses as !((l.any p) = true). Case on the Bool with cases hc : (...) instead of by_cases plus rw.