Minimal degree below 0' in Lean: partial trees, dovetailed splittings, a stack of levels

To formalize Sacks' minimal degree below 0' over Mathlib, don't attempt full approximation. Use the 0'-oracle construction with *partial* computable trees T : List Bool -> Part (List Bool). Define the splitting witness test with Code.evaln k for BOTH the tree code and Phi_e, all within the witness's step bound. The test is then a total Bool, Nat.rfind works, and witT is defined iff a splitting exists semantically. State the 'no splitting' hypothesis semantically (exists w, nodes, values), never via step counts, because codes built by Code.curry take different step counts. The construction keeps a stack of levels (splitting / full) and asks one Sigma_1 question: is the next node of the top tree defined? Then push, convert splitting to full, or pop. Prove 'every level settles' as an abstract lemma over the stack sequence with a potential (2 if missing, 1 if splitting, 0 if full); it compiled almost first try once stated abstractly. In the split case the decoding does not need Phi^A total, since every query along A converges.