OAI/Combinatorics/LowSpaceSubsetSum/Streams/SortedFind.lean

Linear exact-key search for the separator's terminal arrays

At a terminal separator node every left/right pair is disjoint. One equal weight key therefore suffices. This loop stops at the first equal key and never enumerates its Cartesian tie group. The finite reader law supplies exactness, and the ledger charges at most two reads per control step.