Definition theta1_tbl q : Z :=
  match q with
  | -21 => 302910693998692996157485768413290076966
  | -20 => 336298426882534191759128470626028036789
  | -19 => 186683128335104582129005107785662008085
  | -18 => 207259907386686073192955235040171322419
  | -17 => 230104721262376436189351064420995165904
  | -16 => 255467559620444135892015707268715336457
  | -15 => 283625966735416996535885333662014114405
  | -14 => 314888078651228693933689466069052580905
  | -13 => 174797997549285651882438866782683340398
  | -12 => 194064761537588616893622436057812819408
  | -11 => 215455166527421378856590945602770070141
  | -10 => 239203286653190548679094257880939433815
  | -9 => 265568996408383549344794103276234313665
  | -8 => 294840814439182918143871451639708507103
  | -7 => 327339060789614187001318969682759915222
  | -6 => 181709681073901722637330951972001133589
  | -5 => 201738271725539733566868685312735302683
  | -4 => 223974474217780421055744228056844427813
  | -3 => 248661618204893321077691124073410420051
  | -2 => 276069853871622551497390234491081018099
  | -1 => 306499108173177771671669405430061836724
  | 0 => 170141183460469231731687303715884105728
  | 1 => 188894659314785808547840000000000000000
  | 2 => 209715200000000000000000000000000000000
  | 3 => 232830643653869628906250000000000000000
  | 4 => 258493941422821148397315216271863391740
  | 5 => 286985925493722536125179818657774823687
  | 6 => 318618382226490455405776079553542361119
  | 7 => 176868732008334225927912486150152183217
  | 8 => 196363738611909062123830878199451025720
  | 9 => 218007543808417316859394750271862213031
  | 10 => 242036994678082392051126914580396990474
  | 11 => 268715044302683550071638623558009085183
  | 12 => 298333629248008269731638612618517353496
  | 13 => 331216864211123806751178713779234900611
  | 14 => 183862294395666818064937594201088633456
  | 15 => 204128152598478183127259193653345185578
  | 16 => 226627774989027955951103258828533066424
  | 17 => 251607373812388019852618613412845800985
  | 18 => 279340299571981831419774226402503504146
  | 19 => 310130032290502989833240994779765547114
  | 20 => 172156751238329846960951049916624692801
  | _ => 0