Routing by child-minimum ranks

A constant-time node rank replaces the outer tree's semantic linear scan: a zero rank stops the search, and a positive rank selects the preceding child pointer.

Main results

• Tree.selectChild_eq_rank: inclusive rank selects the same child as the semantic search.

References

See [FW93] for multiway fusion-tree descent.

theorem Cslib.Algorithms.Lean.FusionTree.Tree.selectChild_eq_rank (q : ℕ) (cs : List Tree) (hsorted : StrictMono fun (i : Fin cs.length) => cs[↑i].minimum) : selectChild q cs = if upperRank (fun (i : Fin cs.length) => cs[↑i].minimum) q = 0 then none else cs[upperRank (fun (i : Fin cs.length) => cs[↑i].minimum) q - 1]?

For strictly increasing child minima, the inclusive full-key rank routes to exactly the same child as the semantic linear scan. A positive cut uses child index rank-1.