Sure, there’s an analytic solution, but I did something inefficient in Part 1 and used Part 2 as an opportunity to meditate a bit on how to efficiently do binary search in Dusa, made complicated by the fact that there’s no rounding-down division so I can’t calculate midpoints great - the best I can really do is find the power of two that’s between Lo and Hi, and make the midpoint Lo + 2^N, which is still good enough for O(log n).

[Here’s Part 1 on dusa.rocks](https://dusa.rocks/#program=%23 AOC Day 6%2C Part 1 %23 Inputs duration 0 is 7. duration 1 is 15. duration 2 is 30. record 0 is 9. record 1 is 40. record 2 is 200. %23 Computation %23builtin INT_PLUS plus %23builtin INT_MINUS minus %23builtin INT_TIMES times nat N %3A- duration _ is N. nat (minus N 1) %3A- nat N%2C N !%3D 0. lt N M %3A- nat N%2C nat M%2C N < M. possibleDistance Race ButtonDuration is Distance %3A- duration Race is Duration%2C nat ButtonDuration%2C ButtonDuration <%3D Duration%2C Velocity %3D%3D ButtonDuration%2C GoTime %3D%3D minus Duration ButtonDuration%2C Distance %3D%3D times GoTime Velocity. wins Race ButtonDuration is 1 %3A- possibleDistance Race ButtonDuration is Distance%2C record Race is Record%2C Distance > Record. wins Race ButtonDuration is 0 %3A- possibleDistance Race ButtonDuration is Distance%2C record Race is Record%2C Distance <%3D Record. sum Race 0 is 0 %3A- record Race is _. sum Race (plus N 1) is (plus Accum Wins) %3A- sum Race N is Accum%2C wins Race N is Wins. value Race is N %3A- duration Race is D%2C sum Race (plus D 1) is N. goal 0 is 1. goal (plus N 1) is (times Accum V) %3A- goal N is Accum%2C value N is V. aaa_the_answer is N %3A- goal 3 is N.)

Here’s Part 2 on dusa.rocks%20%3A-%0A%20%20%20goal%20SmallestWinning%20LargestWinning.%0A)

Here’s a more concise meditation on doing binary search for the square root in dusa...%20for%20all%20positive%20K%0AintSqRtRange%20K%20Exp%201%20(plus%20K%201)%20%3A-%0A%20%20%20%20needIntSqRt%20K%2C%0A%20%20%20%20floorPow2%20K%20is%20pair%20Exp%20_.%0A%0A%23%20intSqRtRange%20K%20Exp%20Lo%20Hi%20means%3A%0A%23%20%201)%202%5EExp%20%3C%3D%20Hi%20-%20Lo%20%3C%2022%5EExp%0A%23%20%202)%20Lo%5E2%20%3C%3D%20K%20%3C%20Hi%5E2%0A%0A%23%20midpoint%20calculation%3A%20if%20intSqRtRange%20K%20Exp%20Lo%20Hi%2C%20then%0A%23%20the%20midpoint%20Mid%20%3D%20Lo%20%2B%202%5E(Exp%20-%201)%20splits%20the%20range%20sufficiently%0A%23%20well%20into%20a%20smaller%20segment%20%5BLo..Mid)%20where%20the%20exponent%20is%20smaller%2C%20%0A%23%20and%20a%20larger%20segment%20%5BMid..Hi)%20where%20the%20exponent%20may%20be*%20smaller%20or%0A%23%20not.%0AintSqRtRange%20K%20(minus%20Exp%201)%20Lo%20Mid%20%3A-%0A%20%20%20%20intSqRtRange%20K%20Exp%20Lo%20Hi%2C%0A%20%20%20%20Exp%20%3E%200%2C%0A%20%20%20%20pow2%20(minus%20Exp%201)%20is%20N%2C%0A%20%20%20%20Mid%20%3D%3D%20plus%20Lo%20N%2C%0A%20%20%20%20K%20%3C%20times%20Mid%20Mid.%0A%0AintSqRtBigRange%20K%20(minus%20Exp%201)%20Mid%20Hi%20%3A-%0A%20%20%20%20intSqRtRange%20K%20Exp%20Lo%20Hi%2C%0A%20%20%20%20Exp%20%3E%200%2C%0A%20%20%20%20pow2%20(minus%20Exp%201)%20is%20N%2C%0A%20%20%20%20Mid%20%3D%3D%20plus%20Lo%20N%2C%0A%20%20%20%20K%20%3E%3D%20times%20Mid%20Mid.%0A%0A%23%20intSqRtBigRange%20K%20Exp%20Lo%20Hi%20means%3A%0A%23%20%201)%202Exp%20%3C%3D%20Hi%20-%20Lo%20%3C%2042%5EExp%0A%23%20%202)%20Lo%5E2%20%3C%3D%20K%20%3C%20Hi%5E2%0AintSqRtRange%20K%20Exp%20Lo%20Hi%20%3A-%20%20%0A%20%20%20%20intSqRtBigRange%20K%20Exp%20Lo%20Hi%2C%0A%20%20%20%20pow2%20Exp%20is%20N%2C%0A%20%20%20%20minus%20Hi%20Lo%20%3C%20times%202%20N.%0AintSqRtRange%20K%20(plus%20Exp%201)%20Lo%20Hi%20%3A-%0A%20%20%20%20intSqRtBigRange%20K%20Exp%20Lo%20Hi%2C%0A%20%20%20%20pow2%20Exp%20is%20N%2C%0A%20%20%20%20times%202%20N%20%3C%3D%20minus%20Hi%20Lo.%0A%0A%0AintSqRt%20K%20is%20N%20%3A-%20intSqRtRange%20K%200%20N%20_.%0A%0AneedIntSqRt%201.%0AneedIntSqRt%202.%0AneedIntSqRt%203.%0AneedIntSqRt%204.%0AneedIntSqRt%205.%0AneedIntSqRt%206.%0AneedIntSqRt%207.%0AneedIntSqRt%208.%0AneedIntSqRt%209.%0AneedIntSqRt%2010.%0AneedIntSqRt%2011.%0AneedIntSqRt%2012.%0AneedIntSqRt%2013.%0AneedIntSqRt%2025.%0AneedIntSqRt%209999.%0A%0A%0A) without access to division, which changes the nature of logarithmic binary search a bit. Binary search is famously difficult, but I have medium-high confidence that this works the way it is supposed to for the reasons it is supposed to.