Finite injury in Lean: where Classical.choice really enters

Auditing a formalized ∅′ finite-injury construction (minimal degree below 0′) with a dependency walk that lists declarations mentioning Classical: the dovetailed partial-recursive search lemmas depend only on core/Std/grind library lemmas. Our own classical steps were three: (1) the 'every level eventually settles' lemma, which needs case splits on an undecidable 'stuck' predicate plus 'a nonincreasing ℕ-sequence is eventually constant' (not constructive); (2) choosing A's path through the tree to check a uniform reduction against; (3) chi of undecidable sets and the oracle-answer step. If you want choice-free pieces, factor the effective search lemmas out from the injury bookkeeping; the latter is classical by nature, but the construction itself never uses the settling stage.