Recurrence 4 lookup certificate: Scalar2Exceptional 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.recurrence4Scalar2Exceptional_coeff_156 : Polynomial.coeff recurrence4Scalar2Exceptional 156 = ((1722259135545036965485700821697737843982490184934162581007940074447 * 10 ^ 70 + 6811056538803431677431797528520122182743981085784532096243686402452094) * 10 ^ 70 + 2668500848265753204204003447219923111333294302033643962990112738422919) * 10 ^ 70 + 8631385474181592202173712311236115990661462978345812975741522586359462

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_157 : Polynomial.coeff recurrence4Scalar2Exceptional 157 = -(((8055461561816930350060230587872914250993279417105110613501924514269 * 10 ^ 70 + 3073297390800499263213544292574947330063580556299971065459420836268476) * 10 ^ 70 + 9955559479253172002778646483485848377534545025996125929074444992243853) * 10 ^ 70 + 6138818425309348462735893416228424543725933727594806687303324968347757)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_158 : Polynomial.coeff recurrence4Scalar2Exceptional 158 = ((36627931567446415925870379175426356347695921972229957038783427791321 * 10 ^ 70 + 1898775168870756515523575930446160305700602681981982010118823711409842) * 10 ^ 70 + 7045558622201339584077457089787017126463503929545770575674703489402252) * 10 ^ 70 + 6760298751173509657061469528741749732734958106607110001257733177963418

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_159 : Polynomial.coeff recurrence4Scalar2Exceptional 159 = -(((162188294292405448151619045943957618250051850147926261986054451502848 * 10 ^ 70 + 1534456939562918056087946659792306774766366924169072012456285884057656) * 10 ^ 70 + 2869954739844330160867042425559629213419271003734436282659869580804191) * 10 ^ 70 + 4674414553707042654106624089364379927884863742284796070171192454181862)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_160 : Polynomial.coeff recurrence4Scalar2Exceptional 160 = ((700350963692292927235116953119812969796164495223207637521014422959219 * 10 ^ 70 + 272493403961464829392064644052579945178834176396494807455160029299181) * 10 ^ 70 + 4016538931501973024857940179283319131294925498287142093719164959115470) * 10 ^ 70 + 1269405878420326488253527766461772748353930619122122303042531757763654

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_161 : Polynomial.coeff recurrence4Scalar2Exceptional 161 = -(((2952532251417406813919199672273361711740457272815812808169844741859256 * 10 ^ 70 + 637997563060357737321714483104106032170593085485080811568792052971119) * 10 ^ 70 + 9504635598263614385318083236221277259587874592879705257151089194465792) * 10 ^ 70 + 3455447938307155120138709364823502841760648136965689465686861878206232)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_162 : Polynomial.coeff recurrence4Scalar2Exceptional 162 = (((1 * 10 ^ 70 + 2163739060476377649190827049754798401534957609548664388042989593974849) * 10 ^ 70 + 8399344061660895978758876635352406009005711823021385315184395360712861) * 10 ^ 70 + 4634402508760249658199238239103406226016865601961932360970125906341841) * 10 ^ 70 + 8173502665298202669607193613266630828922929827067621671741177499263581

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_163 : Polynomial.coeff recurrence4Scalar2Exceptional 163 = -((((4 * 10 ^ 70 + 9009518814919973647702218408697136128254768462386784387519121600839608) * 10 ^ 70 + 7657510209451392159980526243946388487219281735630381594968505469597141) * 10 ^ 70 + 3704160711014890144895610391881957577952628233575420611484086836181978) * 10 ^ 70 + 2418360111317584460148191615915995550016148895759513599535136356685946)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_164 : Polynomial.coeff recurrence4Scalar2Exceptional 164 = (((19 * 10 ^ 70 + 3255755805755568321964619687689993685080702664832526841546579735699993) * 10 ^ 70 + 5909392365587311279763803050927471465853702610358925761155452622123193) * 10 ^ 70 + 7787746812923047669933654786310944773512172035613368219396061938208404) * 10 ^ 70 + 6034852014569982126100459083469401485362729695428687607886141210252030

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_165 : Polynomial.coeff recurrence4Scalar2Exceptional 165 = -((((74 * 10 ^ 70 + 6244912814153207939166767276649666369462014288396761090131825656314390) * 10 ^ 70 + 484328633290945420809144089938097833753532861829383262298387909637546) * 10 ^ 70 + 7480206837548950212938853884521903391702991244389887183036853926003808) * 10 ^ 70 + 8995043428369492258039253871207128102072309572815158307083472247213423)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_166 : Polynomial.coeff recurrence4Scalar2Exceptional 166 = (((282 * 10 ^ 70 + 3278371783672948558440410806241948679515803594928100197463513877244875) * 10 ^ 70 + 9508025098745724312445380816859995746611754666826419643408633302435049) * 10 ^ 70 + 1166614821521169848298820728731758681302425464235276499254603803021651) * 10 ^ 70 + 5896547139538353751916537970453167239588081766900969789917996587731543

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_167 : Polynomial.coeff recurrence4Scalar2Exceptional 167 = -((((1047 * 10 ^ 70 + 73625659785096636694516858936430928563169810965533606217585898574106) * 10 ^ 70 + 4767338013895144320148357122588553676483191267717743103306168248856819) * 10 ^ 70 + 594183905912587543816820865824147125755969911947853496301680668813232) * 10 ^ 70 + 7747433094364067302439963824008936455206077744725664642339245624366635)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_168 : Polynomial.coeff recurrence4Scalar2Exceptional 168 = (((3807 * 10 ^ 70 + 5729388105632386429635630372500517596761234887584439237081148353254255) * 10 ^ 70 + 696800221374688617803351714274265791517661417566170729601993100338513) * 10 ^ 70 + 412433223907696388114512298524358901521465938549865651288620691179286) * 10 ^ 70 + 8615886495320057233370954176215983181190696407532184500471541112637380

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_169 : Polynomial.coeff recurrence4Scalar2Exceptional 169 = -((((13583 * 10 ^ 70 + 4424579556015367743350623456487396137357980925630456254950693281823533) * 10 ^ 70 + 2316835539905878783424153063409543322286197697241746531391926086975646) * 10 ^ 70 + 1400103747962177572347713426488900241975310340680018806058079948846280) * 10 ^ 70 + 3982036360470028784336275927100101584356162936682574217789245448589007)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_170 : Polynomial.coeff recurrence4Scalar2Exceptional 170 = (((47553 * 10 ^ 70 + 2220994723261192011692887853339704573680505875829218050542356277562913) * 10 ^ 70 + 9218512678045580667247258863456900415163810287798390041073642605387529) * 10 ^ 70 + 8741538943289003306708330920975340098897385576261250249369840255378242) * 10 ^ 70 + 3965949166934063983357155836326589778684802775582200577507239009376763

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_171 : Polynomial.coeff recurrence4Scalar2Exceptional 171 = -((((163414 * 10 ^ 70 + 6004053180166700852612354139335643410055316199703796973310610974031049) * 10 ^ 70 + 9879895821765674746153260658143836705620596759672654740049882158317405) * 10 ^ 70 + 573240814162563755516716703156378230621442605706193247027349709385313) * 10 ^ 70 + 9608354891012069593990838037795763218925065067322036468380624001842070)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_172 : Polynomial.coeff recurrence4Scalar2Exceptional 172 = (((551396 * 10 ^ 70 + 703895529524587799773634977507865573411059695803474757728793339129217) * 10 ^ 70 + 7685198737419972888176657669745866774700288952652130971335698673586794) * 10 ^ 70 + 7119555004691952230287920251258105611687103064816435950491288930544139) * 10 ^ 70 + 825908523667952532951917355783753103705099914663548037386443981698531

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_173 : Polynomial.coeff recurrence4Scalar2Exceptional 173 = -((((1827299 * 10 ^ 70 + 5734634264984774300750296381285628831639769087230226114024718496199261) * 10 ^ 70 + 9260756396416742038321997943867006540811771302335829427311275426440190) * 10 ^ 70 + 6726267797386846821782920458974282903156508461473241315360262524082711) * 10 ^ 70 + 281450409469535502840286801337317142598927695359895636278175388988459)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_174 : Polynomial.coeff recurrence4Scalar2Exceptional 174 = (((5948836 * 10 ^ 70 + 575136993967327713928513665666437166535284530424358195512018010901178) * 10 ^ 70 + 9927122372702913091408098291218235838289481083657165044539607604754579) * 10 ^ 70 + 6304218670289311021783125313467302726414936875698395661343979775615378) * 10 ^ 70 + 451494513671293198798531305744287243627868721296422314029813433056568

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_175 : Polynomial.coeff recurrence4Scalar2Exceptional 175 = -((((19029432 * 10 ^ 70 + 7057053502472431358669866419124279125143535448803784323117137103218008) * 10 ^ 70 + 7506510315719996097340358577134331390309710837036529279832712725515953) * 10 ^ 70 + 3435362414895130125650788450487552021309048215786472894503114186262357) * 10 ^ 70 + 8024551461840622121177031574613569781590893831648726277757243733435304)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_176 : Polynomial.coeff recurrence4Scalar2Exceptional 176 = (((59824643 * 10 ^ 70 + 9014127613439362602996511784313605796887616695828797061625774295779911) * 10 ^ 70 + 6000739631479282634429144980920580396407101145399635140756818890830411) * 10 ^ 70 + 7385267157814157175786512958574064423018811076789043072160840819918571) * 10 ^ 70 + 2947987048509576346604698056786523124410427429061009417220675213956146

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_177 : Polynomial.coeff recurrence4Scalar2Exceptional 177 = -((((184874851 * 10 ^ 70 + 1397560954452565045602231282545624862743884740453793652108854910671543) * 10 ^ 70 + 1611462456822520716822006854717282488795303037204820519998573041396229) * 10 ^ 70 + 7527160284864705631309169510941810621991223159521811466295435654253945) * 10 ^ 70 + 6786961978350647113539403952496816537543835792433845588209707898473808)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_178 : Polynomial.coeff recurrence4Scalar2Exceptional 178 = (((561690082 * 10 ^ 70 + 5753439799514767594413001478968882328187400407965206943143454406038529) * 10 ^ 70 + 6736640503751373799891069034898284849582682639141583752417981347333672) * 10 ^ 70 + 9136146927863241164601761823738346272451902040123184702299139564982730) * 10 ^ 70 + 1447721322995461645203162231630115821687245564175385389877382233863470

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_179 : Polynomial.coeff recurrence4Scalar2Exceptional 179 = -((((1678069550 * 10 ^ 70 + 1217977835117642974628362923987882545013015830005741356716812415201180) * 10 ^ 70 + 712462090676044977764278702919023055575660876962835209525579555606312) * 10 ^ 70 + 6003668606347342359621607168723799963762061255824941594785456883962942) * 10 ^ 70 + 5887126239437383897080727599700613677251020537195706790314303884684254)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_180 : Polynomial.coeff recurrence4Scalar2Exceptional 180 = (((4930446955 * 10 ^ 70 + 7528034215561882967993344203594773107281223610822219048955825084843457) * 10 ^ 70 + 3689307978798681775554397091078186244159779037862920475518375926095811) * 10 ^ 70 + 4886262717855415582592439009027085522310691327346041593052347982688091) * 10 ^ 70 + 3658301984094967170235891136904759425906809495503331250445069155793661

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_181 : Polynomial.coeff recurrence4Scalar2Exceptional 181 = -((((14249209752 * 10 ^ 70 + 3373362824966456488137290064891093891402138692311654979631656372976129) * 10 ^ 70 + 9681131063173580988134432866708437633824993441836782800015701991990585) * 10 ^ 70 + 9064088691187621494072108452997542210563991420209998011881234442360103) * 10 ^ 70 + 4264608765953278712942073357541043346678034556362053316336300777887404)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_182 : Polynomial.coeff recurrence4Scalar2Exceptional 182 = (((40512119359 * 10 ^ 70 + 8033352495717418610497701271167621601464892946295378027860022910472446) * 10 ^ 70 + 2981173889023139472011302850658098685410572990986438442191460143204851) * 10 ^ 70 + 1844163128098220592384199411768614297858537146103788884315837786452958) * 10 ^ 70 + 4153514613450980197251558529969683740048645556478239778105530714777363

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_183 : Polynomial.coeff recurrence4Scalar2Exceptional 183 = -((((113325385970 * 10 ^ 70 + 4191160573050371853531942877904284529173668586978628626064313452852899) * 10 ^ 70 + 8109579192769651805398769334175260127052172601797556055153727037993666) * 10 ^ 70 + 6608155089120149256036263975150700923257162529273106463902272338235396) * 10 ^ 70 + 1647384871867467286794497050338295530675110185849668802639008333053225)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_184 : Polynomial.coeff recurrence4Scalar2Exceptional 184 = (((311941361350 * 10 ^ 70 + 9665044890489994019514032533671295078128431632100543998400522241899116) * 10 ^ 70 + 4778541271433006276861306512813691495456851122250256518332292482766762) * 10 ^ 70 + 691845405158271011659100704766251558131548873952679321153853031802780) * 10 ^ 70 + 9449712666874256364508388099714040104071226451204711763818795472698311

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_185 : Polynomial.coeff recurrence4Scalar2Exceptional 185 = -((((845035611255 * 10 ^ 70 + 9571759636564688227554404327374923563366391351865535275351165580220501) * 10 ^ 70 + 4168487966165052983353964941426724301679119778857531461505804971938038) * 10 ^ 70 + 2903897766979820107906998342930308843187283256487389750605987010646921) * 10 ^ 70 + 5364456300769966002862595656120183466030519820168855920362076559368145)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_186 : Polynomial.coeff recurrence4Scalar2Exceptional 186 = (((2253116580848 * 10 ^ 70 + 804796284222044334732533544680367858534793123983383244913712832064302) * 10 ^ 70 + 8171967804926376691165693163074983897269337001411892580726243040075160) * 10 ^ 70 + 7160866049530463901250771925216965163074637284594082069308920405126033) * 10 ^ 70 + 5639903000732771483387439876201610037952500299948310919693119650988331

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_187 : Polynomial.coeff recurrence4Scalar2Exceptional 187 = -((((5913531994507 * 10 ^ 70 + 1051411800948125784827618662502395748863385053694427346549797412365783) * 10 ^ 70 + 135994818131020712931283537383490524291000860841007514990928678680633) * 10 ^ 70 + 7329885334462155614588990740187533682248389578854348957450215614128113) * 10 ^ 70 + 8426411434283758904333232920129736814285457690511905986724921187729948)