Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0LeftPart0.Coefficients135To162

Recurrence 4 lookup certificate: Scalar0Left coefficient convolution #

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_135 :
Polynomial.coeff recurrence4Scalar0Left 135 = -(((54813238226920978366371500310469547637911993826201015727 * 10 ^ 70 + 591227961759512646393321232449099388637535199568604671087023759544852) * 10 ^ 70 + 3917313303937190941400733515637285162075777725691282349194081468937146) * 10 ^ 70 + 7298600109393621874059875234530574492748925016586257636829928437681441)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_136 :
Polynomial.coeff recurrence4Scalar0Left 136 = ((314852236662517487607346837466039904980770564795600033044 * 10 ^ 70 + 3734052811969507995664359964799930083379511236042648293496212916499278) * 10 ^ 70 + 5682153709397262389934186717040088426083920417558234009402462480913685) * 10 ^ 70 + 3294789636317614630399407398922952380470758651219439575662260488441021
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_137 :
Polynomial.coeff recurrence4Scalar0Left 137 = -(((1774828587855102458767742643329368122991414759590751484108 * 10 ^ 70 + 9422360065784288867284082719387794062688924880997642151122745056650646) * 10 ^ 70 + 4089270371782359349059966236107192345369305637988357089633462655622390) * 10 ^ 70 + 71631917011182380953586299550913636421126399002770403319205597224351)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_138 :
Polynomial.coeff recurrence4Scalar0Left 138 = ((9819843956687692115889527163890247349745691934017736918978 * 10 ^ 70 + 4760812694346963166541411946880387206939998048461782133446500587813564) * 10 ^ 70 + 5761399348466204507441512997542696937291238400772086832451402731952939) * 10 ^ 70 + 2862628377434434448086616322206323374678740269933528561918546939216127
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_139 :
Polynomial.coeff recurrence4Scalar0Left 139 = -(((53335879374996119925864622382308309493976724913891356963546 * 10 ^ 70 + 6653788699261969764063143489688777323021701508229886835813617633316807) * 10 ^ 70 + 9035212813761588591599111558223744040469243602664676076712994161463020) * 10 ^ 70 + 7544905028392763604509407370539756781109891553794443237244598199926763)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_140 :
Polynomial.coeff recurrence4Scalar0Left 140 = ((284424638765686293322647915478476865728361456755457151057873 * 10 ^ 70 + 4683899469389285357105382238793130818374463209827032430563341300362682) * 10 ^ 70 + 5111647368524003168913876241498037053390997463803748755104088661213139) * 10 ^ 70 + 8665747133713239938486729950478991955013017325180079292630374437944778
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_141 :
Polynomial.coeff recurrence4Scalar0Left 141 = -(((1489402657388471955435736378235877503296316322883820716301287 * 10 ^ 70 + 6388589230655832945373237922004642712577885333538684689317186661426953) * 10 ^ 70 + 850333814622282464112398893520460526003030440283134699069260049570449) * 10 ^ 70 + 7251237335113278845937356875367013125129381285805955911884089159826688)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_142 :
Polynomial.coeff recurrence4Scalar0Left 142 = ((7659785741176226916561718361967380823684930039315230462890261 * 10 ^ 70 + 6515522634230965497678799038121543979331771677529530470611990529883715) * 10 ^ 70 + 6954221339234285301503209695545693497595854277519181832762768937899853) * 10 ^ 70 + 9442725414936002643680944250045228883535472208180814105890478041728415
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_143 :
Polynomial.coeff recurrence4Scalar0Left 143 = -(((38693798829747665190436217149697812987811190721458826500379461 * 10 ^ 70 + 3183841075742266135663553021115044417830747856684165852327270089676031) * 10 ^ 70 + 5391996504013769777381155947800982981348718014687789336228889232302904) * 10 ^ 70 + 9605747636809278167928265713235243624303780963963606007470472151092887)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_144 :
Polynomial.coeff recurrence4Scalar0Left 144 = ((192019492904576894289356233721258317874061637421476706510340472 * 10 ^ 70 + 8417522986839700581914836963259506693621445349786179398107583746283374) * 10 ^ 70 + 1716534776689889539272488305377590853264085683731567010499050550394489) * 10 ^ 70 + 964940668754285389463878540363343069743379216252884177915950477238327
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_145 :
Polynomial.coeff recurrence4Scalar0Left 145 = -(((936236926388480854792375401580633880051517588247668518209460513 * 10 ^ 70 + 2999061431401286632570801037877133707905039148690101406046513890513356) * 10 ^ 70 + 3285054437949147079858793178024309140794340882771222154574654828230621) * 10 ^ 70 + 1604934841841981941506972589545604777804131035837747038036696304748356)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_146 :
Polynomial.coeff recurrence4Scalar0Left 146 = ((4485577972379420835801572335315351578026724776009342825917937750 * 10 ^ 70 + 5619365594404735280023191742191771878720792187851089982172242252673108) * 10 ^ 70 + 5184579065639229889457694283797013006936660134603859826977057919280114) * 10 ^ 70 + 3218598652849718934422860933932058354960089329105351446323791803439856
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_147 :
Polynomial.coeff recurrence4Scalar0Left 147 = -(((21120169488760465233919412178322864614086614226699831601809893220 * 10 ^ 70 + 278618392134642712164291281913191302904913972178049223090007694354158) * 10 ^ 70 + 8476145374966580970798081748880413382853610732908158065143240945604026) * 10 ^ 70 + 8538953107293324870134921174569364147075682326563690799644417027357685)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_148 :
Polynomial.coeff recurrence4Scalar0Left 148 = ((97740685178183524378606310698234792308129674027585511632420848121 * 10 ^ 70 + 7628904442361559000481696971875006687781158997739690903092332572567290) * 10 ^ 70 + 4467749888704752448788118209660995586939092626549506993469143141782248) * 10 ^ 70 + 502512675601602026475194478664618620520175654553869333147133499288052
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_149 :
Polynomial.coeff recurrence4Scalar0Left 149 = -(((444634892980022301699122871396247723915559208061136704925912859122 * 10 ^ 70 + 692974433383668854031522257916740416877492378089610191843498422590116) * 10 ^ 70 + 2954662522305738812754045738155777027231314947201711606228825312856546) * 10 ^ 70 + 2400350489262217322007837162380437644222014008864375460621771981202832)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_150 :
Polynomial.coeff recurrence4Scalar0Left 150 = ((1988527778617387588674114467152183438506925146787772200698306227688 * 10 ^ 70 + 444101230087621713466334544785802408019496311150192453297576271496688) * 10 ^ 70 + 9050830784549249454316162869090727322892493069468125144359513926029463) * 10 ^ 70 + 8276805080276969612016879256287177273674719750214793648286146039973075
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_151 :
Polynomial.coeff recurrence4Scalar0Left 151 = -(((8743959680853543042953601185860347823630101337245274836119481313270 * 10 ^ 70 + 5122526772476742141535339576447958503595721164568831053546292599289676) * 10 ^ 70 + 4072603492313934184032262380688097124766346938044415697218741312269933) * 10 ^ 70 + 9835462131847635835524809990538562807180193351856538368666195936347856)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_152 :
Polynomial.coeff recurrence4Scalar0Left 152 = ((37807683064189673497141684931776192509832807739970325278366810493870 * 10 ^ 70 + 9286713500666181075816694117291203330785588324867915515887225234295071) * 10 ^ 70 + 8119127583689919625568778317175330103262134342554985762760495446464118) * 10 ^ 70 + 1373498754710036332318573720496963387082168797328345662418498685308994
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_153 :
Polynomial.coeff recurrence4Scalar0Left 153 = -(((160765622592281569280805023635264586481975722415702869228033669279006 * 10 ^ 70 + 6622889220897107516422458025385488105224087911738627046483835791423694) * 10 ^ 70 + 3406253318649183774353503704555741748079224942317195864253746005628325) * 10 ^ 70 + 9226684269991089205148599991324901980988381422799480116199973330619611)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_154 :
Polynomial.coeff recurrence4Scalar0Left 154 = ((672344762185203307934492202805093163158816844998301622178591088557359 * 10 ^ 70 + 4020069396652838138999285285213276293878983655399160181889782426088206) * 10 ^ 70 + 8317346116613439609384269963528451735935664880833692800835037496144805) * 10 ^ 70 + 6001584685423772289209143194898407872234839590569587547216915339246718
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_155 :
Polynomial.coeff recurrence4Scalar0Left 155 = -(((2765794208874419492220867157547259939267410007696629330242299960219987 * 10 ^ 70 + 8859780127275249308815700602969994017031514451471210837372313940660646) * 10 ^ 70 + 7488237494054083765386632967656880880331526701371941963171520306068076) * 10 ^ 70 + 8438607989848311020767949256692628137593059215448478688822098467622386)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_156 :
Polynomial.coeff recurrence4Scalar0Left 156 = (((1 * 10 ^ 70 + 1192285582873756997726626964787282559789111066080978242054640379400767) * 10 ^ 70 + 9545232182157526158560239880684494900211671475843385954870712015694203) * 10 ^ 70 + 1151023030196431672348576325513284395609247120097755719973278148261718) * 10 ^ 70 + 231624990486254274401083133824074624812241228096076889372032728456695
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_157 :
Polynomial.coeff recurrence4Scalar0Left 157 = -((((4 * 10 ^ 70 + 4558412120649568780362792321583885805074663980878399182056177861832161) * 10 ^ 70 + 6093140880687732762345394038201587529362884042903816095691887494338028) * 10 ^ 70 + 8816734001394562430712162369249767953082732202425268440972946438208471) * 10 ^ 70 + 439922482501746490951837720605490011743350583425615191865881860912384)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_158 :
Polynomial.coeff recurrence4Scalar0Left 158 = (((17 * 10 ^ 70 + 4538972517567483494176437163030230788871912630314425600996914784081361) * 10 ^ 70 + 7599564538406672426492508881107370280151091460234051929224432924765372) * 10 ^ 70 + 84485031533966693387886907433967470610787388974440183365414184766659) * 10 ^ 70 + 4932855805401018322804331617208783819594157678504186851866477352979268
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_159 :
Polynomial.coeff recurrence4Scalar0Left 159 = -((((67 * 10 ^ 70 + 2737421102361317117194509294778915557852410075869162913422785555908411) * 10 ^ 70 + 3341834745306938229130535674643912978099605700153837276772316043491221) * 10 ^ 70 + 1226818025193379947270967044423747893784521042485734465701251252777777) * 10 ^ 70 + 4602212172299243784977948703619764635628730401857772020161135357704032)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_160 :
Polynomial.coeff recurrence4Scalar0Left 160 = (((255 * 10 ^ 70 + 1683553143240329775647795827119712559273972459464307349703318464068043) * 10 ^ 70 + 2644146650440872156318240952154154949051175906353963805143452377089475) * 10 ^ 70 + 5553469076193667550508205527175618256028733156970027259447613644284191) * 10 ^ 70 + 9271156323805852086403625215216150781974587468111953120985644266051413
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_161 :
Polynomial.coeff recurrence4Scalar0Left 161 = -((((952 * 10 ^ 70 + 5167933876858770961754830199150845961428535582726197312310707099411109) * 10 ^ 70 + 2633262664940719238363592031786603753344853818593180649857777050845494) * 10 ^ 70 + 3023577925726305236885261092360344001208294509523802649891872001036296) * 10 ^ 70 + 1048355215850873981512060544498376473507012768383993172118189969474301)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_162 :
Polynomial.coeff recurrence4Scalar0Left 162 = (((3499 * 10 ^ 70 + 6013787481189289166633245890829536901422818967359721710162942277948776) * 10 ^ 70 + 1380399420474739099491381763394908771484577674528968109627628001730437) * 10 ^ 70 + 7348036099103673754596893137896023054018530328792688778264250898420374) * 10 ^ 70 + 6812044780854591228949355402554755850704611875607838234064996393717101