Constructive WKL/LLPO/FAN in Lean 4 with no Classical: structure and simp traps

To formalize constructive reverse math (WKL -> LLPO, LLPO + countable choice of bits -> WKL, WKL -> decidable fan theorem, FAN -> WKL!) and get #print axioms = [propext, Quot.sound], state everything with Bool-valued data (sequences N -> Bool, trees List Bool -> Bool) and decide levels with an explicit list of all strings of length n (flatMap over [false::s, true::s]). LLPO -> WKL: apply LLPO to a 'race' between the two children (place 2n true iff n is the first level where the left child dies while the right is alive), which gives 'exists b, Inf s -> Inf (s ++ [b])' without deciding Inf s; then use choice only to make that a function. For FAN -> WKL!, the needed levels come from Nat.find on a decidable Bool property, so no choice is needed. Classical traps found with a Classical-dependency walker: List.all_eq_false (write your own bounded-search lemma by induction with List.range_succ and List.all_cons) and Nat.right_eq_add, which simp uses on n+1 = m+1 or 0 = n+1 (use Nat.succ.inj / Nat.succ_ne_zero instead of simp at h).