On a problem attributed to T. Gowers

In a talk at Isaac Newton Institute during the Big Proofs seminar, Joe Korneli referred to a problem that he attributes to T. Gowers

What is the 500th decimal of $\displaystyle (\sqrt{2} + \sqrt{3})^{2012}$ ?

He describes how mathematics are discovered, what kind of trials and discussions may happen. It is not the point here, since I already know the answer from reading that page and attending that talk. Still, I would like to see how easy it is to formalize the final result.

Here is the final explanation, when considering $\displaystyle (\sqrt{3} + \sqrt{2})^{2n}$ and $\displaystyle(\sqrt{3}-\sqrt{2})^{2n}$ as sums, they contains the same terms upto potentially different signs. When regrouping these terms and cancelling the cases where they have different signs, one obtains the following equality

$\displaystyle (\sqrt{2} + \sqrt{3})^{2n}+(\sqrt{3} - \sqrt{2})^{2n} =\sum_{i=0}^{n} \left(\begin{array}{c}2i\\2n\end{array}\right)2^i 3^{n - i}$

The right-hand side of the equality is an integer, and the second term of the sum in the left-hand side is a high power of a number between 0 and 1, when n is high. This high power of a small number is small enough that all digits up to the 500th are nines.

Now I wish to write a formal proof of this funny result. Obviously, I will need to be more precise in the statement: show that $\displaystyle (\sqrt{3} - \sqrt{2})^{2012}$ is smaller than $\displaystyle 10^{500}$ . I will also need to manipulate the binomial formulas and reason about big sums. For this reason, I choose to work directly using the mathematical components library.

I have an instance of coq where enough all the mathematical components are installed and I start my development in the following manner:

From mathcomp Require Import all_ssreflect all_algebra all_field.
Import Num Num.ExtraDef.
Import Num.Theory GRing.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicits Defensive.

Section the_exercise.

Variable R : rcfType.

Open Scope ring_scope.

Computing numerical bounds

I first want to compute an upper bound of $\displaystyle (\sqrt{3} - \sqrt{2}) ^ {2012}$ and therefore I need a lower bound of $\displaystyle \sqrt{2}$ . I would have liked to do this automatically,
for instance using the interval tactic, but making interval and mathematical components to work together requires too much sweat, so here is my first proof:

Lemma sqrt2_lb : 7%:R / 5%:R < sqrtr 2%:R :> R.
Proof.
rewrite ltr_pdivr_mulr; last by rewrite ltr0n.
have -> : 7%:R = sqrtr 49%:R :> R.
rewrite (_ : 49%:R = 7%:R ^+2); last first.
by rewrite expr2 -natrM.
by rewrite sqrtr_sqr; apply/eqP; rewrite eq_sym eqr_norm_id ler0n.
have -> : 5%:R = sqrtr 25%:R :> R.
rewrite (_ : 25%:R = 5%:R ^+2); last first.
by rewrite expr2 -natrM.
by rewrite sqrtr_sqr; apply/eqP; rewrite eq_sym eqr_norm_id ler0n.
rewrite -sqrtrM; last by rewrite ler0n.
by rewrite -natrM ltr_sqrt ?ltr_nat ?ltr0n.
Qed.

Now obviously, I can do a similar proof to obtain an upper bound of $\displaystyle \sqrt{3}$ . However, I see a lot of duplication in this text,
so I choose to give myself an extra lemma:

Lemma sqrtrn_sqr n : n%:R = sqrtr((n * n)%:R) :> R.
Proof.
rewrite natrM -expr2 sqrtr_sqr; apply/eqP.
by rewrite eq_sym eqr_norm_id; apply:ler0n.
Qed.

Now, my first proof can be rewritten as follows:

Lemma sqrt2_lb : 7%:R / 5%:R < sqrtr 2%:R :> R.
Proof.
rewrite ltr_pdivr_mulr; last by rewrite ltr0n.
rewrite [7%:R]sqrtrn_sqr [5%:R]sqrtrn_sqr -sqrtrM; last by apply:ler0n.
by rewrite -!natrM ltr_sqrt ?ltr0n ?ltr_nat.
Qed.

For the upper bound of I choose $\frac{26}{15}$ , because it gives 1/3 as an upper bound for the difference.

Lemma sqrt3_ub : sqrt 3%:R < 26%:R / 15%:R :> R.
Proof.
rewrite ltr_pdivl_mulr; last by rewrite ltr0n.
rewrite [26%:R]sqrtrn_sqr [15%:R]sqrtrn_sqr -sqrtrM; last by apply ler0n.
by rewrite -!natrM ltr_sqrt ?ltr0n ?ltr_nat.
Qed.

This is too complicated for my taste, but the reason for working with mathematical components is that I want to benefit from the work already done for binomial formulas and big sums. I will complete this post later on this topic.

