Recurrence 4 lookup certificate: Scalar1Second 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.recurrence4Scalar1Second_coeff_224 :
Polynomial.coeff recurrence4Scalar1Second 224 = (((64277762283386024630274007 * 10 ^ 70 + 1322452047003742909448253013815132128024730371949861066933901875048383) * 10 ^ 70 + 5599685200634379818561954149675881709365176691918997362430766924001557) * 10 ^ 70 + 7812194797517443167727968039637653691945247769734869308570054080759006) * 10 ^ 70 + 2262767461558108379998156927294509285144890273275409016716282565144276
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_225 :
Polynomial.coeff recurrence4Scalar1Second 225 = -((((91076374222210967959869321 * 10 ^ 70 + 3450927426020252510533026884386805681227618742904055389137383632989199) * 10 ^ 70 + 3007118090221521373402953869157588560539383975551997057501267278699794) * 10 ^ 70 + 4071665002138251637035715467847130773770835437472612354845579875547896) * 10 ^ 70 + 8365412902013762917527291161908847463507663615312569956432513481775107)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_226 :
Polynomial.coeff recurrence4Scalar1Second 226 = (((126939097136595707123571005 * 10 ^ 70 + 3139270648972654589739751272579356100549409281712629372830115226196592) * 10 ^ 70 + 3736866119204178952314633733292001602381144312152915213264751738373786) * 10 ^ 70 + 6121592754754232983306427070373470767044889789181648917549655831608139) * 10 ^ 70 + 8092524862662769952327426392384541497191045546988697961643805817125109
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_227 :
Polynomial.coeff recurrence4Scalar1Second 227 = -((((173971902796878330577499077 * 10 ^ 70 + 5552773377810021654348509478517875188089217929547697240331515752833757) * 10 ^ 70 + 3911342018719382738404709366497583125205016741854649338987034503500801) * 10 ^ 70 + 9819717167392716291304284326595675752338778089357501096128802697812933) * 10 ^ 70 + 3699952189646154403873858835277746170589573922827667230276100397473607)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_228 :
Polynomial.coeff recurrence4Scalar1Second 228 = (((234356853477826135483874636 * 10 ^ 70 + 3539764194352129067029438412117026668043265718174797546766057743269213) * 10 ^ 70 + 7563276849979084496051485323680847102856858593374940653083573479298306) * 10 ^ 70 + 3229854573796995499631571973453492298208957120056126293547515387959824) * 10 ^ 70 + 8588173426259748126071311565440547014300706762208143940381642766187467
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_229 :
Polynomial.coeff recurrence4Scalar1Second 229 = -((((310152885275789095354193712 * 10 ^ 70 + 4451444861008298595340692387379016473685073981213448857518304654598046) * 10 ^ 70 + 7698610799746807691078619204607133988267479339355668627045846529717438) * 10 ^ 70 + 9891404323569456080685350800755001319920379530165662074555344641978961) * 10 ^ 70 + 430522553844886721193800949203518059310493963586741070382608068551564)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_230 :
Polynomial.coeff recurrence4Scalar1Second 230 = (((403006694427585549340796322 * 10 ^ 70 + 1018575008626511628196290519095793819087526498121770392428148686978885) * 10 ^ 70 + 4824121993027352223681565788326970549068972399990432485492533765831214) * 10 ^ 70 + 2579547987437657844192119646688119645809213565607551060198594242689635) * 10 ^ 70 + 3757409663726274466999061762417174481634313758716850839548846265633785
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_231 :
Polynomial.coeff recurrence4Scalar1Second 231 = -((((513766109635470966579028379 * 10 ^ 70 + 5520424850600296350313584757533977548694491139135651131375106878263632) * 10 ^ 70 + 1088510791936299880908858239345114685286939661460838266179503849349429) * 10 ^ 70 + 5784664197420058592560122753787212252726806501516792867323038890539415) * 10 ^ 70 + 5785981087594299968044301532080844467927500791902433367698520952398684)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_232 :
Polynomial.coeff recurrence4Scalar1Second 232 = (((641998320526939874182553327 * 10 ^ 70 + 1217801231243217719326736912852842214898641145278174589856611659803818) * 10 ^ 70 + 6366845028954427588412325429640939765062116938269793132136172942763150) * 10 ^ 70 + 6771437382671015555141743486777260581515025754286278103481780592354992) * 10 ^ 70 + 1595350189069658184352246041061776161272781228438215550210499124134307
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_233 :
Polynomial.coeff recurrence4Scalar1Second 233 = -((((785429489373611953175291286 * 10 ^ 70 + 1610363239120786075563696675645228798582880218376416542583501680161031) * 10 ^ 70 + 6288393310833645747968141543714808076640158374595840888831671818573946) * 10 ^ 70 + 3723025175238050079841806890966271797718330904131754749155639037415430) * 10 ^ 70 + 3695095895004243447696443632481462250400143979709053086596728015952661)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_234 :
Polynomial.coeff recurrence4Scalar1Second 234 = (((939340079456755918197604905 * 10 ^ 70 + 6645156207520050684592770125438862734571456302185722953154155534996331) * 10 ^ 70 + 7919038198108294592430184629952683802128658528732990400570772815737338) * 10 ^ 70 + 7967905153879774221687550676254798639034365533894877431907808682795580) * 10 ^ 70 + 4777196536747410635045366887285349160369795208234559823813750051840380
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_235 :
Polynomial.coeff recurrence4Scalar1Second 235 = -((((1095970289739031771944113543 * 10 ^ 70 + 9665206970794944945663169899744138725585352277215566585293735127262243) * 10 ^ 70 + 7449052510009267526777206977983610790109481660387992997106186512015085) * 10 ^ 70 + 931808718557924721869452346350558337399878461680589911832858960879399) * 10 ^ 70 + 6055101342677160474768384872871684948225329097068532070183678927997171)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_236 :
Polynomial.coeff recurrence4Scalar1Second 236 = (((1244009920643576342730522621 * 10 ^ 70 + 5160197326866650062844808290407585040197248898811251416466133200144676) * 10 ^ 70 + 321718458679808528349256339914227820233242862898755520454681333236840) * 10 ^ 70 + 6027508073454682590696025241871297721060612023337200974674628613602862) * 10 ^ 70 + 3069272320083452744774131467274067065180353811744469493805203548757949
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_237 :
Polynomial.coeff recurrence4Scalar1Second 237 = -((((1368263537444817456336377991 * 10 ^ 70 + 5319846341692681785180037610975954523293396384772819845685967019200686) * 10 ^ 70 + 6073689195799005512370033857576365818533455937973666314316259763613584) * 10 ^ 70 + 1170784377463608933981878759264974238896951859612309061640618117701338) * 10 ^ 70 + 1282748360446091140451475113011670073233087333686594809431871920796080)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_238 :
Polynomial.coeff recurrence4Scalar1Second 238 = (((1449591055951173564475263054 * 10 ^ 70 + 145184157421612857410684583190146291177410196573567651464784858138876) * 10 ^ 70 + 4287976241953818000176782953211882273631588221158255850514405906002203) * 10 ^ 70 + 13228312868802223286907018940814541973319419626468181566543644382279) * 10 ^ 70 + 1746325196418603074833283258089154471843107176978675428289375241295460
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_239 :
Polynomial.coeff recurrence4Scalar1Second 239 = -((((1465221855522087376139867567 * 10 ^ 70 + 1487685909585456293282682024500538906890547905476291939728305670201731) * 10 ^ 70 + 9913795806562647749831600108971553533388127531501092829467308139502511) * 10 ^ 70 + 7303823367947728076798996268534351674096409126892527173969666616971292) * 10 ^ 70 + 6572414310768929877997028458586553016642045897223742659129441973686016)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_240 :
Polynomial.coeff recurrence4Scalar1Second 240 = (((1389523842650489374371013321 * 10 ^ 70 + 3061362134131228231120315977169402265848251803202138426375190005901978) * 10 ^ 70 + 108433820264666789410984880412076819492621797452729878612146901996547) * 10 ^ 70 + 2140540061775836399266832973408711704397440216318112700363344598746248) * 10 ^ 70 + 5552700345032441808044522905809845530878505200185281527470250472702937
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_241 :
Polynomial.coeff recurrence4Scalar1Second 241 = -((((1195275598300550181945002986 * 10 ^ 70 + 8913175191269554018492677223640611465643276368296091089250093006347326) * 10 ^ 70 + 5639448708294646011954790105433495231183120426692506035602498934646169) * 10 ^ 70 + 5368711547436805465084139996931132491340078745189919512982634317192071) * 10 ^ 70 + 4007943039215868786019399012875969447246582356992955856778210097096907)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_242 :
Polynomial.coeff recurrence4Scalar1Second 242 = (((855440137863527391265830191 * 10 ^ 70 + 5033377124702679646368677190187408059485614814051000120275927085655053) * 10 ^ 70 + 1492477539233170315294615273066911587717702740436224567059908868075136) * 10 ^ 70 + 3888730070541210819157832851135134116712686776801947735815110492728747) * 10 ^ 70 + 7351925496531537144501835225062850064995581275068990858264293414935799
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_243 :
Polynomial.coeff recurrence4Scalar1Second 243 = -((((345376024024573876194631425 * 10 ^ 70 + 3413245875767717564011493014121431064645343924828152710276153662559011) * 10 ^ 70 + 2899614108028451157819768405825213377892674321963816220663791945218599) * 10 ^ 70 + 5246135749275597907867946956451372580475920458245548399807024865462437) * 10 ^ 70 + 1134592310747257006297318433150504720531375230609828846039321994757758)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_244 :
Polynomial.coeff recurrence4Scalar1Second 244 = -((((354648228663536970965253911 * 10 ^ 70 + 9680772970910884382293570942015216920897157262671639202937432144113864) * 10 ^ 70 + 9656483321024753964074361830212645280634823087958308408826867434345094) * 10 ^ 70 + 1991297709814169772855589273262255521138558656571666634536879844204939) * 10 ^ 70 + 4769380130288690406715328897882537092133982822579830476334895513605968)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_245 :
Polynomial.coeff recurrence4Scalar1Second 245 = (((1256838455536064196204283070 * 10 ^ 70 + 1632889171082594525080000051811869338555341744568195692410090234366064) * 10 ^ 70 + 8198757633442086477845546734164083431317333376072847158271354151016782) * 10 ^ 70 + 280819813173798990896009267541786238991486965692396658279401836162759) * 10 ^ 70 + 553583974122950330473200999497839482182488393234699175725124738870460
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_246 :
Polynomial.coeff recurrence4Scalar1Second 246 = -((((2363415279367108107200506367 * 10 ^ 70 + 3920870571713899574816654316476629789827083864580715932428339456162867) * 10 ^ 70 + 4743266185176232172792917769038350216056859377083825511764701752764861) * 10 ^ 70 + 3387025644896120225976027893488998910497853945971765228560058501020239) * 10 ^ 70 + 3695420702619149137151556256041242419679121936671711929372050181855488)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_247 :
Polynomial.coeff recurrence4Scalar1Second 247 = (((3664600136572796843347730141 * 10 ^ 70 + 2759070790093154880399687280838399579551002394451896104032373623867804) * 10 ^ 70 + 4930571968157687709327869032746887989225745198660701339331492824885101) * 10 ^ 70 + 2560462626039342084622057978788324553830752666820104556611134535214366) * 10 ^ 70 + 2313724321100582025859297278998798036185266363875072133312821818816307
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_248 :
Polynomial.coeff recurrence4Scalar1Second 248 = -((((5137335670770175199745669363 * 10 ^ 70 + 8497126862502214675390080331772025245020268928898908234969380068862568) * 10 ^ 70 + 6394164550578294971641772208494069018970206940574763339525172086290096) * 10 ^ 70 + 4556179862566802947782696313204438763298817270892773718662800093635360) * 10 ^ 70 + 8365735666776473056463174687404809129238868770082772756888695104630233)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_249 :
Polynomial.coeff recurrence4Scalar1Second 249 = (((6744990167506193067298803259 * 10 ^ 70 + 3155754601000156365834539271182149097044615615610560399283000104903174) * 10 ^ 70 + 1785429198595841177036324888991704092871110661115266259459816909746390) * 10 ^ 70 + 5569625861537853600921708250229127005305254951890465138057092994270385) * 10 ^ 70 + 5268073198664864100755325378592024593881678612019782691968051115257902