Hi all and sorry for the bad English!
I'm implementing Bombelli's algorithm for a big-integer library, and for optimization I'd need to prove some details regarding the values that certain variables can assume or not.
First of all, here is my algorithm formalization attempt:
What I should prove (or even disprove) is:
a) [imath]a_i[/imath] has at most one more digit than [imath]2bR_{i-1} \ [/imath];
b) for [imath]r_i \neq 0[/imath] the difference [imath]a_i-c_i[/imath] has at most the same number of digits as [imath]c_i \ [/imath];
c) for [imath]i>1[/imath] when [imath]a_i[/imath] has one more digit than [imath]2bR_{i-1} \ [/imath], let [imath]A[/imath] be the number consisting of the first two digits of [imath]a_i[/imath] and [imath]B[/imath] be the number consisting of the first digit of [imath]2bR_{i-1} \ [/imath], then [imath]\frac{A}{B+1}<b \ [/imath].
About a), the numerical example above demonstrates that [imath]a_i[/imath] can have one more digit than [imath]2bR_{i-1} \ [/imath], so now we need to show that it cannot have [imath]2[/imath] (or more) more. Assuming that [imath]a_i[/imath] has [imath]2[/imath] more digits than [imath]2bR_{i-1} \ [/imath], we can set [imath]a_i \geq b^{k+1}[/imath] and [imath]2bR_{i-1} \leq b^k-b[/imath], that is, [imath]a_i[/imath] is greater than or equal to the smallest number of [imath]k+2[/imath] digits and [imath]2bR_{i-1}[/imath] is less than or equal to the largest number of [imath]k[/imath] digits ending in [imath]0[/imath]; in this case 4) would also be verified for [imath]r_i=b \ [/imath], in fact [math]c_i=r_i(2bR_{i-1}+r_i) \leq b(b^k-b+b)=b^{k+1} \leq a_i[/math] but since it must be [imath]r_i<b \ [/imath], we can conclude that [imath]a_1[/imath] will have at most one more digit than [imath]2bR_{i-1} \ [/imath].
About b), obviously the problem only arises when [imath]a_i[/imath] has more digits than [imath]c_i \ [/imath]. I would have thought of distinguishing the case [imath]i=1[/imath] from the case i>1, but in any case I would only be able to prove the first case.
About c), to maximize [imath]\frac{A}{B+1}[/imath] we set [imath]B=1[/imath] (we can obtain it for example for [imath]r_1 \geq \Bigl \lceil \frac{b}{2} \Bigr \rceil[/imath]), then we get that [imath]\frac{A}{1+1}<b \Rightarrow A<2b \ [/imath] , that is, the first digit of [imath]A[/imath] should be [imath]1[/imath], but i don't know how to prove it.
So in the end I ask whether my proof of a) is correct and whether it can be done better, and how to prove (or even disprove) b) and c).
I'm implementing Bombelli's algorithm for a big-integer library, and for optimization I'd need to prove some details regarding the values that certain variables can assume or not.
First of all, here is my algorithm formalization attempt:
Below we can see that [imath]72908835647=270016^2+195391 \ [/imath]:
What I should prove (or even disprove) is:
a) [imath]a_i[/imath] has at most one more digit than [imath]2bR_{i-1} \ [/imath];
b) for [imath]r_i \neq 0[/imath] the difference [imath]a_i-c_i[/imath] has at most the same number of digits as [imath]c_i \ [/imath];
c) for [imath]i>1[/imath] when [imath]a_i[/imath] has one more digit than [imath]2bR_{i-1} \ [/imath], let [imath]A[/imath] be the number consisting of the first two digits of [imath]a_i[/imath] and [imath]B[/imath] be the number consisting of the first digit of [imath]2bR_{i-1} \ [/imath], then [imath]\frac{A}{B+1}<b \ [/imath].
About a), the numerical example above demonstrates that [imath]a_i[/imath] can have one more digit than [imath]2bR_{i-1} \ [/imath], so now we need to show that it cannot have [imath]2[/imath] (or more) more. Assuming that [imath]a_i[/imath] has [imath]2[/imath] more digits than [imath]2bR_{i-1} \ [/imath], we can set [imath]a_i \geq b^{k+1}[/imath] and [imath]2bR_{i-1} \leq b^k-b[/imath], that is, [imath]a_i[/imath] is greater than or equal to the smallest number of [imath]k+2[/imath] digits and [imath]2bR_{i-1}[/imath] is less than or equal to the largest number of [imath]k[/imath] digits ending in [imath]0[/imath]; in this case 4) would also be verified for [imath]r_i=b \ [/imath], in fact [math]c_i=r_i(2bR_{i-1}+r_i) \leq b(b^k-b+b)=b^{k+1} \leq a_i[/math] but since it must be [imath]r_i<b \ [/imath], we can conclude that [imath]a_1[/imath] will have at most one more digit than [imath]2bR_{i-1} \ [/imath].
About b), obviously the problem only arises when [imath]a_i[/imath] has more digits than [imath]c_i \ [/imath]. I would have thought of distinguishing the case [imath]i=1[/imath] from the case i>1, but in any case I would only be able to prove the first case.
About c), to maximize [imath]\frac{A}{B+1}[/imath] we set [imath]B=1[/imath] (we can obtain it for example for [imath]r_1 \geq \Bigl \lceil \frac{b}{2} \Bigr \rceil[/imath]), then we get that [imath]\frac{A}{1+1}<b \Rightarrow A<2b \ [/imath] , that is, the first digit of [imath]A[/imath] should be [imath]1[/imath], but i don't know how to prove it.
So in the end I ask whether my proof of a) is correct and whether it can be done better, and how to prove (or even disprove) b) and c).
