Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupB3Low

Recurrence 2 lookup certificate: B3 source coefficients, low half #

This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_0 :
Polynomial.coeff remainder3Coefficient3 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_1 :
Polynomial.coeff remainder3Coefficient3 1 = 480
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_2 :
Polynomial.coeff remainder3Coefficient3 2 = 2101370
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_3 :
Polynomial.coeff remainder3Coefficient3 3 = 6741833232
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_4 :
Polynomial.coeff remainder3Coefficient3 4 = 1007725038232
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_5 :
Polynomial.coeff remainder3Coefficient3 5 = 1514210590514436
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_6 :
Polynomial.coeff remainder3Coefficient3 6 = -252661954362651579
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_7 :
Polynomial.coeff remainder3Coefficient3 7 = 70580976386535404667
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_8 :
Polynomial.coeff remainder3Coefficient3 8 = -7770078999813774941161
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_9 :
Polynomial.coeff remainder3Coefficient3 9 = 665619660847415358333691
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_10 :
Polynomial.coeff remainder3Coefficient3 10 = -29151787061008139356079371
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_11 :
Polynomial.coeff remainder3Coefficient3 11 = 431573081168452503245082016
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_12 :
Polynomial.coeff remainder3Coefficient3 12 = 30765060231123124340888747962
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_13 :
Polynomial.coeff remainder3Coefficient3 13 = -420465597786790140177689853690
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_14 :
Polynomial.coeff remainder3Coefficient3 14 = -231635597859453393669645890767315
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_15 :
Polynomial.coeff remainder3Coefficient3 15 = 25672040339073566305162429711917504
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_16 :
Polynomial.coeff remainder3Coefficient3 16 = -1592649904244241948776821944667945208
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_17 :
Polynomial.coeff remainder3Coefficient3 17 = 70157524981800905948027975244144740677
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_18 :
Polynomial.coeff remainder3Coefficient3 18 = -2364120591100822355029001163835195851320
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_19 :
Polynomial.coeff remainder3Coefficient3 19 = 62761081465454613200917170451308753755965
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_20 :
Polynomial.coeff remainder3Coefficient3 20 = -1318506620132714491021676215087936613503383
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_21 :
Polynomial.coeff remainder3Coefficient3 21 = 21363805450566397992596429376467518622113721
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_22 :
Polynomial.coeff remainder3Coefficient3 22 = -239591519486512844355524506906757411025312820
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_23 :
Polynomial.coeff remainder3Coefficient3 23 = 838631976014592192045689475297883405338670433
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_24 :
Polynomial.coeff remainder3Coefficient3 24 = 39323680664207917462371268634588994878314588210
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_25 :
Polynomial.coeff remainder3Coefficient3 25 = -1255110642812999386812854618143537947008519295245
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_26 :
Polynomial.coeff remainder3Coefficient3 26 = 24053754625448439086729037783714806004867064042388
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_27 :
Polynomial.coeff remainder3Coefficient3 27 = -358260090509608225437473550360386781388050237382264
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_28 :
Polynomial.coeff remainder3Coefficient3 28 = 4458993574907075907833466976323982545417966441849142
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_29 :
Polynomial.coeff remainder3Coefficient3 29 = -47902052794745215049494643059608532424443234199200138
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_30 :
Polynomial.coeff remainder3Coefficient3 30 = 452230724637998595531068226168393585178727164709934656
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_31 :
Polynomial.coeff remainder3Coefficient3 31 = -3794690300542582961642781778549697535408669518720738785
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_32 :
Polynomial.coeff remainder3Coefficient3 32 = 28519195587756404058556484972768149611446839249356728281
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_33 :
Polynomial.coeff remainder3Coefficient3 33 = -193006169853746414143059339818637808762978975764455612203
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_34 :
Polynomial.coeff remainder3Coefficient3 34 = 1180512781369252764224539615477987005850127381835100835434
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_35 :
Polynomial.coeff remainder3Coefficient3 35 = -6540297908704906261785640102274014945053908943605902258910
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_36 :
Polynomial.coeff remainder3Coefficient3 36 = 32845376198865990567951542846521074366912829360068369899529
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_37 :
Polynomial.coeff remainder3Coefficient3 37 = -149370660360551090862289677618089905267374498746780124414367
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_38 :
Polynomial.coeff remainder3Coefficient3 38 = 613047825618599045320058133249562112630192030938648579518817
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_39 :
Polynomial.coeff remainder3Coefficient3 39 = -2254365055564034132731832311863235427197643124596087865032902
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_40 :
Polynomial.coeff remainder3Coefficient3 40 = 7321318705668383896097494672479343144359967198655430342717486
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_41 :
Polynomial.coeff remainder3Coefficient3 41 = -20359196587192512199618778289586529741252603082861773640976589
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_42 :
Polynomial.coeff remainder3Coefficient3 42 = 44716004517758441781127530550017635633020047704487393900203363
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_43 :
Polynomial.coeff remainder3Coefficient3 43 = -54547649269116285811940460593138403304655554475696782746415836
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_44 :
Polynomial.coeff remainder3Coefficient3 44 = -125509718208091748382174758817225511947054422065220370360597262
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_45 :
Polynomial.coeff remainder3Coefficient3 45 = 1215361719188425093232555521244922693523846897761855976385158596
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_46 :
Polynomial.coeff remainder3Coefficient3 46 = -5541279931949491542041626920062413590725488757902183037311898975
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_47 :
Polynomial.coeff remainder3Coefficient3 47 = 19436837625481187499608194721315137768824828232880362815327875540
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_48 :
Polynomial.coeff remainder3Coefficient3 48 = -58004990475890653255376363542401572493144229521007025661597927553
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_49 :
Polynomial.coeff remainder3Coefficient3 49 = 153900138161638371624835943034609193562584588628438062946369208590
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_50 :
Polynomial.coeff remainder3Coefficient3 50 = -369949353922945682441428217191353664500854628602529259821808490438
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_51 :
Polynomial.coeff remainder3Coefficient3 51 = 786531198946204696287853158862770410673610041919757365882480319893
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_52 :
Polynomial.coeff remainder3Coefficient3 52 = -1315148907904428959344457482256885861297507477213747480995800745496
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_53 :
Polynomial.coeff remainder3Coefficient3 53 = 1119265223719573832872973365455181888551819724380791786529972617873
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_54 :
Polynomial.coeff remainder3Coefficient3 54 = 1103333684396259870377688427485826900794632598081214990524829572842
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_55 :
Polynomial.coeff remainder3Coefficient3 55 = 1879283894331569741651940079644695979141359000303877435700869098121
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_56 :
Polynomial.coeff remainder3Coefficient3 56 = -55916938128361122720655140509859282882931568761100019509452561234930
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_57 :
Polynomial.coeff remainder3Coefficient3 57 = 237409309822331554824686877050604264611793171567334358766319913269188
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_58 :
Polynomial.coeff remainder3Coefficient3 58 = -213809508961350916516566904523070525246423816908895380968995947186338
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_59 :
Polynomial.coeff remainder3Coefficient3 59 = -2435613045093290359826760836596567532184760578143784772131849034201698
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_60 :
Polynomial.coeff remainder3Coefficient3 60 = 1 * 10 ^ 70 + 3669025606547521390174941188337277461436254658068376501898396076304454
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_61 :
Polynomial.coeff remainder3Coefficient3 61 = -(2 * 10 ^ 70 + 9337314899757779683220696984335609046041918345516209208311730243348620)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_62 :
Polynomial.coeff remainder3Coefficient3 62 = -(3 * 10 ^ 70 + 6308947584604616756602443827076121828667671223942697206251844585543158)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_63 :
Polynomial.coeff remainder3Coefficient3 63 = 49 * 10 ^ 70 + 7066274580660981369955743351611388439772409469801925676732534327609626
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_64 :
Polynomial.coeff remainder3Coefficient3 64 = -(177 * 10 ^ 70 + 530895444771418085531175747306495574764841097798966157168987918658459)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_65 :
Polynomial.coeff remainder3Coefficient3 65 = 246 * 10 ^ 70 + 7981732566273496085035602001082015752261480043597428754637415453115977
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_66 :
Polynomial.coeff remainder3Coefficient3 66 = 724 * 10 ^ 70 + 1357216704572356197710263676729547799881075345243555549121601273000653
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_67 :
Polynomial.coeff remainder3Coefficient3 67 = -(5601 * 10 ^ 70 + 3296515130011635859672204617785145896963808738077525612998095820173738)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_68 :
Polynomial.coeff remainder3Coefficient3 68 = 17865 * 10 ^ 70 + 7839627351753032682798882747466385046668110767113526829669925648872946
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_69 :
Polynomial.coeff remainder3Coefficient3 69 = -(28299 * 10 ^ 70 + 8781924408871682093359956131542837394822113871837939698690563478178401)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_70 :
Polynomial.coeff remainder3Coefficient3 70 = -(29616 * 10 ^ 70 + 7432209641770047161144972637366501188852007704895018441642063244091365)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_71 :
Polynomial.coeff remainder3Coefficient3 71 = 366354 * 10 ^ 70 + 8145118652539719394997134023618733741136223405375632738092129050866093