The second supplement to the law of quadratic reciprocity.

[Alexander van der Vekens]

I started to prove some theorems for Fermat numbers, but I got stuck because I need the "second supplement to the law of quadratic reciprocity", i.e the value of the Legendre/Kronecker symbol for 2. The theorem is available in set.mm ( ~2lgs), but unfortunately without proof (and commented out).

I think Gauss' Lemma is required for the proof, which could be (formally) stated as follows:

Let p be an odd prime and a an integer which is not divisible by p. Let S={a,2a,3a,...,(p-1)a/2}. Let n denote the number of elements of S whose least positive residue modulo p is greater than p/2. Then ( a | p )  = (-1)^n.

gausslemma $p |- ( ( ( P e. Prime /\ -. 2 || P ) /\ ( A e. ZZ /\ -. P || A )
                                      /\ N = ( # ` { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) )

                                                                           ( x = ( i x. A ) /\ ( P / 2 ) < ( x mod P ) ) } ) )
                                  -> ( A /L P ) = ( -u 1 ^ N ) ) $=
    ? $.

I succeeded already in proving ~2lg on base of ~ gausslemma (with A = 2), but to prove ~gausslemma would still be tedious (see, for example https://proofwiki.org/wiki/Gauss%27s_Lemma_(Number_Theory) ).

Is there an alternate way to proof ~2lg? Is there a simple proof for ~gausslemma? Which theorems are already available in set.mm which could help to finish the proofs for ~2lg and ~gausslemma?

[Thierry Arnoux]

Hi Alexander,

Theorem ~ lgsquadlem2 seems to be similar to Gauss' Lemma. Wikipedia also mentions it in its entry on Eisenstein proof of the quadratic reciprocity: This result is very similar to Gauss's lemma, and can be proved in a similar fashion.

After a bit more consideration though, it does not seem to me that it is easy to derive Gauss' lemma from it. This would leave you with proving Gauss' lemma.

Or, if you don't mind cooperation, you could call for someone in the community to prove Gauss' lemma while you continue on Fermat numbers.

BR,
_
Thierry

[Alexander van der Vekens]

On Sunday, June 20, 2021 at 12:01:38 PM UTC+2 Alexander van der Vekens wrote:

I started to prove some theorems for Fermat numbers, but I got stuck because I need the "second supplement to the law of quadratic reciprocity", i.e the value of the Legendre/Kronecker symbol for 2. The theorem is available in set.mm ( ~2lgs), but unfortunately without proof (and commented out).

I could prove ~2lgs now - it's available in the latest version of set.mm.

I think Gauss' Lemma is required for the proof, which could be (formally) stated as follows:

Let p be an odd prime and a an integer which is not divisible by p. Let S={a,2a,3a,...,(p-1)a/2}. Let n denote the number of elements of S whose least positive residue modulo p is greater than p/2. Then ( a | p )  = (-1)^n.

gausslemma $p |- ( ( ( P e. Prime /\ -. 2 || P ) /\ ( A e. ZZ /\ -. P || A )
                                      /\ N = ( # ` { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) )

                                                                           ( x = ( i x. A ) /\ ( P / 2 ) < ( x mod P ) ) } ) )
                                  -> ( A /L P ) = ( -u 1 ^ N ) ) $=
    ? $.

I succeeded already in proving ~2lg on base of ~ gausslemma (with A = 2), but to prove ~gausslemma would still be tedious (see, for example https://proofwiki.org/wiki/Gauss%27s_Lemma_(Number_Theory) ).

I proved the special case of Gauss' lemma (for A = 2, see ~ gausslemma2d ), which was sufficient to prove ~2lgs. The general version of Gauss' lemma is still  unproven. If anybody wants to prove it, the theorem is available as ~gausslemma in set.mm (commented out).