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_188 :
Polynomial.coeff recurrence4Scalar2Exceptional 188 = (((15279557844530 * 10 ^ 70 + 5044192487572112627596050386317142997927007157144007885890593864337295) * 10 ^ 70 + 8707504032977312445154521043202230709785236006192404537665637994095718) * 10 ^ 70 + 6991195953799082510208612770280537618026474134036472986521091183783263) * 10 ^ 70 + 194603865050233784811374788896357128110196990514316415901087538358477
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_189 :
Polynomial.coeff recurrence4Scalar2Exceptional 189 = -((((38870409524087 * 10 ^ 70 + 8455183790389169594979872460490163063922060945963412110331363565687824) * 10 ^ 70 + 2209465380028367637650419655234448857717199620274571411644861359958115) * 10 ^ 70 + 3588739659375163486140926114918808026851132721500370642239531863237342) * 10 ^ 70 + 7622840416702111207569585459105543358875100726291115496016918782858044)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_190 :
Polynomial.coeff recurrence4Scalar2Exceptional 190 = (((97367505959319 * 10 ^ 70 + 249465205506121076352616072212471456418175399889294362009107206606518) * 10 ^ 70 + 7680603597066133876390814524294270977199305360966350818158688075475719) * 10 ^ 70 + 2719846428260629584176544680899628205294953014561346580915584128696233) * 10 ^ 70 + 3715235289794418365479235814092427292725115712768235736798374874136080
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_191 :
Polynomial.coeff recurrence4Scalar2Exceptional 191 = -((((240179515518498 * 10 ^ 70 + 3969789999719686552979377679996478512750434265712247546317060187637521) * 10 ^ 70 + 4903266281835743082491959900632981952770324420550729662167035528564129) * 10 ^ 70 + 7943652126698267158364065156460928349789178577193107484948478139394132) * 10 ^ 70 + 741358880475518085455732426032961260003888476289715301714088321732705)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_192 :
Polynomial.coeff recurrence4Scalar2Exceptional 192 = (((583476876888254 * 10 ^ 70 + 7970701436785931047551892914930226406218830756686284716191752431128537) * 10 ^ 70 + 3791328310566564243675024549301203042758343917370879820332359015220482) * 10 ^ 70 + 1685932135875065544917917438593348666458806397715783793636053351719241) * 10 ^ 70 + 9826878955733114622249807080439970415757222858400800851491233805985809
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_193 :
Polynomial.coeff recurrence4Scalar2Exceptional 193 = -((((1396093049858785 * 10 ^ 70 + 7332807988907594767669903790759181169540049585717160794925105478898617) * 10 ^ 70 + 752259591688028773410480020242739933235374556289764964309413769167698) * 10 ^ 70 + 4861057152029494255132542208109948127141594334518652006440596021917694) * 10 ^ 70 + 8387625784695214685106520779984762170468811474508292791733319185836514)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_194 :
Polynomial.coeff recurrence4Scalar2Exceptional 194 = (((3290364023434998 * 10 ^ 70 + 3256109077922920813215970932778236782333212742812168597032036923779692) * 10 ^ 70 + 6206383619064233736522913737031824138529873888888212061962528472367961) * 10 ^ 70 + 5215028541241928829133221787833825706687473510111054850830413261373312) * 10 ^ 70 + 1452016255276349778148179484277038777176179224284059109936724348596657
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_195 :
Polynomial.coeff recurrence4Scalar2Exceptional 195 = -((((7639182577332071 * 10 ^ 70 + 3413875847034584458023177828523129122782957443279311344249511750388514) * 10 ^ 70 + 28860901155959808300645804336699361641837649176135768897792130909654) * 10 ^ 70 + 2961785657182667940963324970732340919003208479176247607480989758327513) * 10 ^ 70 + 5408372454370080478881026312200933972121729691777948091614000940856298)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_196 :
Polynomial.coeff recurrence4Scalar2Exceptional 196 = (((17472554702459541 * 10 ^ 70 + 8078117465411929308200751705967492761283809277568798597411186422962758) * 10 ^ 70 + 6610184124445000069053805703316964769458336272364596640481234787737031) * 10 ^ 70 + 2147505282554193231410104613874141953449576239576361336224431658081614) * 10 ^ 70 + 4905973916299277504472489390521014992052316069384213312608188201854775
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_197 :
Polynomial.coeff recurrence4Scalar2Exceptional 197 = -((((39373544845347455 * 10 ^ 70 + 4872398786317164053027303900326725477917969236436141143449823029530933) * 10 ^ 70 + 554413673055444633386337638928506003732136247209150193734411052648547) * 10 ^ 70 + 2983727799967746234141358013084787440642101928300592997145004440626705) * 10 ^ 70 + 2008297637070095438362373955854598408516012024248141298067824591600083)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_198 :
Polynomial.coeff recurrence4Scalar2Exceptional 198 = (((87422269998165601 * 10 ^ 70 + 2405764538159235256496074127343692401514863809756098750180145504949775) * 10 ^ 70 + 8650920769212527194018868772205186805516539477958918819342529061024638) * 10 ^ 70 + 2613716271919863071589440187637381497384908994081011601800024682715205) * 10 ^ 70 + 7044078928627138441596091926922398268162567663992607094883046789422471
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_199 :
Polynomial.coeff recurrence4Scalar2Exceptional 199 = -((((191266483309773926 * 10 ^ 70 + 1427732510773316758343760440455254964435181170153211364263797721833104) * 10 ^ 70 + 425359495736237296862924697346396699754114713563553806499221810525506) * 10 ^ 70 + 1081350374949204312559042176444399613066664150052034630876012113644872) * 10 ^ 70 + 815512159074663866447073847850837584397764382461703696006916446112602)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_200 :
Polynomial.coeff recurrence4Scalar2Exceptional 200 = (((412366745973954835 * 10 ^ 70 + 1544608253364138767913303299017903987479190409500509677893372993242570) * 10 ^ 70 + 7233560361116756028686490434830863392259749649713287684116495093932245) * 10 ^ 70 + 4122394680941444706769297077727660600841895011135476530420389845362808) * 10 ^ 70 + 4823792307669667347506750335223791007325019272042365044632755394695330
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_201 :
Polynomial.coeff recurrence4Scalar2Exceptional 201 = -((((876161397180500515 * 10 ^ 70 + 1810233956261205012357627592764166598011514904328177620293660524915369) * 10 ^ 70 + 4879384893903073293189899194736311250905021969912319002520230463968305) * 10 ^ 70 + 8631540784087950091377899227465453450952067661159757250492096112356318) * 10 ^ 70 + 7019822881275407569778893083223908157120155374773041549069493578955380)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_202 :
Polynomial.coeff recurrence4Scalar2Exceptional 202 = (((1834708653533126435 * 10 ^ 70 + 3575537003466636320292372373828604504298381375739874602135800508557863) * 10 ^ 70 + 7515268063084367983492293427667597206834490475461963453473544541396029) * 10 ^ 70 + 3652035955952073408872926054839947648638427139047279063734586945967316) * 10 ^ 70 + 2335524076340990487328738671268364635452731499004762909824545373579288
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_203 :
Polynomial.coeff recurrence4Scalar2Exceptional 203 = -((((3786679183794101214 * 10 ^ 70 + 8192322025859569949509325550299426221743288301170026119085416064075943) * 10 ^ 70 + 4530156750185089886155030287221967994745426433216012430867480111479237) * 10 ^ 70 + 1477022096657105809830591472294569978544858648133417977414880199092055) * 10 ^ 70 + 4866834949308396038084704725447878410548815202421528728006931188040560)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_204 :
Polynomial.coeff recurrence4Scalar2Exceptional 204 = (((7703415908918024110 * 10 ^ 70 + 1225704521569333988770176819201890567968789055163763868174113228089904) * 10 ^ 70 + 3765491296385834070810514589666242991960323217082680722634063732620308) * 10 ^ 70 + 8724609045098352284628088850102173199757960919545556648569534730130257) * 10 ^ 70 + 5745841382038143029404484892493667468591635107799110690292455223125074
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_205 :
Polynomial.coeff recurrence4Scalar2Exceptional 205 = -((((15447770140544397461 * 10 ^ 70 + 8294891817739709012001617774947726565038306842240141920114626542189529) * 10 ^ 70 + 3291089476728481293538440837357347470958262733715753651680479717385480) * 10 ^ 70 + 9816360671370724632381296833137180724486737698850923814494485743166007) * 10 ^ 70 + 340169681942791240008402815921071906501739851388083818272927321412500)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_206 :
Polynomial.coeff recurrence4Scalar2Exceptional 206 = (((30537202866102705091 * 10 ^ 70 + 2124977233446543930618657831946419131086473650957277976876238451864875) * 10 ^ 70 + 6294392288335898031777812805487121368212280156253535965800502048093029) * 10 ^ 70 + 7556206747926898266863923225610259945334204712662303741376850868164864) * 10 ^ 70 + 9236444008921046365196901863741585128133608434701842866108867354368801
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_207 :
Polynomial.coeff recurrence4Scalar2Exceptional 207 = -((((59510873421759282582 * 10 ^ 70 + 3361005410898690668518245174836508901890379816942966992997260416184194) * 10 ^ 70 + 2829759166891700280699417172182247878410137241928860596487266486960278) * 10 ^ 70 + 9837775667396935712062170411605440057188144219401583738808341284293591) * 10 ^ 70 + 8992960241255681467979488735736529987685872683623622148284433073038910)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_208 :
Polynomial.coeff recurrence4Scalar2Exceptional 208 = (((114337548114450120729 * 10 ^ 70 + 8044726106054821185211961936456339298121523812800419943344260850453423) * 10 ^ 70 + 6000703635104881984011995666045480413916913243258455684397205953645186) * 10 ^ 70 + 666451454236002678761867581971382845777540854045713583627711862622575) * 10 ^ 70 + 8269627782698383540969923544294100530293643533446861563735896725222256
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_209 :
Polynomial.coeff recurrence4Scalar2Exceptional 209 = -((((216584838848950867003 * 10 ^ 70 + 7654849651449460310551444607166173206040648764267288189303843853188074) * 10 ^ 70 + 5240584173484915485364481081449458273143826544779270408811779165024429) * 10 ^ 70 + 7989608635672937822322142548530375479275458832777224968492190742771626) * 10 ^ 70 + 9987496779277418886064428184776068377876616848876946476841443139267945)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_210 :
Polynomial.coeff recurrence4Scalar2Exceptional 210 = (((404514699503874873523 * 10 ^ 70 + 7065414389852701494214319254650536166862477675449252081353748993231392) * 10 ^ 70 + 4014157536276918171616809525761850868102780524873471337013429040408676) * 10 ^ 70 + 3167360336888015819822213185127838304695715568050947176585493411613782) * 10 ^ 70 + 2625053689552383755960499056819389332179549540117724743293363418124316
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_211 :
Polynomial.coeff recurrence4Scalar2Exceptional 211 = -((((744950507053642060924 * 10 ^ 70 + 5039211596043914128745892129317678409136791136970874534972157470853798) * 10 ^ 70 + 5609183534892182734558620998968540972916498404039252500445700016138348) * 10 ^ 70 + 491430438892143658619036255804268695988779868175560844785437810518885) * 10 ^ 70 + 2661695542984562381572249702722509350883869468115891267426726494626649)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_212 :
Polynomial.coeff recurrence4Scalar2Exceptional 212 = (((1352777950412606821288 * 10 ^ 70 + 1205266348296405519827166576122724596032589583055892213333267050701255) * 10 ^ 70 + 2894920495484141941013357570380017390604771777828034965986450302428960) * 10 ^ 70 + 4863675016301288568264946094628555454059800266280101364142260529428216) * 10 ^ 70 + 5759495996651051301205945287748483949684140271465132134341606342890997
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_213 :
Polynomial.coeff recurrence4Scalar2Exceptional 213 = -((((2422423608753774171721 * 10 ^ 70 + 6614650193462622237078165755193164513948228166008212867131332903061881) * 10 ^ 70 + 1638572850140344173603287533028190221638913421585778125515721563838375) * 10 ^ 70 + 8663037354282525394543780229168245534629758827395498814594240529197888) * 10 ^ 70 + 516941971423458324074926533493878713158353644749644298614840127721211)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_214 :
Polynomial.coeff recurrence4Scalar2Exceptional 214 = (((4277756164851042049642 * 10 ^ 70 + 3851241068580839670592695377231653465602854230348960625021063124659646) * 10 ^ 70 + 4630955055903146718014490324713153015848988386506081072628360433087866) * 10 ^ 70 + 3290806636473542321077314363319287152056018226658363332036193647517465) * 10 ^ 70 + 4508005046892994095980318968449252560443956431608773383427056995946386
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_215 :
Polynomial.coeff recurrence4Scalar2Exceptional 215 = -((((7449748447460810465905 * 10 ^ 70 + 7068056159253777287554822505354285391116964430416156160500659059327409) * 10 ^ 70 + 9606593252815055258142252583181480898435485216344350697479592879471804) * 10 ^ 70 + 8281536379564837209696284111009473907107882386719801184768851163976626) * 10 ^ 70 + 9555790796690308624342476658376314089524744372488729217385708779613908)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_216 :
Polynomial.coeff recurrence4Scalar2Exceptional 216 = (((12795095885959051515724 * 10 ^ 70 + 7543868106698633904217777535291279191228472575851132604118824023622862) * 10 ^ 70 + 3685087374751892929736336870267036117998666464608606547780197231608501) * 10 ^ 70 + 5927176785022731261175802320391235401678117128978831138526486213983113) * 10 ^ 70 + 8383113247839131712557101986843561632186350149202499187519915950945824
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_217 :
Polynomial.coeff recurrence4Scalar2Exceptional 217 = -((((21673945552510217475598 * 10 ^ 70 + 4664508167040169037358978970699141039038891568834439771502121581656883) * 10 ^ 70 + 2971709228223263152799321142559968228958725343589033503359333576236548) * 10 ^ 70 + 4773639145306230637400486490808201084196422446996247876432907756073946) * 10 ^ 70 + 7063762520382075581067463143991190985310617402725031314868297991784577)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_218 :
Polynomial.coeff recurrence4Scalar2Exceptional 218 = (((36210998560762794532764 * 10 ^ 70 + 3918250143612486724144382951717112709805246002057124505374728760166352) * 10 ^ 70 + 6324252519737862816318328666382452443484637844379197608066442773638793) * 10 ^ 70 + 2403534530790537008724902329902545313002550973414176270080366243566763) * 10 ^ 70 + 8558371253035398553004368250192329126165320689943362936553281586187467
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_219 :
Polynomial.coeff recurrence4Scalar2Exceptional 219 = -((((59671392308471724340286 * 10 ^ 70 + 2234883150005085166444582348137203716464303732367091062774675969683184) * 10 ^ 70 + 7058920177629572457366378167598181832057953072331177606133958454530546) * 10 ^ 70 + 4274125789240941540641738368286554231982770074099513093615050734934122) * 10 ^ 70 + 9533648602111968962455140566132667324739090793140531448081030393183529)