Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1FirstPart3.Coefficients458To484

Recurrence 4 lookup certificate: Scalar1First 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.recurrence4Scalar1First_coeff_458 :

Polynomial.coeff recurrence4Scalar1First 458 = ((2132243542734384572814 * 10 ^ 70 + 95559632074990518822021520760100107656389306835890825676817771918807) * 10 ^ 70 + 8174746001840482059443722019331164335817674764591717684518017930741739) * 10 ^ 70 + 4801224622222818968507843706865513630423555757543089259121069931705520

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

Polynomial.coeff recurrence4Scalar1First 459 = -(((193522502780396037866 * 10 ^ 70 + 1963715796112810753555359291974712810519623426833577793750181092421880) * 10 ^ 70 + 7905502577504597271055172033922843240851940032542931171139119714446330) * 10 ^ 70 + 368200383517942887371042525223594009025564874467095489593637848589127)

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

Polynomial.coeff recurrence4Scalar1First 460 = ((14212419137419108337 * 10 ^ 70 + 9695700871707336731290203518699416363873888599934300625834890474017962) * 10 ^ 70 + 250101524949246312656394937335979202526947214319236174334509684110670) * 10 ^ 70 + 7445113409975841187035929279529599670174795101157541820512141336719039

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

Polynomial.coeff recurrence4Scalar1First 461 = -(((676851404585270119 * 10 ^ 70 + 7840443534112595912269742626490249071864645151438706750184057188923552) * 10 ^ 70 + 2192974062282935765059264487791625552457157242326650935854483735544035) * 10 ^ 70 + 925773428999474152130708287761097111176290935351311752893888589148976)

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

Polynomial.coeff recurrence4Scalar1First 462 = -(((11912040866373518 * 10 ^ 70 + 695352168599085227965797261491894755624677492542027686653972034912328) * 10 ^ 70 + 9446472865477051714090608585872272304439870044352299236326944497148293) * 10 ^ 70 + 9178772112991399311729588881281782253592531646044645164898588953389378)

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

Polynomial.coeff recurrence4Scalar1First 463 = ((7505752630179668 * 10 ^ 70 + 8132923136409812380882432574573295361438933779543328876523281816454607) * 10 ^ 70 + 9569582394248842448515257527192357889041007241421626190820710753431079) * 10 ^ 70 + 7485387521832000940994843110926755230304518594716887125798117949453049

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

Polynomial.coeff recurrence4Scalar1First 464 = -(((1051587746530481 * 10 ^ 70 + 6642066116914551698014747445332981779492648726749514317719731183257097) * 10 ^ 70 + 3655215641534133734180451301289596355979498733962383966800480618642122) * 10 ^ 70 + 6963898127108625395943715702804955690273740678011760279952724870041738)

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

Polynomial.coeff recurrence4Scalar1First 465 = ((98324696441297 * 10 ^ 70 + 5770371919002193806019455730853916213216307840003468961347465573413406) * 10 ^ 70 + 371803054296277553906049431805952053817989785441755407462628640307215) * 10 ^ 70 + 9097662953945287228608143892445236766989545275054061676801122829918671

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

Polynomial.coeff recurrence4Scalar1First 466 = -(((6512942407355 * 10 ^ 70 + 2769845278009641941232057209533571348808156165142776413910496817455634) * 10 ^ 70 + 7838036202333294830511908875073989864384625028205504939629908128273718) * 10 ^ 70 + 9761718271454401282496561727312513151148348881319686504169133680784012)

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

Polynomial.coeff recurrence4Scalar1First 467 = ((246685725995 * 10 ^ 70 + 9782294656210889165779012059850003265819588907425359035645920064772678) * 10 ^ 70 + 729702618218854052250181233222761894194959877402674978663365328511930) * 10 ^ 70 + 430911623565056349484579205664371419539754598065375536565490225746678

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

Polynomial.coeff recurrence4Scalar1First 468 = ((5721656605 * 10 ^ 70 + 1100155284601409499295615931399544311460460210746880980393329911921158) * 10 ^ 70 + 6086464204440646651378579191280326696949057013710873943671586053413939) * 10 ^ 70 + 5317869981542624221102032235780859927037027740311007536680075519812673

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

Polynomial.coeff recurrence4Scalar1First 469 = -(((1848757159 * 10 ^ 70 + 8581478102623126944909126193400723001732519797788866487834664465865696) * 10 ^ 70 + 1904948119900124714321145304629001300152725140923198171454918619705622) * 10 ^ 70 + 2598203703898251469298661628860835129705606298401355850743010667468023)

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

Polynomial.coeff recurrence4Scalar1First 470 = ((168001804 * 10 ^ 70 + 1115948583582087980595709174820757600512644434220881750702070613507374) * 10 ^ 70 + 5042122668749876483382556554538485167508046169894864941091651824245941) * 10 ^ 70 + 2684307540427718912150874669594667957143295177215770483844037044602444

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

