Recurrence 4 lookup certificate: Scalar0Exceptional 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.recurrence4Scalar0Exceptional_coeff_383 : Polynomial.coeff recurrence4Scalar0Exceptional 383 = ((2919565769158562813058025795282273593010842801655141831373196635653 * 10 ^ 70 + 6781042312348921644263684375109326191629131205799810161202505883747314) * 10 ^ 70 + 5242182512604009853018421152756166817491159004575942267231841490841318) * 10 ^ 70 + 4601303656930032057286025043220942708285334398323036083906149371696184

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_384 : Polynomial.coeff recurrence4Scalar0Exceptional 384 = -(((913370038555173607291592776420133527380361862449176569574295862813 * 10 ^ 70 + 9026440678182052568168088732946512513838914165575504016297137715120858) * 10 ^ 70 + 4300258203429420260957054453827844879922529409135742064525925430547750) * 10 ^ 70 + 4907057157737819915680697076032523877005718154890255463940621032458307)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_385 : Polynomial.coeff recurrence4Scalar0Exceptional 385 = ((264675978510108061945619102098425634702557566582666797965092612053 * 10 ^ 70 + 1701809027695076227612377435888357350112449694067057189315334156655434) * 10 ^ 70 + 1330298123737394942288750789444952682616799619062641817536097690375116) * 10 ^ 70 + 6324546274097283103035316328728673874598050247806058129199559222760090

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_386 : Polynomial.coeff recurrence4Scalar0Exceptional 386 = -(((67161255084639831352654709474242085600100521076191232688025677609 * 10 ^ 70 + 2150408919662318078005286794028297361508534778775450751651791585527689) * 10 ^ 70 + 3712508634535624249118325635046179397784083738133242108867377808912344) * 10 ^ 70 + 4300659847609106584732727082966713179263786965152623660287706573332822)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_387 : Polynomial.coeff recurrence4Scalar0Exceptional 387 = ((12318067720325663217717192384298010743203417509339973308707180728 * 10 ^ 70 + 1809003984699393489096165558963131832991895133988989530118019772587555) * 10 ^ 70 + 987086760838507699384975566642261492987469321195772636003054394543164) * 10 ^ 70 + 7386193477757194606959344540236525030714846401186957618905428599978100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_388 : Polynomial.coeff recurrence4Scalar0Exceptional 388 = ((439450911622108481163168638789224874957658493364663506404642412 * 10 ^ 70 + 8291159864489283917987078597583920363868726489304659434268317157821413) * 10 ^ 70 + 6134109076174107213201731673938472463074828758885565648554230424140614) * 10 ^ 70 + 1591571630154338629065950882781147133425346232851575062268470861217301

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_389 : Polynomial.coeff recurrence4Scalar0Exceptional 389 = -(((2125061311278028056007634144219208412120591339726278909211531235 * 10 ^ 70 + 993497641190071606012565591467039417969784004052258485291816497126619) * 10 ^ 70 + 1749518360221104617707929514663554495419303591949136352531696124881964) * 10 ^ 70 + 377147497971061791046048415912102110291607437594905826373125469409977)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_390 : Polynomial.coeff recurrence4Scalar0Exceptional 390 = ((1547023521898412124987622246629109326664102912309121044604812375 * 10 ^ 70 + 6439688718851077328904686880974684817660375906917888168140650813468953) * 10 ^ 70 + 1165862781636538620906779169791072732140213227025145310674863037362742) * 10 ^ 70 + 7565327504228419763021468057022267182340148412751315754518094526267994

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_391 : Polynomial.coeff recurrence4Scalar0Exceptional 391 = -(((863084717939008600617460282297558685211272669000345261694009073 * 10 ^ 70 + 8543724367320939185540323604298506944123635615194069928441502867520825) * 10 ^ 70 + 6613914450570770085980696278805531739975817379508233783738621884900545) * 10 ^ 70 + 6884404395310645925404233308092606611894652106827093303960652213164759)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_392 : Polynomial.coeff recurrence4Scalar0Exceptional 392 = ((428268428430636607221713386100727984115867684304687225873840778 * 10 ^ 70 + 7217158120476847536499039378426969857468303760273710894541085466312735) * 10 ^ 70 + 6739312527415422200526188589016909995917209626562141991720042747135765) * 10 ^ 70 + 5263338391809783269167824508555182701271701303492633914940484770211549

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_393 : Polynomial.coeff recurrence4Scalar0Exceptional 393 = -(((198144106803240498493910231916807951143894185355742487486729687 * 10 ^ 70 + 6307576873969791272157149739119835250392743418916912507793892987120867) * 10 ^ 70 + 9235710054964509124904289496481553137319642978874245164426671760606226) * 10 ^ 70 + 6016951656228732031167993303366172216368846899047640076613486469333764)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_394 : Polynomial.coeff recurrence4Scalar0Exceptional 394 = ((87194189753242267344778127737400194185512149840341846759122242 * 10 ^ 70 + 7666770027797713515713990268979101456940188652654950568247965660630987) * 10 ^ 70 + 123284878106581886966804116119981473161877277625904967607466668666980) * 10 ^ 70 + 2029602286463685398116709329844054932598313056793060917132101557565171

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_395 : Polynomial.coeff recurrence4Scalar0Exceptional 395 = -(((36836939858499763031492268402575909562417717070092242019331304 * 10 ^ 70 + 6601371933361982830979236378720283576337325614519225826863308424597453) * 10 ^ 70 + 1548640633596147625476289510253805725590617213291720008637035278281295) * 10 ^ 70 + 2648107340378630138632965773150273689702242259675045416066283377189966)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_396 : Polynomial.coeff recurrence4Scalar0Exceptional 396 = ((15006198071976899846264206847904360125664204484849982446184079 * 10 ^ 70 + 7554813952905870777877540390490463655201421178152560560602974449243298) * 10 ^ 70 + 609344586134426207315745812838701520891222222391445334278448110134323) * 10 ^ 70 + 6868205813264710695743786763775935388991272776948822610946571375145259

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_397 : Polynomial.coeff recurrence4Scalar0Exceptional 397 = -(((5905024101016281589885655714649369824332039437584014308473540 * 10 ^ 70 + 322412465620490837005312777937592772375131669094312015341234679672508) * 10 ^ 70 + 2500519279196940825790148142936093403368452322525078311104350709567107) * 10 ^ 70 + 6426389985025487949205113974310943638825895004792396452866864303628617)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_398 : Polynomial.coeff recurrence4Scalar0Exceptional 398 = ((2245190846666701396880516264608477357443643852488110305527395 * 10 ^ 70 + 1988026638200221967447848112009497068827928648880189547426724691039406) * 10 ^ 70 + 7403654926824099440042327511479258633274820371780553832763559264176193) * 10 ^ 70 + 3792023890827648999911993225464730923951772426841109207414581682784747

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_399 : Polynomial.coeff recurrence4Scalar0Exceptional 399 = -(((824224341784308549150839624778418360342764172586214636381911 * 10 ^ 70 + 5179904009111190423679925119067735251326354361178012819871738415224678) * 10 ^ 70 + 8919196221214386780638517950365839954346306396763503415015452468698674) * 10 ^ 70 + 7830086282971854364036460723415753542632777103236501783683257766288327)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_400 : Polynomial.coeff recurrence4Scalar0Exceptional 400 = ((291688056471747539365504019307918408632507601770146061695958 * 10 ^ 70 + 1641694399562226279499067221447318040303997124319947327651964712195312) * 10 ^ 70 + 6260632585784917494787138197523938267804359113408004270482115060907281) * 10 ^ 70 + 6641171563958209557922589395717043947271527955390350730551136622773811

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_401 : Polynomial.coeff recurrence4Scalar0Exceptional 401 = -(((99267862433742878256314488153424967108461221681865263371543 * 10 ^ 70 + 7789319832613701900033194163087448004092466562884988969625251803018253) * 10 ^ 70 + 6507926002446329229420600514142964158595110945800117629805832676052608) * 10 ^ 70 + 7122269864396937570101882629375774232546783335260992106980325094347931)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_402 : Polynomial.coeff recurrence4Scalar0Exceptional 402 = ((32369517259994684267100203166578665870605181006507846417215 * 10 ^ 70 + 5726648651336674389933793660985007420347795380668830526463105006919048) * 10 ^ 70 + 7539979525080036118094297314911851084509966154798481401821515746652483) * 10 ^ 70 + 4475117514801611267314410391855836305187295798990728540706241978502985

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_403 : Polynomial.coeff recurrence4Scalar0Exceptional 403 = -(((10058181286183665705929499482678015471464989009489148380436 * 10 ^ 70 + 1482992689889331876585373012457056067618139513112082779947379877197207) * 10 ^ 70 + 8130234326871854785262711768016043604709880439124525856476978276137717) * 10 ^ 70 + 8433626844911275607638585678063143507082848791798511547928709998577154)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_404 : Polynomial.coeff recurrence4Scalar0Exceptional 404 = ((2952425382095459376634911087538508073355704431144642245831 * 10 ^ 70 + 5814492228497546278037539691326375130562507303596389796924494553896945) * 10 ^ 70 + 9823783795153560062028293866474487929203427314161973648922032806004942) * 10 ^ 70 + 9059609609510594079668862890612457112257260623662319188542196669416197

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_405 : Polynomial.coeff recurrence4Scalar0Exceptional 405 = -(((806512980834959615071994046837369641344707270362128071325 * 10 ^ 70 + 6039255677105156956081846172686318975829621257303193755726961974681354) * 10 ^ 70 + 5096643903451295883664500516844518426521128752079825744589983538347752) * 10 ^ 70 + 6079321096498433162676609184897686468691909392477527396546843235202239)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_406 : Polynomial.coeff recurrence4Scalar0Exceptional 406 = ((199133213144971282295259157492176301610433857504525026140 * 10 ^ 70 + 3561735705411140645028417636246099325447667115814619114764501871136335) * 10 ^ 70 + 2678757448993217814463159895569453023912718728377033501590556000414173) * 10 ^ 70 + 7261975360774606870534222768364646868759993756904368760475333573509835