When I come back to this post, August 31st 2017, I can benefit from the comments of Cyril and Laurent and prove that a high power of $\displaystyle \frac{1}{3}$ is small enough.

Lemma magnitude : 10%:R ^+ 910 < 3%:R ^+ 2012 :>R.
Proof.
have st2 : 10%:R ^+ 5 <= 3%:R ^+ 11 :> R.
by rewrite -!natrX ler_nat.
rewrite -[X in 10%:R ^+ X]/(5 * 182)%N exprM.
have st3 : 10%:R ^+ 5 ^+ 182 <= 3 %:R ^+ 11 ^+ 182 :> R.
by apply: ler_expn2r => //; apply/exprn_ge0/ler0n.
apply: (ler_lt_trans st3).
by rewrite -exprM ltr_eexpn2l ?(ltr_nat _ 1).
Qed.

A few comments on this proof. First, this lemma could be used to show that all digits up to the 910th are nines. Second, the real mathematical way to compute the number of digits that are nines would be to compute $\frac{2012 \ln 3}{\ln 10}\geq959$ , but the Mathematical Components library does not cover the logarithm function. Third, here we instead first compare $10^5$ and $3^{11}$ and then scale the ratio $\frac{11}{5} \times 2012 \geq 910$ .

The binomial sums

I now want to compute the big sum that results from adding the power of a sum of two numbers and the difference of these numbers. The lemma statement has the following shape.

Lemma main_trick (a b : R) (n : nat) :
(a + b) ^+ (2 * n) + (a - b) ^+ (2 * n) =
2%:R *
\sum_(i < n.+1) a ^+ (2* n - 2 * i) * b ^+ (2 * i) *+ 'C(2 * n, 2 * i).
Proof.

The ssralg library provides two theorems to compute the powers of sums and differences, named exprBn (for subtraction) and exprDn (for addition). In the bigop library, there is a theorem for conflating two sums with the same ranges into a single sum, called big_split. We use these for our first step.

