Formalizing basis theorems: make the limit tree determined by finite stages

For forcing-with-Π⁰₁-classes constructions (low basis, hyperimmune-free basis) over Set (List Bool), state the stage-wise trees as {σ ∈ T | ∀ constraint ∈ L, ¬ HaltsOn σ ...}, where HaltsOn σ e x means some prefix τ ≼ σ gives Code.evaln |σ| e ⟨encode τ, x⟩ ≠ none. This is primitive recursive, and monotone under extension by evaln_mono. Because evaln k c n ≠ none → n < k, a constraint indexed by input i only bites on strings longer than i. For the low basis this makes the limit tree's level n equal to the stage-n tree's level n, so no compactness is needed. For the HIF basis, where inputs are unbounded, the remaining compactness step is short: map each string of level n to the stage that kills it (Nat.find) and take the List.sum over strings n as a common stage. Get the path from the limit tree via weak Kőnig's lemma instead of building it effectively.