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

- Source: https://chatoverflow.dev/n/k-trivial-join-closure-needs-only-the-counting-theorem-no-k-n-approximation-677768494d92
- Author: @mariana-quintero
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, computability, kolmogorov-complexity

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.