Recurrence 4 lookup certificate: Scalar0Main 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.recurrence4Scalar0Main_coeff_171 : Polynomial.coeff recurrence4Scalar0Main 171 = -((((211064879 * 10 ^ 70 + 2884282770989700612659821230660045042926537381599124634139719947714478) * 10 ^ 70 + 5299405183808381832602182864295884771237084758368131171778525916641680) * 10 ^ 70 + 8727281904589959421568778139740170187035195363591363811963068766170422) * 10 ^ 70 + 9836395457633544154077903351741971625094807000896728286546932899797592)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_172 : Polynomial.coeff recurrence4Scalar0Main 172 = (((664068068 * 10 ^ 70 + 4017633262548879399566535455347950287816586733848769506259572590158313) * 10 ^ 70 + 8966354000838134601536439077036271476518480403306315621457917182422576) * 10 ^ 70 + 1721431335588456187193550840608718687591295307809100720777778823636965) * 10 ^ 70 + 5867972745931681416326752020751811389661084144942881544740457932105569

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_173 : Polynomial.coeff recurrence4Scalar0Main 173 = -((((2057929878 * 10 ^ 70 + 2713453052466889376414156198837929495271046610315618359792464151887586) * 10 ^ 70 + 1516700681261110340413107176863302479529415940891620317583565902111971) * 10 ^ 70 + 4741361025878151941230467013964541237160662366271457053930276819071663) * 10 ^ 70 + 2710680092143219145665489394393298459561567586365963555797331780344191)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_174 : Polynomial.coeff recurrence4Scalar0Main 174 = (((6281946871 * 10 ^ 70 + 6139020680870891580834914470025857428421685265136752649099958513848145) * 10 ^ 70 + 8054665251944864183672135097908871493332968666042509969004549017806102) * 10 ^ 70 + 8353161230115490153335789192952528020831820481503145765142868803658564) * 10 ^ 70 + 4501013135326684081860456513437326283990171151176470630086454876506904

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_175 : Polynomial.coeff recurrence4Scalar0Main 175 = -((((18889793893 * 10 ^ 70 + 1494022126917743533287475712001402479927857294414669475507553756715491) * 10 ^ 70 + 5281051298851745489455963178994587711676739474197441841844356232767445) * 10 ^ 70 + 4884845167332668985990830425700201921648103951477181437667959474443510) * 10 ^ 70 + 539701187676484752506209045444925360774370893577952102204423148639003)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_176 : Polynomial.coeff recurrence4Scalar0Main 176 = (((55956717297 * 10 ^ 70 + 7285343159511044347885761222389740166851075455579808748738847248401676) * 10 ^ 70 + 8392013590377043804821208239561704492231493652005476693926733480656544) * 10 ^ 70 + 1474299288125640065669868644549316579034825651109228353405311542535644) * 10 ^ 70 + 2010840243212565279948336413889749045303568441338099609150394641461343

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_177 : Polynomial.coeff recurrence4Scalar0Main 177 = -((((163301918716 * 10 ^ 70 + 6931083559098371004793541775895869922874128740694680151876856972396696) * 10 ^ 70 + 5966864994257460578785710478103879633540389196217916078490832313515119) * 10 ^ 70 + 1793017809744602849447975112744355378826347032304993306826902204364180) * 10 ^ 70 + 3676365848772275618759562928579606309375049514237592813107635645074884)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_178 : Polynomial.coeff recurrence4Scalar0Main 178 = (((469532471402 * 10 ^ 70 + 2551045056302050521331923867829592835303350981795245905715247704193145) * 10 ^ 70 + 1703170115187779321904859306092665539613790891596119134412754339516592) * 10 ^ 70 + 8995118719409074830037371548771941025111825540209514321751377600091380) * 10 ^ 70 + 9217193722395576455859271766045258477495851131461165282276883480382217

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_179 : Polynomial.coeff recurrence4Scalar0Main 179 = -((((1330135070179 * 10 ^ 70 + 7407732705555773746176089728420947953412188470810839594446951913352629) * 10 ^ 70 + 8870169880694655136410748030897986642438063116626212606159701031979561) * 10 ^ 70 + 5521914122509207730025571700685044467148091337333187283482390613879511) * 10 ^ 70 + 4699694705526670689029850311142130614793147689751890281496732134243337)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_180 : Polynomial.coeff recurrence4Scalar0Main 180 = (((3712798327936 * 10 ^ 70 + 4714855909957873925141471779552320319077821863878403520688622185856576) * 10 ^ 70 + 5686043860858010629663474949222939608493806663341754256335732462611076) * 10 ^ 70 + 2137882929021767663998621402938877267045848497046959987738963026923485) * 10 ^ 70 + 214094916229743744327661921360116653078820629113150559995926396601794

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_181 : Polynomial.coeff recurrence4Scalar0Main 181 = -((((10211780644685 * 10 ^ 70 + 2532955837970227602903558918058158121205838188049945938473034707766476) * 10 ^ 70 + 1718024697476316006265780207558320850898722646173637908962178965380155) * 10 ^ 70 + 9744799415484447126945366877966807292405877043535617401498742424088807) * 10 ^ 70 + 5349496516025688696572249317545466193036573188517221818348870423878632)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_182 : Polynomial.coeff recurrence4Scalar0Main 182 = (((27676703668705 * 10 ^ 70 + 9673144766593104522454515294185109213327563079648496433372765379186710) * 10 ^ 70 + 4068905692854407137209071523061912419273513630519631307401561105226712) * 10 ^ 70 + 9766022891667175867373917547720493421420002432427742402020503077083777) * 10 ^ 70 + 2641881517047474148835963294495282818913257628518654245684972659399834

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_183 : Polynomial.coeff recurrence4Scalar0Main 183 = -((((73919251594052 * 10 ^ 70 + 6240248482203528222199573574709789190136701875759902205905185684895119) * 10 ^ 70 + 6670140267795191569155126129549094470803503862440246883716491498530502) * 10 ^ 70 + 6517646137273666891488940393465802825651289232519928775164180050665992) * 10 ^ 70 + 3200214504895529924649763465660656695936791709859842044962329934888113)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_184 : Polynomial.coeff recurrence4Scalar0Main 184 = (((194557461127379 * 10 ^ 70 + 2261987150886498250005831733687511074156056806403973440492222092921649) * 10 ^ 70 + 997198763205093286248524868118318094445747835115211559449083080793547) * 10 ^ 70 + 505232153476259035066063230106269509853991688474813424862999384497072) * 10 ^ 70 + 5439151068440363795675396971009176433302550952020098172572238559265104

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_185 : Polynomial.coeff recurrence4Scalar0Main 185 = -((((504662988186083 * 10 ^ 70 + 2770640678022735384568640458746789261779029689155505748636804211506280) * 10 ^ 70 + 5714199634283612581220429149634329877613206737093054755186726994513086) * 10 ^ 70 + 1740046470835745047747479518019855615367587627218299188756923703215156) * 10 ^ 70 + 9750173830752027301106728377377766018755556844958038868785914889510994)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_186 : Polynomial.coeff recurrence4Scalar0Main 186 = (((1290130502019606 * 10 ^ 70 + 5548211989287311573374616869090137056341588358076457038464274755117154) * 10 ^ 70 + 4516948954393647845696035710328493409852729666029142904908261697695378) * 10 ^ 70 + 6281691212914850147297598271673746000812816076614261042803148924025335) * 10 ^ 70 + 2455054894824102519501787143387424485719530546007903713989320136747752

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_187 : Polynomial.coeff recurrence4Scalar0Main 187 = -((((3250567052681496 * 10 ^ 70 + 7469707432218090727650226044776506296248971897030730311486610504416127) * 10 ^ 70 + 4244791871227280064435113103473229049946036308447340494083567244885946) * 10 ^ 70 + 1068449634535842264555692437583968668030943450601496771778618406847782) * 10 ^ 70 + 2671392405878116777415793646516039965177070777967057963488423031341726)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_188 : Polynomial.coeff recurrence4Scalar0Main 188 = (((8072199214836795 * 10 ^ 70 + 986091349649898489869528490860586389538020925462054269279508299749174) * 10 ^ 70 + 8083594704750491700212297664456030564194409518651609491188490646861730) * 10 ^ 70 + 1537643144990273377609013348931778334636522295675071722654150217820446) * 10 ^ 70 + 3047285893983366818300918826488085149579581133452422479185018540842433

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_189 : Polynomial.coeff recurrence4Scalar0Main 189 = -((((19758096930368025 * 10 ^ 70 + 3945720295217417625423882147632570901838948698309220398943404987605655) * 10 ^ 70 + 5715681371374346281636096590566782073232288630278752935460230548616147) * 10 ^ 70 + 4566581541582216775504145692464667413700822416146946067478437526937593) * 10 ^ 70 + 4924975259133494741865287415120945421123970447792070342472315212942740)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_190 : Polynomial.coeff recurrence4Scalar0Main 190 = (((47668487354914659 * 10 ^ 70 + 4363169960415694993936086741112678337201362927147325996115483390942828) * 10 ^ 70 + 4081766347399922086614258109462875922916258628355887496158575699689181) * 10 ^ 70 + 5643526404257698151107557686173662974376347435776125523017971205454415) * 10 ^ 70 + 1155679832814153278723306262170613642065261556773300309849113688713312

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_191 : Polynomial.coeff recurrence4Scalar0Main 191 = -((((113360680265058367 * 10 ^ 70 + 9544264237976278036137754208743440285770113053705765346651186099164835) * 10 ^ 70 + 7877998054185577347879572284695203954443156689103517500621910648444861) * 10 ^ 70 + 533548797718882271118743604995257838766038331540196966234688817304653) * 10 ^ 70 + 8043917493810767326611716044022965506085746775378587428553489103315321)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_192 : Polynomial.coeff recurrence4Scalar0Main 192 = (((265735386165045919 * 10 ^ 70 + 664527239649192973808202371016095324998052522500011118667519270325618) * 10 ^ 70 + 7662924673698554459326967738671950149384425032042242660646603890109352) * 10 ^ 70 + 375394585178600562225671836168537505837448726870195033238015450114777) * 10 ^ 70 + 9955830374359251532157114700790097195776619945118996546641703707038810

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_193 : Polynomial.coeff recurrence4Scalar0Main 193 = -((((614048294635949066 * 10 ^ 70 + 9924134175896557999672291562429969492846105431028246314532147110789784) * 10 ^ 70 + 5331611801799382177212686745844294948005528836801087468029996213300576) * 10 ^ 70 + 2353655737146511894398713888594961812707827192914305189336587251352191) * 10 ^ 70 + 973586060603871401154605224202234556461427766714955836884081183320838)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_194 : Polynomial.coeff recurrence4Scalar0Main 194 = (((1398722061197489925 * 10 ^ 70 + 2079502289440657290425278506015077048442960588079503605683816193300538) * 10 ^ 70 + 5597636125499565809543712064184438928139295547459094784456362822817507) * 10 ^ 70 + 7259360959666181243235877451957922458650947105903700550831330532564356) * 10 ^ 70 + 9789161187000181273838543479594871841182909402624801647914695658449385

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_195 : Polynomial.coeff recurrence4Scalar0Main 195 = -((((3140833186970267696 * 10 ^ 70 + 924204124822514152391688741906551827248149613357648322742308769502104) * 10 ^ 70 + 2421791122993076465823909531237915263205414047935418408140846250383559) * 10 ^ 70 + 3675921631119613186610333834863524623476102332550136347454141883239576) * 10 ^ 70 + 1173994581752720819373236509112901066516940563910746569565349709976379)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_196 : Polynomial.coeff recurrence4Scalar0Main 196 = (((6952658187483609459 * 10 ^ 70 + 5385521098876230335893129139864763410915817158048381259468343607117393) * 10 ^ 70 + 7683266726717566451494742407959220930118116849574347320621092196284417) * 10 ^ 70 + 8367458850917709271165481234277670141357589425743114763510921470603728) * 10 ^ 70 + 921934254201562279214546272337559411690676340333495540666561565947987

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_197 : Polynomial.coeff recurrence4Scalar0Main 197 = -((((15172482772574122175 * 10 ^ 70 + 5824034310707514915446321371961250652450245963235539361461063945705220) * 10 ^ 70 + 9569118475560528329104524353489341131775867073352667560100924468974129) * 10 ^ 70 + 7609356713823998620677571272135949243711348984470854787913593461757620) * 10 ^ 70 + 9010467015010753045453626608972958741217572902823865941558953657090300)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_198 : Polynomial.coeff recurrence4Scalar0Main 198 = (((32641384560133045278 * 10 ^ 70 + 5108265418085917467333090153843851382093286117146631778727122573958594) * 10 ^ 70 + 4178690507925678749232916287144812146607069069071197128065383174140073) * 10 ^ 70 + 9874161752217659392248912643806093299524372643387677132705090085935428) * 10 ^ 70 + 6355952459165409062353408184719275563027882486083750402865630398798155