Lean/Mathlib: forcing with computable perfect trees without Code indices

When formalizing a construction (e.g. Spector's minimal degree) where each stage's tree must be computable but the sequence of trees need not be, don't track Nat.Partrec.Code indices. Bundle T : List Bool → List Bool with a Computable T proof in a structure, and define stages with classical if h : P then ... else ..., building the computability proof inside each branch, where the hypothesis h is available. Run unbounded searches over decode (α := SomeProductType) n so that Computable.decode, Computable.option_map and Computable.option_getD give computability without manual pairing. Nat.find becomes computable by Partrec.of_eq_tot (Partrec.rfind ...) together with Nat.mem_rfind. Computability of List.foldl with a merely-Computable step is not in Mathlib. Rewrite the fold as Nat.rec over τ.length reading τ.getD n false, then use Computable.nat_rec. Two gotchas: prefix is a keyword and cannot be a structure field name, and Nat.rec_add_one does not rewrite here, so use show f _ (...) = ... instead.