Recurrence 4 lookup certificate: Scalar1Left 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.recurrence4Scalar1Left_coeff_402 : Polynomial.coeff recurrence4Scalar1Left 402 = -(((98917408296810271292170158808917936167325896172452075238 * 10 ^ 70 + 9169418257578094511175341965660512776544462122859079807439191400257008) * 10 ^ 70 + 5400387037596255149655546111624879898995381343463200222585982850039105) * 10 ^ 70 + 4353881076843710411188718031963635799294629020482387471015307450565664)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_403 : Polynomial.coeff recurrence4Scalar1Left 403 = ((25846881918653240098034177302852290182952481196438292163 * 10 ^ 70 + 2570225796188144464798417345153265864641008668365226429169773339511799) * 10 ^ 70 + 2154737625335994079643359869028001379978071241056494024315293872235177) * 10 ^ 70 + 7131615875789113140133482786878238086467096229178946221832342698348831

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_404 : Polynomial.coeff recurrence4Scalar1Left 404 = -(((5740402188605195907472400344130340770211200135599075651 * 10 ^ 70 + 560003251999741123666681771231998711188719219727411244286395820992567) * 10 ^ 70 + 2190573122789264921647764864345487586590772584428097401730498778034083) * 10 ^ 70 + 9196843614328480620238869185752761695960025562418982160072582381567167)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_405 : Polynomial.coeff recurrence4Scalar1Left 405 = ((862872694813203644206140148585639008528870726707884809 * 10 ^ 70 + 8967064915181247241662684393189569207362875732855764767650662915568811) * 10 ^ 70 + 3102163939232872677796778228325135324240118042485581256164447411617729) * 10 ^ 70 + 9744257686529476786317350356872136002415883727270756313708784115368614

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_406 : Polynomial.coeff recurrence4Scalar1Left 406 = ((64580528461842676327668427939213690958491912497404247 * 10 ^ 70 + 5140426344799803355782779423849857514325572779137368147986789576850114) * 10 ^ 70 + 2995395822250643736005192863973284563014217279761447828018657773962184) * 10 ^ 70 + 5562824849090928545524406498265953089816634592560704181718331386290243

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_407 : Polynomial.coeff recurrence4Scalar1Left 407 = -(((129855082238557060531636140453726928486478398458326952 * 10 ^ 70 + 72211381698904914286665233272197993204202892821685277573499322148915) * 10 ^ 70 + 9568046203136006468050496109477719390064035799037448565463452603325588) * 10 ^ 70 + 6897678354882317782781371900463215928124531984314749904438120767317417)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_408 : Polynomial.coeff recurrence4Scalar1Left 408 = ((73459474923106570375205302864195010801279789206854839 * 10 ^ 70 + 6018836374486327695723341164531081636783691662559399068766588647134660) * 10 ^ 70 + 7089682455127297177757354634919546782462683144628031349405279296747534) * 10 ^ 70 + 1097128352039454060058962586724668040157171994372766447361314277541714

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_409 : Polynomial.coeff recurrence4Scalar1Left 409 = -(((31820808060979318536141641939563337208727640615542154 * 10 ^ 70 + 4037147711301805069834593766475507552469801309177756450023727502243082) * 10 ^ 70 + 6392356130604645363001636207816250350088262745977487867771263165615839) * 10 ^ 70 + 3024993965341673086180955474982614459861939201039729347983884631501576)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_410 : Polynomial.coeff recurrence4Scalar1Left 410 = ((11994358246079443290585941401826812595140920859566178 * 10 ^ 70 + 9683890495452234652004104537769374887298675975130935985560637713488089) * 10 ^ 70 + 2396486437086105963064866308802806266118950030216728262747177089172581) * 10 ^ 70 + 3189819720392827392440320705534111116112038916802652886666450741164327

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_411 : Polynomial.coeff recurrence4Scalar1Left 411 = -(((4093671763381681896092051416408173094667996093033718 * 10 ^ 70 + 5018460905050237008100748920873282186447989251926484817135527037917295) * 10 ^ 70 + 7845514590531867474283596776966287501163374743623457848581552618040595) * 10 ^ 70 + 4970592591284959260482848793370107295676550505828338598423548382496355)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_412 : Polynomial.coeff recurrence4Scalar1Left 412 = ((1279919271796075695545371370259381360927466363969625 * 10 ^ 70 + 9395963517978325275154296671380923570840430305438325485349175070209183) * 10 ^ 70 + 551724092038884498873180375015260763465414168392786190696355232625318) * 10 ^ 70 + 9745357993942996022285614724118974824881865326959549056619899874358434

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_413 : Polynomial.coeff recurrence4Scalar1Left 413 = -(((364240652672719534656407688975153628253462084434102 * 10 ^ 70 + 3419985171278512717081510964126738033519701850532104384619071642234280) * 10 ^ 70 + 5484733120762020260584673016102477110082918827475485063668918854304877) * 10 ^ 70 + 4107391998202213521235144502197855630197551440930291305605238757127339)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_414 : Polynomial.coeff recurrence4Scalar1Left 414 = ((91321664644834798443420472916971665488340525665319 * 10 ^ 70 + 6869021028907105602022973209332927536952039587201809480726558936793727) * 10 ^ 70 + 7712521298751055130823100930486599751324285228301730376102860924059763) * 10 ^ 70 + 7444773667273925475485147299406743971451332504838440215527581783518564

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_415 : Polynomial.coeff recurrence4Scalar1Left 415 = -(((18093747532835580094931853914879635823519590959047 * 10 ^ 70 + 5299912497583999877128029133569553890273620795871722117037577042383698) * 10 ^ 70 + 943471285750363489270191334550555451627419500664566414032817088979510) * 10 ^ 70 + 8342558641568778314270571948923146307134734783467450079207590644915365)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_416 : Polynomial.coeff recurrence4Scalar1Left 416 = ((1406482427381880496917275668061640484620845854284 * 10 ^ 70 + 3535156518383724821813346622282727829912979021605441814269171835531793) * 10 ^ 70 + 3238688166584019888775097379902988964555717422853434906107629574176032) * 10 ^ 70 + 4634937818662564289236177718066929197338073127047772509985006751798255

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_417 : Polynomial.coeff recurrence4Scalar1Left 417 = ((1157762835744256948124674258530090550893825979758 * 10 ^ 70 + 8544841375731930974319139188316223435000188492297111112828735019133558) * 10 ^ 70 + 9737357803721534270173124970375218362946650720851294873397102512236948) * 10 ^ 70 + 4840709909838745138023788703667819298184673173200706981795682795143364

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_418 : Polynomial.coeff recurrence4Scalar1Left 418 = -(((929318956110608539262677086872859490775358433728 * 10 ^ 70 + 9223945280735823351859086278314892771964068651413934522587902823358253) * 10 ^ 70 + 1620181821801449622014932646703778525066809965184897832096785347938424) * 10 ^ 70 + 1149804731049418471702505947825838553536102874738345108587247150229125)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_419 : Polynomial.coeff recurrence4Scalar1Left 419 = ((482532798387741048559158022224549802066621763098 * 10 ^ 70 + 2018085154093259519784368587024677217731071925777641137935506559804199) * 10 ^ 70 + 3656206730775272875848513862692501727630214597144877393921917775305030) * 10 ^ 70 + 5652826316983765573641726104454260482430037230679419041903820912550965

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_420 : Polynomial.coeff recurrence4Scalar1Left 420 = -(((212802550572357516279276818998013942756872855859 * 10 ^ 70 + 2952079727664940331509087990466261543387028886709537547051776657454939) * 10 ^ 70 + 7045375904498403636574439865267542370522177742875207402955377624719073) * 10 ^ 70 + 9928081166094371690554193953696438344467475339256811978058098127408297)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_421 : Polynomial.coeff recurrence4Scalar1Left 421 = ((85485934851589261048121537841986589127367836226 * 10 ^ 70 + 9226554947561281556844601239616532849331873963361472618191330679456930) * 10 ^ 70 + 9218100292762478650690207657198514401693982352964041576581675256912819) * 10 ^ 70 + 4784102538173421702272514605778261489462036194080591908961079321485280

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_422 : Polynomial.coeff recurrence4Scalar1Left 422 = -(((32162316501865814673465326214540829125997317131 * 10 ^ 70 + 8634042671021146138533878564363120211999272491803526574007819747702961) * 10 ^ 70 + 6116747266385140278723110149793709669615724471868184662133539799398663) * 10 ^ 70 + 8683727173807980215388693580805732923079166274552759539602834003331337)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_423 : Polynomial.coeff recurrence4Scalar1Left 423 = ((11481874743921516202302170479634166852776845910 * 10 ^ 70 + 1178699175480294085065914435084039575835135000503029053277294987321254) * 10 ^ 70 + 4189933263732237677157265446844914178947605976095126330153570848718749) * 10 ^ 70 + 8783967675683629535835042393585389818222873933709738153407498383749465

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_424 : Polynomial.coeff recurrence4Scalar1Left 424 = -(((3914663403823228204292044633680909866561209145 * 10 ^ 70 + 2553596080157661507293674855882181731270374611353986082432277846207611) * 10 ^ 70 + 570989106528106227676889898097985479741373582980236723717353619064150) * 10 ^ 70 + 3307234237222509036469599899541951082468260058078817185812007994787358)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_425 : Polynomial.coeff recurrence4Scalar1Left 425 = ((1278372127621498003456893497531497334324378763 * 10 ^ 70 + 7254472650410482461200304417954883076615316805277582380453341455389521) * 10 ^ 70 + 7408983869057327636061937179926488988616130997670717205879135223382317) * 10 ^ 70 + 3587970728232440711378235027570001689297850861633746163600141222564702