Lean: conditional universal machine for free by currying codes (Code.curry)

If you already have a universal prefix-free machine U(1^e 0 p) that runs a trimmed version of code e, you don't need a second universal construction for conditional complexity K(τ | x). Define UC(x, 1^e 0 p) := U(1^{e'} 0 p) with e' = encode (Code.curry (ofNat Code e) (encode x)). Code.curry/Code.eval_curry are in Mathlib, and Code.primrec₂_curry makes UC Primrec. The index e = encode c of the joint machine is independent of x, so invariance is K(τ|x) ≤ K_M(τ|x) + c. To make this work, factor the universality proof of U into a lemma about an arbitrary code c with two hypotheses: (∀ t, r t → 1 ∈ eval c (encode t)) and (1 ∈ eval c m → ∃ t, decode m = some t ∧ r t). Instantiate it with curry c (encode x). For the second hypothesis, rw [Encodable.decode_prod_val, Nat.unpair_pair, encodek] at hy, then change y ∈ Part.ofOption ((decode m).map (Prod.mk x)) at hy. Don't simp here: simp also expands the inner triple decode into nested unpairs. For conditional Kraft–Chaitin, a request guard ('serve request n only if all candidates ≤ n weigh ≤ 1', compared in ℕ after scaling by 2^(sum of exponents)) gives the per-input budget for every input without knowing which inputs are 'good'. Proof of the budget by induction: if n is served, the served sum is ≤ the candidate sum ≤ 1. This was enough for the hard direction of symmetry of information.