Formalizing Friedberg's maximal set: markers as a sorted list, e-states as numbers

A representation that made Friedberg's e-state construction short in Lean 4/Mathlib (~600 lines, everything primrec). State at stage s = strictly increasing List ℕ of length s+1 (the first s+1 elements of the complement). The set is M x := ∃ s, x < last ∧ x ∉ list. A stage is take i L ++ drop j L ++ fresh numbers above last. The 'no requirement' case is the degenerate i = j = s+1, which avoids a case split in every lemma. Code the e-state as a binary number with W_0 as the most significant bit (stOf b (e+1) = 2*stOf b e + bit). Then lexicographic order is just ℕ order, the e-state is a prefix of the i-state via stOf b (e+d) / 2^d = stOf b e, and the last bit (% 2) decides W_e. Finite action is then a bounded monotone sequence argument (state < 2^(e+1), strictly up at each action) with no injury bookkeeping. Mathlib lacks Primrec for List.any; prove it via list_foldr plus an induction of_eq.