Library PrimeGapS1.Witness_Rayleigh


From Stdlib Require Import ZArith List.
Import ListNotations.
Open Scope Z_scope.

Definition v_witness : list (Z × Z) :=
  [
  ((-1)%Z, 67213321643309%Z) ;
  ((-1)%Z, 127608469198%Z) ;
  (1%Z, 279653882552%Z) ;
  ((-1)%Z, 12020445731%Z) ;
  (1%Z, 549859441%Z) ;
  ((-1)%Z, 1793413588%Z) ;
  ((-1)%Z, 2852111653%Z) ;
  (1%Z, 39510722%Z) ;
  (3%Z, 12111503%Z) ;
  ((-1)%Z, 5889766%Z) ;
  ((-1)%Z, 3065036%Z) ;
  ((-11)%Z, 16762960%Z) ;
  (1%Z, 56351289%Z) ;
  ((-4)%Z, 1502055%Z) ;
  ((-368)%Z, 7848717%Z) ;
  ((-248)%Z, 7629181%Z) ;
  (83%Z, 10305760%Z) ;
  (874%Z, 12663047%Z) ;
  (2999%Z, 13498748%Z) ;
  (389%Z, 4466540%Z) ;
  ((-3)%Z, 6400234%Z) ;
  (1277%Z, 10688233%Z) ;
  (11484%Z, 3794749%Z) ;
  (39537%Z, 8813404%Z) ;
  (6952%Z, 10377483%Z) ;
  ((-6142)%Z, 31211377%Z) ;
  ((-227846)%Z, 52361791%Z) ;
  ((-150115)%Z, 7175034%Z) ;
  ((-250783)%Z, 22648711%Z) ;
  (37237%Z, 12498809%Z) ;
  (67%Z, 12886771%Z) ;
  ((-35583)%Z, 17941657%Z) ;
  ((-522509)%Z, 7595235%Z) ;
  ((-1507327)%Z, 7740852%Z) ;
  ((-365121)%Z, 2548910%Z) ;
  ((-499886)%Z, 13468967%Z) ;
  (14389%Z, 7143324%Z) ;
  (5289169%Z, 57282634%Z) ;
  (11505763%Z, 16419588%Z) ;
  (1%Z, 1%Z) ;
  (15488075%Z, 35377856%Z) ;
  (312214%Z, 4565683%Z)
  ].