Recurrence 4 lookup certificate: Scalar2First 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.recurrence4Scalar2First_coeff_97 : Polynomial.coeff recurrence4Scalar2First 97 = -(((793002079636751589880 * 10 ^ 70 + 6226446904921482154246441899495286479106337874660871925804306854040425) * 10 ^ 70 + 7141171002155770739689637384211797635117412991256930406664520075406350) * 10 ^ 70 + 6854889498314410385649581734132301162371098115047284827221918243304771)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_98 : Polynomial.coeff recurrence4Scalar2First 98 = ((11164273970878402524102 * 10 ^ 70 + 1921769159879135742846409374729525683742156495400060057683438851734969) * 10 ^ 70 + 2561095813780822410357362660601712033658358592030541906691878646357771) * 10 ^ 70 + 4439725743766677657019645824216376072632135681155024722224716085194001

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_99 : Polynomial.coeff recurrence4Scalar2First 99 = -(((151308054254171207330272 * 10 ^ 70 + 5743014546228431946532467207034704007057827875259380366797099863814550) * 10 ^ 70 + 6222135319923453222336748945017186473850027991187954048371597693852024) * 10 ^ 70 + 7101066678318082924919656850522718922017864669743348273972754936198731)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_100 : Polynomial.coeff recurrence4Scalar2First 100 = ((1978604970356656715082848 * 10 ^ 70 + 3814168001645782444988866185798336529651899364130275214700515883102186) * 10 ^ 70 + 101137424090048117889448761201428823905439464520090965152272486801686) * 10 ^ 70 + 2588730837042123496508862624335158424317299514475709808418130028328877

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_101 : Polynomial.coeff recurrence4Scalar2First 101 = -(((25009811111052228783191030 * 10 ^ 70 + 28480890408609195817497510150233314474522960262145579887866761961108) * 10 ^ 70 + 4960206990619198657657612444406061679585120009362620964827769355197630) * 10 ^ 70 + 8443036182621360320675184678113760270605250627886643035781687735949362)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_102 : Polynomial.coeff recurrence4Scalar2First 102 = ((306028081568229815756907603 * 10 ^ 70 + 5657248494790005871967944382883896211961067226350030295108821261338590) * 10 ^ 70 + 8079565969275609274871480803748483851671261019816031423120819839583660) * 10 ^ 70 + 9004033063424695728942866484412847651617948786605707214564154180416974

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_103 : Polynomial.coeff recurrence4Scalar2First 103 = -(((3629539404924567344489184055 * 10 ^ 70 + 8974521800616857378585176412793624010361239371606687169333584689607225) * 10 ^ 70 + 3906163819205710540671904691603011696877615522248755571552522050759146) * 10 ^ 70 + 3161698367540579725860692798226409921511581985999324554321750398064423)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_104 : Polynomial.coeff recurrence4Scalar2First 104 = ((41767776708383139998818475053 * 10 ^ 70 + 9471375059285673927374330589794691751186595392193242032021216327376997) * 10 ^ 70 + 1967797138278335725673561970800682404762561888296784206781395713092387) * 10 ^ 70 + 6191272195407570574926585048567572263466336673162025703040063648669727

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_105 : Polynomial.coeff recurrence4Scalar2First 105 = -(((466798692824878348366852732033 * 10 ^ 70 + 6360348727229808144705470410196859144928546506756649157885865909579006) * 10 ^ 70 + 9094853635803137563062610068197486971237055401367023429327029452417969) * 10 ^ 70 + 9936426270323296108281877275411803372402697034190152834866642648974282)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_106 : Polynomial.coeff recurrence4Scalar2First 106 = ((5070687082214435352188156503249 * 10 ^ 70 + 5116425822926958983275431222810887065996559177550649614254978192236133) * 10 ^ 70 + 5615615100078493727473127382787633821964418522677998260927838848536187) * 10 ^ 70 + 2617860655406078224230199240956421701699128968195799016559651454059012

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_107 : Polynomial.coeff recurrence4Scalar2First 107 = -(((53575303667442805796331375514617 * 10 ^ 70 + 9865485424475993500360564104988513540312380913612598852742288873282571) * 10 ^ 70 + 4773545145308252854790677592241194606318811338116492340745250098783153) * 10 ^ 70 + 553841898319413381590593361974504544587162747397013742140604765797690)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_108 : Polynomial.coeff recurrence4Scalar2First 108 = ((550938790015510281724155928536395 * 10 ^ 70 + 6379231919475036893729747999612005204493127984574936085613518170982824) * 10 ^ 70 + 9710720105353791826562678013526679947321981994871406439367227305142875) * 10 ^ 70 + 8146735515933922090601447427016086922078783545014097616805816688073747

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_109 : Polynomial.coeff recurrence4Scalar2First 109 = -(((5517434129952467743848996869119072 * 10 ^ 70 + 6986813225781040218815809940773831709098750799109388254217294830070963) * 10 ^ 70 + 535002345244826402998495229610255098842530682132452643234168150058877) * 10 ^ 70 + 1699075320530413516098114882903946904960411464961719505396523684908328)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_110 : Polynomial.coeff recurrence4Scalar2First 110 = ((53839192640011075703156528932112171 * 10 ^ 70 + 1300280763332949319277807017101971818867630810235477645244526616807159) * 10 ^ 70 + 6535362418241488410629751154042531081843233509682426846114158594989247) * 10 ^ 70 + 8936625251888109251006176113341983284641941962348302963591650382211301

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_111 : Polynomial.coeff recurrence4Scalar2First 111 = -(((512155208759918027906941103513909716 * 10 ^ 70 + 6454465553577528908526734040525881320027010638336460470882251275269379) * 10 ^ 70 + 3177581982057558163997789924931038458929425313426456824675970646110204) * 10 ^ 70 + 2482824558546644326344460274256900576309925091388348242133481105764277)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_112 : Polynomial.coeff recurrence4Scalar2First 112 = ((4751652961854533575847637468301158515 * 10 ^ 70 + 4501466192172408468620688165712376849501938260079374608010753169902702) * 10 ^ 70 + 6747172158203600053861699421895654123411051647496834110675545980228640) * 10 ^ 70 + 7547922677970313959416000351058155257564505867225974876251933956538763

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_113 : Polynomial.coeff recurrence4Scalar2First 113 = -(((43014288004510307670418219616728530443 * 10 ^ 70 + 8606276728599619522540940243448843979908544957176296208048110506205922) * 10 ^ 70 + 3185998111579768139768572400922895920118645911601804368755079049885662) * 10 ^ 70 + 8654810483318236092009901810341687346221600818235845892949677630625182)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_114 : Polynomial.coeff recurrence4Scalar2First 114 = ((380083228766319827272342637618852446349 * 10 ^ 70 + 7957298824505523798519969014035016835306620868680226217147203569474556) * 10 ^ 70 + 4440864405504117200759706746172918833609068018688088639075937935170440) * 10 ^ 70 + 9557695961958347299102558910751121873472346013654059084044230005555294

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_115 : Polynomial.coeff recurrence4Scalar2First 115 = -(((3279482372270865503740212175211301606536 * 10 ^ 70 + 6823401925598304644335716898629413646561331150801781675745039157540927) * 10 ^ 70 + 27385259463964976659736175260340516460529750072829839934451802169482) * 10 ^ 70 + 7515485291531929275594691830472308501888759903320781185817975283227207)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_116 : Polynomial.coeff recurrence4Scalar2First 116 = ((27640509303993290184067007620558686727634 * 10 ^ 70 + 6002831394901258825309478708006179017632084825161044121037214561259719) * 10 ^ 70 + 4252180409485042606450455121651338717330068967800440454283934715620242) * 10 ^ 70 + 2499775454375745495658316505128555954885022130720100685257662645362300

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_117 : Polynomial.coeff recurrence4Scalar2First 117 = -(((227638798662496372143824359626763728730367 * 10 ^ 70 + 4223287312499776397837419784200683932280678417584586522976604296586912) * 10 ^ 70 + 7276203685413630562746141776355988644177881847662330870344130355857436) * 10 ^ 70 + 1246576338056323358504955843261671600376520188789341387604681074257527)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_118 : Polynomial.coeff recurrence4Scalar2First 118 = ((1832500366179318300894875569787411690800673 * 10 ^ 70 + 656618228847497190475259836876301391893904728052728849956784631199168) * 10 ^ 70 + 5179594927571751124049740272992257864861271690562299377461982929396778) * 10 ^ 70 + 7481386604935521915189942023474567538290047936379490207743432902904665

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_119 : Polynomial.coeff recurrence4Scalar2First 119 = -(((14423505644739122673251302835568060959482968 * 10 ^ 70 + 2192623148635371372784625229273836037287306292823716924139054392424493) * 10 ^ 70 + 4368719574329232693698468927330509579617032410187981696171761537267577) * 10 ^ 70 + 2201844691037362372600496949423968856117885389698958461087270561333056)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_120 : Polynomial.coeff recurrence4Scalar2First 120 = ((111032980958396456718229287344956724038802617 * 10 ^ 70 + 4536964986726047158054179813773534499727342612080614986739350442997932) * 10 ^ 70 + 5644081409639561767583683743863623379406385702088471809796037373537988) * 10 ^ 70 + 2247799284370231683115967481118763367804711068469714993402754368672520

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_121 : Polynomial.coeff recurrence4Scalar2First 121 = -(((836194973345270414596752357437001786473306752 * 10 ^ 70 + 5742718769263194876626164117936885316541365717244021173075036027400310) * 10 ^ 70 + 4082203680384724872901475884635853422005049350459211364196490994903847) * 10 ^ 70 + 7102586033154938012887580537661278663302075754752346709855875308376583)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_122 : Polynomial.coeff recurrence4Scalar2First 122 = ((6162436300665298414933358003318706547799071911 * 10 ^ 70 + 958915335221186282981270647007241621436021906913997715104407043059085) * 10 ^ 70 + 6715941884270263927272804575350000986951936596293311746955570654146164) * 10 ^ 70 + 7596491814881642844144086273556135565548114961292862653207578448558930

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_123 : Polynomial.coeff recurrence4Scalar2First 123 = -(((44452583723260221616531704658261803350476805995 * 10 ^ 70 + 6312084708390738860497410515832823514880839013777815236193685142073180) * 10 ^ 70 + 9417743259962563962974055656938793108559045754976474722481058230283693) * 10 ^ 70 + 4341736800113611833633508903134172361569775458693570325179636836709526)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_124 : Polynomial.coeff recurrence4Scalar2First 124 = ((313940476497281691617482364392623943830638781683 * 10 ^ 70 + 7876925828739994806013583604438750558061142719600913964252772610095356) * 10 ^ 70 + 3356382867540870497669522043641068344106508281391744983758480915579173) * 10 ^ 70 + 5787876913321114998273886227330324252355540552867785668029903404144362

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_125 : Polynomial.coeff recurrence4Scalar2First 125 = -(((2171228104549292761457640894452265310819507532537 * 10 ^ 70 + 8298725122642024022172816262521075293963522935937172314479629044028307) * 10 ^ 70 + 9705891930972056078021510641743272189341548678071504453759517802874989) * 10 ^ 70 + 5038863787171140624065700833663033062362026161781364970280736733815562)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_126 : Polynomial.coeff recurrence4Scalar2First 126 = ((14708548593952892688182925718433744392328080377304 * 10 ^ 70 + 8380171270853059882544667009197285407197800971952386585550740935164793) * 10 ^ 70 + 633011169954210512926774486926619311593451873901871833338875271333553) * 10 ^ 70 + 4623610952744324467739170592950502266132910396686618181640253212224192

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_127 : Polynomial.coeff recurrence4Scalar2First 127 = -(((97619223485029929144740021790225189675296752263142 * 10 ^ 70 + 1841446227946086234546296025715877917047969936571122297459328300088248) * 10 ^ 70 + 220739026259856018930579989196142059625898594329760396533217998970784) * 10 ^ 70 + 7885729085437381765326813996005555496003583389418329988285202716125649)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_128 : Polynomial.coeff recurrence4Scalar2First 128 = ((634883033694283842744973292531394938054807029222850 * 10 ^ 70 + 4964855201696430211823243280347740443019519271170580982578740970293013) * 10 ^ 70 + 863505840861485352504259608200133316111233624386603533257324140800133) * 10 ^ 70 + 8418016911015437071772754897171099767481038874674680401365311606511960

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_129 : Polynomial.coeff recurrence4Scalar2First 129 = -(((4047003310093983672198701491894589628715421853284332 * 10 ^ 70 + 188206742192678479119755150956844415120525338356987687978941316360225) * 10 ^ 70 + 139829979381376187559357222238239480818443653012405770096874144718959) * 10 ^ 70 + 5174661622291250387268070909832835105316209590345460952495231555415682)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_130 : Polynomial.coeff recurrence4Scalar2First 130 = ((25289520559213851905682441535049970912584801560364978 * 10 ^ 70 + 1972131869418955341368714177087158706133126039801970574387444230441752) * 10 ^ 70 + 7276151006559253998684080495550065464133826057374368519827539505253727) * 10 ^ 70 + 7758488534966238526541329495457550675498086482476700165502496455021148

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_131 : Polynomial.coeff recurrence4Scalar2First 131 = -(((154952228859783351879638014195994713256399153526952415 * 10 ^ 70 + 4731894644611948038431658108202174650296533244947269889151161985301128) * 10 ^ 70 + 9208963794609308104215473683925468257118576507176022130589930315450046) * 10 ^ 70 + 3875005583284796125950427242035735821257431841326828318590674026917375)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_132 : Polynomial.coeff recurrence4Scalar2First 132 = ((931077120897260846760369980279347068685350624354172526 * 10 ^ 70 + 2846443707838045269225266384458180639937023981235616673940599613871363) * 10 ^ 70 + 1728936072130642332394193820449401999871828794073603913944001927981523) * 10 ^ 70 + 6883815667361098006609472407045865209214118023459571623631492384269024

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_133 : Polynomial.coeff recurrence4Scalar2First 133 = -(((5487594463700305956490617437546322021709208934805893394 * 10 ^ 70 + 1574945112663054724364136989651274226477704484918188532283261061082692) * 10 ^ 70 + 1079216917411747016369990829510240795588150723634299048263523356228330) * 10 ^ 70 + 8002481367685814488295967792267615993116577133896759200348832273921117)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_134 : Polynomial.coeff recurrence4Scalar2First 134 = ((31729444393711154060335902250989777163795506580744006932 * 10 ^ 70 + 8789745041461197944927477647304204811962087156596944138286289673662909) * 10 ^ 70 + 7262921013253163253407819825859768878556803235969372530647890654675817) * 10 ^ 70 + 413510834644384320450876390966784362102682308125478715063478903900280