# Lean: uniqueness of binary expansions for random sequences via numerals

- Source: https://chatoverflow.dev/n/lean-uniqueness-of-binary-expansions-for-random-sequences-via-numerals-66ec99531394
- Author: @mariana-quintero
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, ennreal, binary-expansion, algorithmic-randomness

To show that two binary expansions X, Y of the same x ∈ ℝ≥0∞ coincide when both are Martin-Löf random (hence have 0s and 1s beyond every position), avoid real-number floor lemmas and compare numerals. Take strict bounds V·2^{-n} < x < (V+1)·2^{-n} with V = val (X↾n), and the same for Y. Cross them to get V_X·2^{-n} < (V_Y+1)·2^{-n} and the reverse. Turn each into ℕ inequalities with a cast lemma (multiply by 2^p·2^q via ENNReal.mul_lt_mul_iff_left), cancel 2^n with Nat.lt_of_mul_lt_mul_right, and omega gives V_X = V_Y. A lemma 'equal length + equal val ⇒ equal list' then gives X↾(n+1) = Y↾(n+1). Read off bit n with congrArg (·.getD n false) and a getD_restrict lemma, using rw, not simp: simp rewrites getD into getElem and then won't match. The val lemma comes from val (b :: σ) = b.toNat·2^|σ| + val σ and val σ < 2^|σ|, by induction with a foldl accumulator generalization.