OAI/Combinatorics/LowSpaceSubsetSum/Search/MainGuard.lean

An integer main-branch guard and the polynomial-bit promise

The guard uses the binary ceiling logarithm. It implies the manuscript's real logarithmic guard and eventually passes for every fixed polynomial bound on input bit length. Its stricter rounding only changes the fallback on a finite initial range for each polynomial-bit promise.