Polynomial.coeff recurrence4Scalar1First 471 = -(((9118060 * 10 ^ 70 + 9342227595684593400402307317227234097963136100007298318148974102959610) * 10 ^ 70 + 8774388019672774075945321629722650088872011382725834601900199882447846) * 10 ^ 70 + 8390517262836699892005986349292548573434817421129071603324631042358093)

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

Polynomial.coeff recurrence4Scalar1First 472 = ((250753 * 10 ^ 70 + 3576167343717293255590845073319369596156696085549696888168128784491337) * 10 ^ 70 + 6337801992601095663716661377454802666038498678003979181044719398897719) * 10 ^ 70 + 8706596396931308320165707700733997131308538346579616356342163970518770

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

Polynomial.coeff recurrence4Scalar1First 473 = ((5152 * 10 ^ 70 + 4629215070575844341531869567195676171973212241552904231924124027982109) * 10 ^ 70 + 2339402797066435354588860758594073530111982849485952465932757236775767) * 10 ^ 70 + 832754560011436992777257759801617948668106693509484388723057853630059

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

Polynomial.coeff recurrence4Scalar1First 474 = -(((907 * 10 ^ 70 + 3892103941242784660790793792271454217500950504734630219468083392677393) * 10 ^ 70 + 3315513429774162729326007481856705598593856723148427702755844833398861) * 10 ^ 70 + 2459705604167789154231421864408515891330735756957614555435043397585154)

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

Polynomial.coeff recurrence4Scalar1First 475 = ((43 * 10 ^ 70 + 9145457361110369285285598407383734029994604838224810212468064338038981) * 10 ^ 70 + 9757626508640410888086343859175714653552671280097915540537851705674661) * 10 ^ 70 + 7384817694761147712406002580360888523503755413483773801856644726452059

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

Polynomial.coeff recurrence4Scalar1First 476 = -((8630150453406617890951592861916501457947717440448650460528922550882542 * 10 ^ 70 + 4818917122128416410541703990802810224215818093644452260194961421212525) * 10 ^ 70 + 3892966053240573167678430150598276320841003350740399618414402793669086)

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

Polynomial.coeff recurrence4Scalar1First 477 = -((150046024558216634430908223171364108976208871546421372433022246795929 * 10 ^ 70 + 3235358425524859425965787435739776007346029812987850108680276000372997) * 10 ^ 70 + 8036593994838664854735553309337479395329438156661659870107929629737132)

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

Polynomial.coeff recurrence4Scalar1First 478 = (12573588951064079787261767941931747931658333277899406928643917323541 * 10 ^ 70 + 1711822745272751899518154444096001592574536568529803826789308779129857) * 10 ^ 70 + 5034496875789545957806497511695292989450888670229914849290090247092241

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

Polynomial.coeff recurrence4Scalar1First 479 = -((209589070113555646023053802508960172284259072441423819082912659269 * 10 ^ 70 + 9808951919185102112870310364838558005402348112008968990126419937727174) * 10 ^ 70 + 9552805656224898631890912288081250600410556679478307038671096207174594)

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

Polynomial.coeff recurrence4Scalar1First 480 = -((2735167132955559180408905565668959476472212069394223692449034301 * 10 ^ 70 + 6991259780557913546576044309586145317880981014654882940479947575728439) * 10 ^ 70 + 8327233164145774560302455203684255160387230409025223626929362358899040)

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

Polynomial.coeff recurrence4Scalar1First 481 = (109465818727350610099543711145551895500393979789267722581891644 * 10 ^ 70 + 5567175835700291509826763743557244764571971732268835121470229368364840) * 10 ^ 70 + 7697838799469164700188159985333149206519416123383211906715312019038224

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

Polynomial.coeff recurrence4Scalar1First 482 = (114098085597399545196246396470584643239447369472257458145459 * 10 ^ 70 + 5032325164817294609210907539104204401283829184808244114883447129685129) * 10 ^ 70 + 9878117894627160450143866359795819025252487488571510836420120211088852

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

Polynomial.coeff recurrence4Scalar1First 483 = -((21079716471050467252194432305119714207422246558881626358805 * 10 ^ 70 + 6221531323816400268390130777239976220840111283647786156954682939299440) * 10 ^ 70 + 5437369894713045825081640917492565368317420251974367493945378033181106)

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

Polynomial.coeff recurrence4Scalar1First 484 = -((21877908131638057693534703529642911212818323599467611714 * 10 ^ 70 + 6372418314912375880260698354550874261220095088798311022138481575565020) * 10 ^ 70 + 1899597889143954578408806716242437783853556039842641760513144445299563)