set lhs := (LHS).
have step0 : lhs = 
    \sum_(i < (2 * n).+1) (a ^+ (2 * n - i) * b ^+ i *+ 'C(2 * n, i) +
           (-1) ^+ i * a ^+ (2 * n - i) * b ^+ i *+ 'C(2 * n, i)).
  by rewrite /lhs exprBn exprDn -big_split /=.

We want to decompose this sum in two different sums, one that collects all the indices where the value cancels to 0 (the odd indices) and the other meaningful one. We prove that the first sum is 0.

set fst_term := \sum_(i < (2 * n).+1 | odd i)
     (a ^+ (2 * n - i) * b ^+ i *+ 'C(2 * n, i) +
      (-1) ^+ i * a ^+ (2 * n - i) * b ^+ i *+ 'C(2 * n, i)).
have step1 : fst_term = 0.
  rewrite /fst_term; apply: big1 => i pi.
  rewrite -signr_odd pi /= expr1 -[X in X + _]mul1r -!(mulrA (-1)).
  by rewrite -!mulrnAr -mulrDl subrr mul0r.

and then we prove the decomposition and remove the 0 term.

have step2 : lhs = 
   fst_term +
  \sum_(i < (2 * n).+1 | ~~ odd i)
     (a ^+ (2 * n - i) * b ^+ i *+ 'C(2 * n, i) +
     (-1) ^+ i * a ^+ (2 * n - i) * b ^+ i *+ 'C(2 * n, i)).
  by rewrite step0 (bigID (fun i : 'I_(2 * n).+1 => odd i)) => /=.
move: step2; rewrite step1 add0r => step2.

We also have to clean-up the second term, making the multiplication by 2 obvious and moving it out of the sum.

have step3 : lhs = 2%:R * \sum_(i &lt; (2 * n).+1 | ~~ odd i)
 (a ^+ (2 * n - i) * b ^+ i *+ 'C(2 * n, i)).
 rewrite step2 big_distrr; apply: eq_bigr => i pi /=.
 by rewrite -signr_odd (negbTE pi) expr0 mul1r mulr2n mulrDl mul1r.

The last step is to reindex the sum, so that the index ranges from 0 to n but the exponents are all doubles. We need to show that this reindexing corresponds to a bijection between the two sets of indices.

have hP : forall i : 'I_n.+1, (2 * i < (2 * n).+1)%N.
  move => i; rewrite ltnS leq_mul2l; apply/orP; right; rewrite -ltnS.
  by case:i.
set h := fun i => Ordinal (hP i).
have bijon : {on [pred i : 'I_(2 * n).+1| ~~ odd i], bijective h}.
  have hP' : forall i : 'I_(2 * n).+1, (i %/ 2 < n.+1)%N.
    move => i; rewrite ltnS [X in (_ <= X)%N](_ : (n = 2 * n %/ 2)%N);
    last by rewrite mulKn.
    by apply: leq_div2r; rewrite -ltnS; case: i.
  exists (fun i => Ordinal (hP' i)); move => i pi; apply val_inj => /=.
    by rewrite mulKn.
  by rewrite [RHS](divn_eq i 2) modn2 (negbTE pi) addn0 mulnC.

With this bijective function, we can reindex the sum and conclude.

have step4 : lhs = 2%:R * (\sum_(j < n.+1 | ~~ odd (2 * j))
      a ^+ (2 * n - 2 * j) * b ^+ (2 * j) *+ 'C(2 * n, 2 * j)).
  by rewrite step3 (reindex h) //=.
by rewrite step4; congr (_ * _); apply/eq_big => // x; rewrite -dvdn2 dvdn_mulr.
Qed.

the final statement

To talk about the 500th digit of a number, I multiply that number by $10^{500}$ . I then show that the new number can be decomposed into a multiple of ten, a digit, and a fractional value between 0 and 1.

Lemma sqrt2_3_instance :
  exists M : nat, exists v, 0 < v < 1 /\
  (Num.sqrt (ratr 3%:Q) + Num.sqrt (ratr 2%:Q)) ^+ 2012 *+ 10 ^ 500 =
  10%:R *+ M + 9%:R + v :>R.
Proof.

The values M and v are as follows

$M = 10 ^ {499} \times 2 \times (\sum_{i=0} ^ {1006} \left(\begin{array}{c}2i\\2012\end{array}\right) 2 ^ i * 3 ^ {1006 - i}) - 1$
$v = 1 - 10 ^ {500} (\sqrt{3} - \sqrt{2}) ^ {2012}$
This is expressed as follows

set M := (10 ^ 499 * 2 *
             (\sum_(i < 1007) 'C(2012, 2 * i) * (2 ^ i * 3 ^ (1006 - i))) - 1)%N.
set v : R := 1 -
    (10 ^ 500)%:R * (Num.sqrt (ratr 3%:Q) - Num.sqrt (ratr 2%:Q)) ^+ 2012.
exists M; exists v; split.

I will not detail the proof that v is between 0 and 1. On the other hand, we need to spend some time explain how the value M fits our needs, because we are actually working in a real-closed field R, and the right-hand side of the equality in lemma main_trick is a value in R that is not guaranteed to be a natural number when a and b are arbitrary.

To make the formulas and commands shorter to write, I define two constants A and B the powers of
the sum and the difference, respectively.

set A := (Num.sqrt (ratr 3%:R) + Num.sqrt (ratr 2%:R)) ^+ 2012.
set B : R := (Num.sqrt (ratr 3%:R) - Num.sqrt (ratr 2%:R)) ^+ 2012.

The goal has the shape

A *+ 10 ^ 500 = 10%:R *+ M + 9%:R + v

But we wish A to be replace by (A + B – B). This is obtained with the following tactic.

rewrite -(addrK B A).

We then distribute the multiplication over the subtraction by $10^{500}$ .

rewrite mulrnBl.

In the right-hand side of the equation, we want to replace $9 + v$ with $10 + (v - 1)$ , so that $(v - 1)$ will be identified with $-B \times 10^{500}$ .

After a few steps of easy algebraic manipulations, we need to identify $A + B$ and

(2 * (\sum_(i < 1007) 'C(2012, 2 * i) * (2 ^ i * 3 ^ (1006 - i))))%:R

After apply the main trick, the expression $A + B$ is replaced by

2%:R *
  (\sum_(i < 1007)
      Num.sqrt (ratr 3%:R) ^+ (2 * 1006 - 2 * i) * Num.sqrt (ratr 2%:R) ^+ (2 * i) *+
      'C(2 * 1006, 2 * i))

The two expressions have the same meaning, but not the same shape. In the right hand-side a full integer expression is cast into the real numbers, in the left hand side, instances of the number two are still hidden inside expressions based on even powers of square roots.
We get rid of the external multiplication by 2 thanks to the following tactic.

rewrite natrM; congr (_ * _).

The two sums have the same index range; it will be possible to compare them term for term, but we first have to make sure that the terms have the same type. For this, we need the conversion to real number to be pushed inside the sum. This is possible thanks to a theorem named big_morph.

rewrite (@big_morph R nat (fun n => n%:R) 0 +%R) /=;[ | | by []]; last first.

This generates a goal where we have to prove that the conversion from natural number to real number indeed is a morphism from the addition on natural numbers to the addition on real numbers.

Once this morphism is applied on the big sum, we can show that the two sums are equal because each term of the sum correspond on each side.

apply: eq_bigr => i _.

The rest is pretty routine.

The complete proof can be seen in the following git repository (the version described is the one with comment “Proof is complete” committed on August 30th, 2017).

Computing numerical bounds

The binomial sums

the final statement

Leave a Reply Cancel reply