Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar2LeftPart2.Coefficients382To406

Recurrence 4 lookup certificate: Scalar2Left 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.recurrence4Scalar2Left_coeff_382 :

Polynomial.coeff recurrence4Scalar2Left 382 = -(((4901743913621891470863522628085701024178795250777890221482128481 * 10 ^ 70 + 2452105975059090113561429655061254547930950737211626117285238995127148) * 10 ^ 70 + 105568248223159202198818886617524657969839539359992051553201736572170) * 10 ^ 70 + 5157715460114435887125092313919226560051202189227732039942550863374416)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_383 :

Polynomial.coeff recurrence4Scalar2Left 383 = ((1408818476863165013156881811703669849491557056155596775717224860 * 10 ^ 70 + 1630140159185983801130057041123529150082729323045273208410183035500364) * 10 ^ 70 + 3099051350250834861785044546161509124663950420412996150491015811108573) * 10 ^ 70 + 6899072844220034900994403159195547241337999602861645103449115303439371

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_384 :

Polynomial.coeff recurrence4Scalar2Left 384 = -(((322161170039024829375794824632417942313110693429320701527708624 * 10 ^ 70 + 5021353163574347016816075377987236251695448239341417720454574841619361) * 10 ^ 70 + 7475156026658584841498331633597154575041779113946346186018189640961004) * 10 ^ 70 + 4355878137809737034474372611389543744342577161144183045170517545203846)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_385 :

Polynomial.coeff recurrence4Scalar2Left 385 = ((35033478559764422255944047726753303951770931661180525538952639 * 10 ^ 70 + 2644193816910550141754269804634994159388251248415590692137624909990566) * 10 ^ 70 + 6690526030271116469940496159411177706743719331272051795700932277057247) * 10 ^ 70 + 4757232541860961756745781689973905829596495948123185714764454082623838

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_386 :

Polynomial.coeff recurrence4Scalar2Left 386 = ((19282666879695887937698758426957480941962872166179735334532521 * 10 ^ 70 + 1775841272941020677361367510351591620283659347886623664288460727299947) * 10 ^ 70 + 5769034487355971032399117331378435923129209831641227536534004866804418) * 10 ^ 70 + 2265974805645025492487723785883582621823103114962090886968888981458012

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_387 :

Polynomial.coeff recurrence4Scalar2Left 387 = -(((18560943311116612265638138801107958759732820644605754782795985 * 10 ^ 70 + 8982073409837647844576862444753110360302844296475385862049428009060086) * 10 ^ 70 + 7298865202053337744217166322576367362033151803114712900766311546551450) * 10 ^ 70 + 5800339450534517243692861231725266027331964343820083333321928913978197)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_388 :

Polynomial.coeff recurrence4Scalar2Left 388 = ((10633804283071655413693847500729009544011689024833846130975729 * 10 ^ 70 + 5073934649011430125528654566833134177123146774989043300824664791725334) * 10 ^ 70 + 5972620209763572041300569216314905702503656586925135725488280360191175) * 10 ^ 70 + 3629057872186195841772652336673129004508080860337935327098940675948091

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_389 :

Polynomial.coeff recurrence4Scalar2Left 389 = -(((5082001605922062495167876507369403564694849832278268308902274 * 10 ^ 70 + 3194820553929379206663447358945523433924879434614002288490043720681372) * 10 ^ 70 + 9826270543671501334516917549528375797981158210251205337402073676581662) * 10 ^ 70 + 565333192852117820519931236465153219922731920803016078385715464560511)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_390 :

Polynomial.coeff recurrence4Scalar2Left 390 = ((2195829221213345794558696493451130734158184445582251093906395 * 10 ^ 70 + 4309811681659772900770879988285133433810796104134355193439657450885190) * 10 ^ 70 + 3356121065051855484638095887186240770777818868352169629608642719513861) * 10 ^ 70 + 8096565506175907931565785606471530901709993556754050818787418936775607

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_391 :

Polynomial.coeff recurrence4Scalar2Left 391 = -(((885497463292703775168307995326555359115124946055047051219147 * 10 ^ 70 + 8250311885031262920170962063936976764997975395175533220882940470761655) * 10 ^ 70 + 1369507363643012056265840573372304523112965965250548417930789058185600) * 10 ^ 70 + 898894070856778060082856761897752435257478613941388831649919129076329)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_392 :

Polynomial.coeff recurrence4Scalar2Left 392 = ((338357486455706244471177393019056959737328208550157187072168 * 10 ^ 70 + 1007195258881656019672047038191031984527591076620212094454928070380598) * 10 ^ 70 + 6382766487234030627546865121768070739172618814636058217011471077076579) * 10 ^ 70 + 1121620851693590897249239810048677969105002508772465217956512772394279

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_393 :

Polynomial.coeff recurrence4Scalar2Left 393 = -(((123427432442073283870315777994179012473590223962047865768601 * 10 ^ 70 + 2070710432092750516697906943496957154607312631632038195794270490769015) * 10 ^ 70 + 8232900565260277960121459712621822171834957292469678360684727987709149) * 10 ^ 70 + 5939157091356672987450102718418246561970440556810383300603396835776690)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_394 :

