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_303 :
Polynomial.coeff recurrence4Scalar0Main 303 = -((((111078813538045498134178 * 10 ^ 70 + 8677765512531565530009819875068159235015676544681763256089196775289662) * 10 ^ 70 + 4338921666306508713595575378658249075855633616416291598591654011188156) * 10 ^ 70 + 2580251251442499763965988932996260560356733674127062536776941722816128) * 10 ^ 70 + 6757800609184230672693926789063354156330831887373030581485962032859178)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_304 :
Polynomial.coeff recurrence4Scalar0Main 304 = (((82018817251037684336264 * 10 ^ 70 + 5929091192724838808011714161762788192866569453411299340274555895443272) * 10 ^ 70 + 3309615799768768656034304272154709667620269356631919277242500634638624) * 10 ^ 70 + 2429594745916105107666340999583965905365782354652531965889927987348999) * 10 ^ 70 + 357892822321212983839100652326147217057346563936091972707579202039159
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_305 :
Polynomial.coeff recurrence4Scalar0Main 305 = -((((57336139153211440772763 * 10 ^ 70 + 8435718425024741634750523530074414251071523455472226658994644715489018) * 10 ^ 70 + 3613644646428161043906987354150260769563891175469887472858431393492984) * 10 ^ 70 + 8720455505549727581520761422712992918785220494465710518372245243730118) * 10 ^ 70 + 3335849961275475333182068235474871196769307078972173940401685889665953)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_306 :
Polynomial.coeff recurrence4Scalar0Main 306 = (((38467194888837402115653 * 10 ^ 70 + 1854805801827636201792026526061501275830835156734253307077471140426651) * 10 ^ 70 + 5707549215714273035509327354962942947539236485131543245252027299078125) * 10 ^ 70 + 8735376399001398285826767223986794250913395696671368095885713409611034) * 10 ^ 70 + 4396690583766461512047141150133638531937128491602989242205377085377693
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_307 :
Polynomial.coeff recurrence4Scalar0Main 307 = -((((24968971241726878932254 * 10 ^ 70 + 8595221368633817671159249370242272714128219515904210251456802135471848) * 10 ^ 70 + 1402021513432849688307191405211543468747366807248555798062227462982542) * 10 ^ 70 + 204321585486326368182076809489007228388693269689166746588249601989542) * 10 ^ 70 + 5495179091972492202962485641513732896511797803608747865210369370024299)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_308 :
Polynomial.coeff recurrence4Scalar0Main 308 = (((15762031548795338676648 * 10 ^ 70 + 2114011299105661986665477212616353737706438651638620241351111930119433) * 10 ^ 70 + 5606947575568265548366578948720567996684818819980315713748818975734608) * 10 ^ 70 + 6782787819131230729945758845406352658589219905785944523779636029354804) * 10 ^ 70 + 1656961124785966103717087254677926294410994628794202761801202905552911
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_309 :
Polynomial.coeff recurrence4Scalar0Main 309 = -((((9711214639921587205327 * 10 ^ 70 + 5335541961331792641181739702137288926998840593604500245445654531411461) * 10 ^ 70 + 5638494228674869800132972888120202002926817579424655842353969079596390) * 10 ^ 70 + 982638799817992828301287765404831547020655318658638974601790559101881) * 10 ^ 70 + 3337557894303768122367247228420258980319994191388377379729053438919203)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_310 :
Polynomial.coeff recurrence4Scalar0Main 310 = (((5854805746344612140409 * 10 ^ 70 + 5774093296924176695971097831182964817486758014253478770911533802486393) * 10 ^ 70 + 7620763579773698954343955956246711971967969038311218607408113651265433) * 10 ^ 70 + 4559575475455285635559739566773638298252201894536421238994942943520806) * 10 ^ 70 + 6672770683069232382494218751963998060217053033372138107514802525494625
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_311 :
Polynomial.coeff recurrence4Scalar0Main 311 = -((((3460996738315403120738 * 10 ^ 70 + 4693103761886092323211124011925588516547898820336706140152679868108193) * 10 ^ 70 + 3006775074882126653300974093358192701738410284788985102888684926052163) * 10 ^ 70 + 9575364148765267584828598120967447592034756487093195706755220936260284) * 10 ^ 70 + 6022059200360008514865278197975840373187541492848590667520210462186747)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_312 :
Polynomial.coeff recurrence4Scalar0Main 312 = (((2009382175563633478846 * 10 ^ 70 + 3709280676339966354660265564251865785106012327710971813082092428730364) * 10 ^ 70 + 4940288973215779002167336917525042399320957851946990947224149059041552) * 10 ^ 70 + 1906565637923740092151480020954008540653874338235424704094233071754050) * 10 ^ 70 + 9889413933363900205076843705410344524996530624353861504670427140031677
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_313 :
Polynomial.coeff recurrence4Scalar0Main 313 = -((((1147484285448696535356 * 10 ^ 70 + 3043754522491883125352363677498880380537549386197247888958901910079477) * 10 ^ 70 + 1302406245872566289296720734583965703507691882086149318641436262695635) * 10 ^ 70 + 8820770552590450389763425803912340657453061926784107227293367364674611) * 10 ^ 70 + 1138507653209809828665142807370742991102165105378120916807612708866953)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_314 :
Polynomial.coeff recurrence4Scalar0Main 314 = (((645495581404073329867 * 10 ^ 70 + 2772785141712157800532335205563299066140293060877188191266651641944273) * 10 ^ 70 + 7727798812528648859756912489014858801142995195056328829667825752102128) * 10 ^ 70 + 1912403407579162567480485139731591969487467516170064380571792560602551) * 10 ^ 70 + 4654548332927390816359060304265558157413375726583233001855372648914908
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_315 :
Polynomial.coeff recurrence4Scalar0Main 315 = -((((358249997323423513020 * 10 ^ 70 + 7249459168469871739274956276169164128714648593402196143427506538640457) * 10 ^ 70 + 993431456370274135551381965383142531598416055694015067790546905144320) * 10 ^ 70 + 8796637113475539716624423452282885240971707500107512152570991934263619) * 10 ^ 70 + 7629731612280373664863733451532975861748467344562648513604947753472166)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_316 :
Polynomial.coeff recurrence4Scalar0Main 316 = (((196519634645896512827 * 10 ^ 70 + 8205298588034154363846956514542302824189985348080868535122568168746031) * 10 ^ 70 + 4066025465607033313425748945440225377237953794957067437785386926482707) * 10 ^ 70 + 3769149241926929743092324543470182466638863387704298533687144407510006) * 10 ^ 70 + 5091040101453408860047663429950781565431075428141855599775352937172231
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_317 :
Polynomial.coeff recurrence4Scalar0Main 317 = -((((106776673191604576864 * 10 ^ 70 + 1380753688051804974647516859096209770837954783179446970485880511952300) * 10 ^ 70 + 9348151771218028194183848888353306723953761063577510141745713751625492) * 10 ^ 70 + 4187970073737748772581733871274529534564716517550727680661685320958447) * 10 ^ 70 + 4317874816066275774896164620590571119399411566252638608638669652001284)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_318 :
Polynomial.coeff recurrence4Scalar0Main 318 = (((57610383413981833400 * 10 ^ 70 + 7933327879043746425288298756359608284095485478980337326116642852718732) * 10 ^ 70 + 2255501889850190922919218139445031773595093335468173691423028684432144) * 10 ^ 70 + 220753362843478640931513173140514474636036917857139908467469209334850) * 10 ^ 70 + 5651980621701468176463800058503131644539810114795787779262584347163882
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_319 :
Polynomial.coeff recurrence4Scalar0Main 319 = -((((30958097155528230078 * 10 ^ 70 + 7858375345093829489310279095691871928644198548898365844469607973209105) * 10 ^ 70 + 6914208780869479156201800759889666853667484634809671624620645165604166) * 10 ^ 70 + 5948344713607108179145944576161622187918612707105818356612959420190239) * 10 ^ 70 + 3650586289201891391620885606626650287229868820997750958992212581619314)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_320 :
Polynomial.coeff recurrence4Scalar0Main 320 = (((16624753873284471845 * 10 ^ 70 + 4329029895554772450783938411259680846237828172101341223185651270919539) * 10 ^ 70 + 8641586970130280991177223289098876822278446096522686507250114758904273) * 10 ^ 70 + 743545332888018190669429286344392492131493294039482569998545793156133) * 10 ^ 70 + 5821926979027039615824782088115356964694437677746687171778052734300963
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_321 :
Polynomial.coeff recurrence4Scalar0Main 321 = -((((8953172881090783493 * 10 ^ 70 + 4009486032316554850560417882071775192299752508289244141208348064938647) * 10 ^ 70 + 8807306600769249106976843702309529961489557918062268416789779761272416) * 10 ^ 70 + 1895925108679886962916234832167012728820072951404322423353138098312249) * 10 ^ 70 + 9712956281715955697908296047594671985157877040940530559483501220176941)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_322 :
Polynomial.coeff recurrence4Scalar0Main 322 = (((4851680400047337302 * 10 ^ 70 + 6236101608266855298702604040894710107966339737507887470417043505318495) * 10 ^ 70 + 1786761385267240171155401928401928826750658539003209815914082072089175) * 10 ^ 70 + 5489420439055363395236079381390288459246503074805610506154088698198136) * 10 ^ 70 + 2547007914778883104656668914581131928792700258679154268181258543796495
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_323 :
Polynomial.coeff recurrence4Scalar0Main 323 = -((((2652572313993869432 * 10 ^ 70 + 3876807110247685232639841174988882158099150320374095877065488958319502) * 10 ^ 70 + 4669424573320442749976488658550255195132851834697593235674638237874751) * 10 ^ 70 + 6938578877910529370654940660074409399899772603738771912828278648218436) * 10 ^ 70 + 2053744777083973454133550122453995350075559002492489174303064652343841)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_324 :
Polynomial.coeff recurrence4Scalar0Main 324 = (((1465467680961098030 * 10 ^ 70 + 6771369106946290862594632688514884980056229420321250938691755815631840) * 10 ^ 70 + 889380237756859918232649660361858311185038202076947046637862420857601) * 10 ^ 70 + 4644046644102379606177953907948771066902825110277470334429103783812923) * 10 ^ 70 + 9929650028627591943773013710176617127448741184127940362742388476353423
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_325 :
Polynomial.coeff recurrence4Scalar0Main 325 = -((((818209732884394916 * 10 ^ 70 + 741800085181816027836436233597902010983878775475021692614382805486392) * 10 ^ 70 + 7179938124958185308984864581737681098645306895668596327953756802650177) * 10 ^ 70 + 1530086053821339909228216229459394315574378524518815884799008858151335) * 10 ^ 70 + 5131768846998606225644849653299273819270453139618481291315353347678003)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_326 :
Polynomial.coeff recurrence4Scalar0Main 326 = (((461038087234618026 * 10 ^ 70 + 1313090122305773921245031369669702359385800393985156058661254930080440) * 10 ^ 70 + 7850032133566574182477009770656860937463833710544932664480121925141450) * 10 ^ 70 + 3049988834349893805576425715459608449831404747776410055172424004756747) * 10 ^ 70 + 5942492655436142981969483393456857624561320247580108168609899977000367
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_327 :
Polynomial.coeff recurrence4Scalar0Main 327 = -((((261501275415638026 * 10 ^ 70 + 1019717520759204154250282847704894409204028547018500923133627280577412) * 10 ^ 70 + 6932312302215502516979111200555828814515256874435909781053620107683913) * 10 ^ 70 + 9200486080933578579456093780606601904196194235418435246821005026722690) * 10 ^ 70 + 8872339696920370650890558446997462708276591996180746801144360245201747)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_328 :
Polynomial.coeff recurrence4Scalar0Main 328 = (((148810791872770289 * 10 ^ 70 + 8932516608052616981045198457249838548669877432377242103765220336760227) * 10 ^ 70 + 1947682671908948016001774947947611408719301309359884328714583081490125) * 10 ^ 70 + 5512337935894245183478966821341790878942415597122948285965851518897909) * 10 ^ 70 + 7550599524028479612033841940348523836398075968236620195333415370190637