Theorem on Lucas numbers modulo 2^b

[David Sparks]

The comments in mpz/lucnum_ui.c mention some unproved assertions
about Lucas numbers mod 2^b, and in particular when
L[2n] = L[n]^2 - 2 can be expected to generate a borrow.

I have what I think is a useful proof on the subject.  I'm not
very experienced at writing proofs, so I hope the following is clear.

We want to know when L[2n] = L[n]^2 - 2^(-1)^n might generate
a carry or borrow out of the lsword.

There are two subcases.  If n is odd, we add +2, and a carry
will be generated if L[2n] == 0 or 1 (mod 2^b).  These are
both impossible by Lemmas 1C and 1A below.

If n is even, then a borrow will be generated if L[2n] == -1 or -2
(mod 2^b).  L[2n] == -2 occurs only if L[n] == 0 (mod 2^b), which
is impossible by Lemma 1C below.  L[2n] == -1 can occur, but not
before L[2^(b-1)]; see the theorem below.


Theorem: L[2n] == -1 (mod 2^(b+1)) iff 2n == +/- 2^b mod 3*2^b.

We start with two lemmas:

Lemma 1: L[n] mod 8 is periodic modulo 12, with residues
L[n] == {2, 1, 3, 4, 7, 3, 2, 5, 7, 4, 3, 7}[n%12] (mod 8).
Proof: By enumeration.  Once two consecutive residues repeat,
the sequence is periodic.
Corollary A: L[k] == 1 (mod 4) iff k == 1 (mod 6).
Corollary B: L[4k+2] == 2 or 3 (mod 8).
Corollary C: L[k] != 0 (mod 8)

Lemma 2: For odd x & y, x^2 == y^2 (mod 2^b) iff x == +/-y (mod 2^(b-1)).
The right => left case is a trivial matter of expansion.
y == +/-x mod 2^(b-1) iff y = k*2^(b-1) +/- x.
y^2 = (k*2^(b-1) +/- x)^2 = (k*2^(2b-2) +/- k^2^b + x^2) == x^2 (mod 2^b).

For left => right, write this as
(x+y)*(x-y) == 0 (mod 2^b)
then consider two cases:
1) x == y (mod 4).  Thus, (x+y) == 2 (mod 4), and (x-y) must contain
all the other factors of 2, at least b-1 of them, so x == y mod 2^(b-1).
2) x == -y (mod 4).  Thus, (x-y) == 2 (mod 4), and (x+y) must contain
all the other factors of 2, at least b-1 of them, so x == -y mod 2^(b-1).


Main theorem: L[2n] == -1 (mod 2^(b+1)) iff 2n == +/- 2^b mod 3*2^b.

The base cases b = 0, 1, 2 are established by Lemma 1.
L[n] % 2 = {0, 1, 1}^*
L[n] % 4 = {2, 1, 3, 0, 3, 3}^*.  L[5] isn't an even index.
L[n] % 8 = {2, 1, 3, 4, 7, 3, 2, 5, 7, 4, 3, 7}^*.  L[11] isn't an even index.

The right => left direction is a simple application of Lemma 2.
If (by the induction hypothesis) We know that L[2n] == -1 (mod 2^(b+1))
when 2n == +/-2^b mod 3*2^b, then 4n == +/-2^(b+1) (mod 3*2^(b+1)) and
L[4n] = L[2n]^2 - 2 == 1-2 = -1 modulo 2^(b+2).

The left => right case requires proving that this congruence
does not hold for any other n, and has two subcases depending
on the parity of the n under consideration.

If n is odd, then 2n = 4k+2 and, by Lemma 1B, 
L[2n] = L[4k+2] != -1 (mod 8), so L[2n] != -1 (mod 2^(b+1))
for any b >= 2.

Therefore, only even n is possible, implying that (-1)^n = 1 and
L[2n] = L[n]^2 - 2, so the left-hand side will hold (by Lemma 2)
iff L[n] == +/-1 (mod 2^b).

By Lemma 1A, L[n] == +1 (mod 2^b) is impossible for even n.
Therefore, L[n] == -1 (mod 2^b).  By the induction hypothesis,
this is true only if n == +/-2^(b-1) (mod 3*2^(b-1)), and thus
the right-hand side is proved.