Polynomial.coeff recurrence4Scalar2Left 394 = ((43114634979088880187485216662855919516109210621617865200757 * 10 ^ 70 + 179248790743748389879052147186370467712475848410031763880815886335361) * 10 ^ 70 + 5031358805732488640368866504616080875687602254712877440637639820509106) * 10 ^ 70 + 1951019935372424780649340031690580308164434672135678367655049220601977

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_395 :

Polynomial.coeff recurrence4Scalar2Left 395 = -(((14419597448581972321927068006744067692866616042800623106765 * 10 ^ 70 + 6592016943301601467316736534063605859951577632439862733347028274557242) * 10 ^ 70 + 7006878232424658947407388697455479607489869681214914990809425372377097) * 10 ^ 70 + 7880717225067899426708038974093735550473616704820416380006714296081179)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_396 :

Polynomial.coeff recurrence4Scalar2Left 396 = ((4602745526014871118348435449396977781143644609484157332506 * 10 ^ 70 + 6908930346840197662277737096551187307471257635067389992138400100433692) * 10 ^ 70 + 1490591208070299323949109735742516539951216461852928885488022939018712) * 10 ^ 70 + 7686130764027758422362691325471738156742354497426863808082928854283908

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_397 :

Polynomial.coeff recurrence4Scalar2Left 397 = -(((1392428690440330616754750644062279438172583830310313903958 * 10 ^ 70 + 3828754965712247916924926610676868134389941053970509374079590163733290) * 10 ^ 70 + 1015947315542613819574502665890756136236635751666590675519889023832033) * 10 ^ 70 + 3693646305076194409835037720655693492703252095116866979249670083754286)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_398 :

Polynomial.coeff recurrence4Scalar2Left 398 = ((393960466887556554665865765423914470034950063250558153529 * 10 ^ 70 + 1966871201378146213279841866460282501904208044040643812140431340373074) * 10 ^ 70 + 6342836938350100557921840933464906766727710942344342640269929104691357) * 10 ^ 70 + 5509471966737002474075236049739236154195016043502858625944343927246903

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_399 :

Polynomial.coeff recurrence4Scalar2Left 399 = -(((101541877205487224690355101032910082832795399811076590530 * 10 ^ 70 + 458633433493952225675084732446728694346929669655042963639576289238415) * 10 ^ 70 + 1401674710006058958089385679433859349176875858367787984146531164124260) * 10 ^ 70 + 4754158609979128279183391684073325990521827194081163852738765420819066)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_400 :

Polynomial.coeff recurrence4Scalar2Left 400 = ((22422738024341612500770933710728882751389230548837969666 * 10 ^ 70 + 2155195859158747019861969168669386461000573553389483334328032642166338) * 10 ^ 70 + 2889005077123068135856951774279258021638343126996216373456534299307772) * 10 ^ 70 + 4139082680269169919977702154142832495885302318981016791912428481756422

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_401 :

Polynomial.coeff recurrence4Scalar2Left 401 = -(((3432979352296467693474476537889009338632239965147358544 * 10 ^ 70 + 3209373367700255009675529821052173102874455590658929108535415783813731) * 10 ^ 70 + 8333389556329640303528955028585764665536775230410486757458286013143557) * 10 ^ 70 + 5206533516717372251359922004913456510571498207707185570300930430758284)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_402 :

Polynomial.coeff recurrence4Scalar2Left 402 = -(((180433339891394026992461656557340444219120102475273068 * 10 ^ 70 + 4925670333837409068375050779352663766530610936076478134413378745233772) * 10 ^ 70 + 5247518793565782662762538687391776322446820032081977757596684378994648) * 10 ^ 70 + 5589483458145206905107838555963809956450603538323063044943528766937470)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_403 :

Polynomial.coeff recurrence4Scalar2Left 403 = ((460434944769605000034817652155602361875932502712365765 * 10 ^ 70 + 206652547356444078983480708261202814504147574995432027452335931245603) * 10 ^ 70 + 3743630870321094259474827738275121339180419374404449946013252888079023) * 10 ^ 70 + 2856575310972205503252628181420151118863481518571759933347116338477785

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_404 :

Polynomial.coeff recurrence4Scalar2Left 404 = -(((262847440013764398859794384401150840245814926130109308 * 10 ^ 70 + 7412010644688753811442946241677212189730105157996141801768997249456792) * 10 ^ 70 + 1233453940548675691806046946303481052050442280207699517813704450984350) * 10 ^ 70 + 543593886089255482116802071407464278439112830530582977105218323683628)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_405 :

Polynomial.coeff recurrence4Scalar2Left 405 = ((113306095038723238476763957304084271070844144806919817 * 10 ^ 70 + 4195828324694562218195477966686084352683614425848242755305459535532052) * 10 ^ 70 + 8335660394844116286853309697140785349447960283989443089865729200108723) * 10 ^ 70 + 1255850589827842142983655183027737424287186112169980562767334032531755

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_406 :

Polynomial.coeff recurrence4Scalar2Left 406 = -(((42147259253345951767882376652022006296697035641401348 * 10 ^ 70 + 6950604529429255135357891086928849044149437636098829795154789619971846) * 10 ^ 70 + 661614757351416434344237125998516199772689775736755079653343499200096) * 10 ^ 70 + 2258910550247949515781247744524352266108399514109817597367146625528168)