Quelle primes_sum_squares.pvs Sprache: PVS

primes_sum_squares: THEORY

%------------------------------------------------------------------------------
% Every Prime p with mod(p,4)=1 is a Sum of Two Squares
% Author: Anthony Narkawicz
% Date:   March 2012
%-------------------------------------------------------------------------------
BEGIN

   IMPORTING ints@primes,ints@gcd, prime_factorization

    % The lemmas below are part of Euler's proof of this result
    % As noted below, the proof using this method is not completed.
    % Instead, Zagier's simpler proof of the result is finally used below

    n,m,i,j,a,b: VAR nat
    pa,pb: VAR posnat
    ai,bi: VAR int
    p: VAR (prime?)

    sum_of_two_squares?(n) : bool = (EXISTS (a,b): n=a^2+b^2)

    sots_int?(n) : bool = (EXISTS (ai,bi): n = ai^2+bi^2)

    sots_int_def: LEMMA sots_int?(n) IMPLIES sum_of_two_squares?(n)

    prime_sum_of_two_squares?(n): bool = prime?(n) AND sum_of_two_squares?(n)

    ns,ms,is,js,bs: VAR (sum_of_two_squares?)

    ps,qs   : VAR (prime_sum_of_two_squares?)

    Brahmagupta_Fibonacci: LEMMA sum_of_two_squares?(ns*ms)

    prime_divides: LEMMA divides(p,ai*bi) IMPLIES (divides(p,ai) OR divides(p,bi))

    sots_div_prime_closed: LEMMA divides(ps,ns) IMPLIES sum_of_two_squares?(ns/ps)

    sots_div_quot_factor: LEMMA sum_of_two_squares?(ns) AND divides(m,ns) AND (NOT sum_of_two_squares?(m)) IMPLIES
          (EXISTS (b): divides(b,ns/m) AND (NOT sum_of_two_squares?(b)))

    rel_prime_sos_factor: LEMMA rel_prime(pa,pb) AND divides(n,pa^2+pb^2) IMPLIES sum_of_two_squares?(n)

    % This ends the work on Euler's proof
    % As it turns out, Zagier's "one line proof" works much better in this context,
    % and it is given below.

    fermat_prime_sos_set(p)(x,y,z:nat): bool = x^2 + 4*y*z = p

    fermat_prime_sos_finite_set: LEMMA
      finite_sets[[nat,nat,nat]].is_finite(fermat_prime_sos_set(p))

    involution_odd_has_fixedpoint: LEMMA
      FORALL (N:posnat,invol:[below(N)->below(N)]):
      odd?(N) AND (FORALL (i:below(N)): invol(invol(i)) = i) IMPLIES
      EXISTS (i:below(N)): invol(i) = i

    involution_one_fixedpoint_odd: LEMMA
      FORALL (N:posnat,invol:[below(N)->below(N)]):
      (FORALL (i:below(N)): invol(invol(i)) = i) AND
      (EXISTS (j:below(N)): FORALL (i:below(N)): invol(i)=i IFF i=j)
      IMPLIES
      odd?(N)

   involution_fermat_set_one_fp_invol: LEMMA
      LET invol:[[nat,nat,nat]->[nat,nat,nat]] =
         (LAMBDA (x,y,z:nat): IF x<y-z THEN (x+2*z,z,y-x-z)
        ELSIF y-z <= x AND x <= 2*y THEN (2*y-x,y,x-y+z)
      ELSE (x-2*y,x-y+z,y) ENDIF)
      IN (FORALL (x,y,z:nat): fermat_prime_sos_set(p)(x,y,z) IMPLIES
        invol(invol(x,y,z)) = (x,y,z) AND
fermat_prime_sos_set(p)(invol(x,y,z)))

    invol_fermat(p)(xyz: (fermat_prime_sos_set(p))): (fermat_prime_sos_set(p)) =
      LET (x,y,z) = xyz IN
      IF x<y-z THEN (x+2*z,z,y-x-z)
        ELSIF y-z <= x AND x <= 2*y THEN (2*y-x,y,x-y+z)
      ELSE (x-2*y,x-y+z,y) ENDIF

    k : VAR posnat

    invol_fermat_one_fp: LEMMA p = 4*k+1 IMPLIES
      FORALL (xyz:(fermat_prime_sos_set(p))):
        invol_fermat(p)(xyz) = xyz IFF xyz = (1,1,k)

    fermat_prime_mod_4: LEMMA mod(p,4) = 1 IMPLIES
      sum_of_two_squares?(p)

END primes_sum_squares

quality90%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.