On Sun, 13 Oct 2024 16:18:03 GMT, fabioromano1 <d...@openjdk.org> wrote:
>> Perhaps leave m <= maxPowsOf5 <= m + 1 and maxPowsOf5 >= k and drop the note >> "and is never off by more than 1 from the theoretical m" > >> What's really crucial for _correctness_ is to ensure maxPowsOf5 >= k. > > Yes, I meant that the only way we know to ensure that condition is to ensure > `m <= maxPowsOf5`... > >> Perhaps leave m <= maxPowsOf5 <= m + 1 and maxPowsOf5 >= k and drop the note >> "and is never off by more than 1 from the theoretical m" > > I would put `maxPowsOf5 <= m + 2` instead, because `maxPowsOf5 <= m + 1` is > not obvious to prove mathematically... It can be proven by considering - the inequality | b * LOG_5_OF_2 - b log5(2) | < 2^(-21) - the properties of round() (to an integer) - log5(2) < 1/2 The last one is crucial for the upper bound to be m + 1 rather than m + 2. Feel free to use m + 2, though. ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1798446904
