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_407 : Polynomial.coeff recurrence4Scalar2Left 407 = ((14037283840209126379681056550909742665168084417250220 * 10 ^ 70 + 5608217981408558865977163373440493778233779523108563746415463751991963) * 10 ^ 70 + 9799117056152075994144654203392724259456838525226180713917222684913567) * 10 ^ 70 + 7697583325411548539134384988381042670045538925744418781098057161282325

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_408 : Polynomial.coeff recurrence4Scalar2Left 408 = -(((4200013804146119815535734396203300291571856594590057 * 10 ^ 70 + 2466913724194785139044700034955068418464714765719761132837786098635170) * 10 ^ 70 + 3731541627245144740654362412565582533471167992590372257729386333365027) * 10 ^ 70 + 3023857823091276471335943895590892293963957596740170615223823370002370)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_409 : Polynomial.coeff recurrence4Scalar2Left 409 = ((1098943874436355151095648008100950769813587497064272 * 10 ^ 70 + 9282607601820148439028404123587544843639495483483735072470930927340115) * 10 ^ 70 + 8445881140775728731425584195836057534339258531645458210474209848030439) * 10 ^ 70 + 1038739562872003223761975786113405773608146738322020799938863747233273

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_410 : Polynomial.coeff recurrence4Scalar2Left 410 = -(((227527466076644583846103849195596516317292882189310 * 10 ^ 70 + 702978504190175329292860474537346122034644598138342235808609736494863) * 10 ^ 70 + 4782892295164099146790256807519826341994633573972614955738625344958311) * 10 ^ 70 + 7654176017204929275853119436753527369180416276342097580489377496001343)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_411 : Polynomial.coeff recurrence4Scalar2Left 411 = ((20291763255669410545474780762982652055968615310913 * 10 ^ 70 + 3970991148012799969484978918395250394905776509415564163495071633587391) * 10 ^ 70 + 3349197163847621530668110803769691846205262174484575357675464074980037) * 10 ^ 70 + 3701016814028457059819604482283175428971450338182849038837324450006062

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_412 : Polynomial.coeff recurrence4Scalar2Left 412 = ((13587829239689476127059194707229014941684873792171 * 10 ^ 70 + 6195022057536186695677537015878556038572929231963712651777160122762973) * 10 ^ 70 + 5943124803411574459130379877665111935943538490447417697548778879544084) * 10 ^ 70 + 4955678661160101267235845700024806193141917795497406966522514963339919

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_413 : Polynomial.coeff recurrence4Scalar2Left 413 = -(((11508344951535161649145027441851644557163307350156 * 10 ^ 70 + 6773738278797132408856655031569323494836447036220414926769354545998417) * 10 ^ 70 + 2737433671156261527159859814039763782285329290853994746093461981404673) * 10 ^ 70 + 5017661172915347860069258999705251171855536430374241966606140212514583)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_414 : Polynomial.coeff recurrence4Scalar2Left 414 = ((6097566519129577841793799885644045737017658040135 * 10 ^ 70 + 677492593665709180798710528119105816125591935989050151613026420429383) * 10 ^ 70 + 5256816933429674281369796849826903412633474545908699291535131054629514) * 10 ^ 70 + 9952664838550767715673531204424893710275663757747186821293584075955320

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_415 : Polynomial.coeff recurrence4Scalar2Left 415 = -(((2725821033410804019275615850618369684810335244502 * 10 ^ 70 + 9257394715502660514694143048168599458851009651581028964048344496754295) * 10 ^ 70 + 2698756234140490910354956063267059037370668450361564900075675838696391) * 10 ^ 70 + 1407587545027072245984251200007597602076660854253692299203577846608043)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_416 : Polynomial.coeff recurrence4Scalar2Left 416 = ((1108329548594360737369687955626276998735493679186 * 10 ^ 70 + 7820738664196224103756483164200628928062162876262326772310700946812723) * 10 ^ 70 + 3215654261055290943985870575738777125727450402724035519453979657265334) * 10 ^ 70 + 1233325232985889204290198155532571577610783259676619449563642701949983

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_417 : Polynomial.coeff recurrence4Scalar2Left 417 = -(((422481658699015212744347573911489686804897733987 * 10 ^ 70 + 7770474316255422575115775185894699026923461889178305857394554962751508) * 10 ^ 70 + 3305003803225560689189165202158654724719065069766068314379536253198641) * 10 ^ 70 + 5643433008522821933147663766504631553354141764692606348729302489209989)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_418 : Polynomial.coeff recurrence4Scalar2Left 418 = ((153218232223868071546027055412929689237354055010 * 10 ^ 70 + 4966067065312458031242221382370473804604595707193209277011029185683613) * 10 ^ 70 + 2172056099058997582367881700749135058214347659305918901696292412917896) * 10 ^ 70 + 7505735917815384214357167907537257170956644079780012948997326761452356

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_419 : Polynomial.coeff recurrence4Scalar2Left 419 = -(((53277106830615301596702112763865384897195046488 * 10 ^ 70 + 1134652059283122979670535446827773451198757783348075831528888934946278) * 10 ^ 70 + 4900150041276340531842541611138055599858572937297535186804508966358437) * 10 ^ 70 + 8031442846133622098986454353424613854971314688512671090711203974388484)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_420 : Polynomial.coeff recurrence4Scalar2Left 420 = ((17833851756745589041588007178425185934182649926 * 10 ^ 70 + 9807659668457112728445590859635006107229086213863705937820706374460260) * 10 ^ 70 + 4592198544570914857625758699389662571461382863745754349950549468181287) * 10 ^ 70 + 1786956899001387004786663419548124581957730780020681699164333929707334

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_421 : Polynomial.coeff recurrence4Scalar2Left 421 = -(((5756840070799112528178896977526376454728726478 * 10 ^ 70 + 7510713400627606119862085738845791174510279969761300903701103378056372) * 10 ^ 70 + 7103494040100918679523874451753851323069260384584950461149931243472077) * 10 ^ 70 + 9362059369123905906631501446399181123629611633213492488326499084276633)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_422 : Polynomial.coeff recurrence4Scalar2Left 422 = ((1792384593817699792764246935340840027473931051 * 10 ^ 70 + 6565286764864004971456572341919525511897697646540862233481867954144048) * 10 ^ 70 + 1235097421955700891370258062082696095439113854040307659382616193736139) * 10 ^ 70 + 9438786787780187337160983103962352756762996787479975617176889092251972

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_423 : Polynomial.coeff recurrence4Scalar2Left 423 = -(((537655303296892559732117557030489502956111965 * 10 ^ 70 + 7843777554979459890963433366527245444032723078565661774875799898073076) * 10 ^ 70 + 5277738610953551274133045624014363264861589557523758450811242803425339) * 10 ^ 70 + 4103279553450047953678949584795193715761312805159552283778693580892312)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_424 : Polynomial.coeff recurrence4Scalar2Left 424 = ((155018569658609261133255147974151832747509949 * 10 ^ 70 + 9520787000143093714387949950434693679275839955621085469046428998614841) * 10 ^ 70 + 547769106357895459568597378502985199366549759134361150679433053138380) * 10 ^ 70 + 4183980648506293859913151675248755569810009993059929655210975090014257

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_425 : Polynomial.coeff recurrence4Scalar2Left 425 = -(((42798652520939500625446795897929864600779843 * 10 ^ 70 + 5682841812963764554724782837621976154535595977924701202435167576646) * 10 ^ 70 + 8635028637057856963204498095173715435786085540230769618958493069256239) * 10 ^ 70 + 1973715814794085583290154515786819930543278201700205931786419177985405)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_426 : Polynomial.coeff recurrence4Scalar2Left 426 = ((11249862868042995839094521084566353260633188 * 10 ^ 70 + 3154349414952587016167660617070100412330054455641095863824494602607732) * 10 ^ 70 + 4124822472783082071396431890724097262888400715919450292542186555023434) * 10 ^ 70 + 9937485635866216575801384741706243256281861652537297776492593752351651

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_427 : Polynomial.coeff recurrence4Scalar2Left 427 = -(((2790426055739078974297544084916752653089904 * 10 ^ 70 + 2592501413560355708106765783329120968022790945401058528987019464359291) * 10 ^ 70 + 8468673612379114185213256436421727395889099820171551760416009876909909) * 10 ^ 70 + 6827619026958562382711652226097404571445014936292182210434487016392666)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_428 : Polynomial.coeff recurrence4Scalar2Left 428 = ((643582332991654987882416063042196169566690 * 10 ^ 70 + 2113949659293866260056119518751497248534855394290842809195481556487176) * 10 ^ 70 + 8859745135424556717215684026953567653739970256393332603165695083867607) * 10 ^ 70 + 5331396433516935878681519225728760278007243034697068357156061053078427

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_429 : Polynomial.coeff recurrence4Scalar2Left 429 = -(((134286107097374431739077623108500871092372 * 10 ^ 70 + 7729621420589808338926482643265680144175871276142396297896520622767537) * 10 ^ 70 + 2871222747455754945884396860993315680276394935861239893278391321051849) * 10 ^ 70 + 6390403026170575410497593950889349335387804424311764873733225319244703)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_430 : Polynomial.coeff recurrence4Scalar2Left 430 = ((23811722635975634582861213912938450396355 * 10 ^ 70 + 5206817936406745789582071988363188734572290725067963546707508087003789) * 10 ^ 70 + 8626501344159756854346803510814671710443809544768670165312442455178048) * 10 ^ 70 + 7327476857187388151240137872965625951729277955256585492831366280571455

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_431 : Polynomial.coeff recurrence4Scalar2Left 431 = -(((2895718397612728902922043096217944037265 * 10 ^ 70 + 850455722476671382031856865647820192420395581088002375168221526315030) * 10 ^ 70 + 9673537203615364572590502950682393064175447962574892301053479428076717) * 10 ^ 70 + 7665378518995707012829497908287587802084629044776602448864399195751432)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_432 : Polynomial.coeff recurrence4Scalar2Left 432 = -(((127409525162271904890740931711636460177 * 10 ^ 70 + 475852437815620141616783232858508746863899797023286932597717466078070) * 10 ^ 70 + 5104650466971171483441514170116851675903617836253130348433787031519490) * 10 ^ 70 + 8668043626834260202318769445156297558985293807477550482389951363004037)