Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar2LeftPart1.Coefficients305To339

Recurrence 2 lookup certificate: Scalar2Left coefficient convolution #

This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_305 :
Polynomial.coeff recurrence2Scalar2Left 305 = (16087760239018333980158038873770159108594768155804 * 10 ^ 70 + 9285668820898670781046553417858002511148646737708885276902357660646957) * 10 ^ 70 + 6083831233171466480861176183635879532562668677431012082331210316804492
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_306 :
Polynomial.coeff recurrence2Scalar2Left 306 = -((4455661371919909605796074153788517877176365365925 * 10 ^ 70 + 7644138935118422674685983669067318246608996933359537880267447161480401) * 10 ^ 70 + 3865862996370770641390316601142924208089462562409412862267762496930317)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_307 :
Polynomial.coeff recurrence2Scalar2Left 307 = (925535389616452272776775299712309472289989423719 * 10 ^ 70 + 1497715069162997130650319533024990865702709386527659001302212842808738) * 10 ^ 70 + 422748839115422325466549624180178676607360082083887899358915012723981
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_308 :
Polynomial.coeff recurrence2Scalar2Left 308 = -((156973418103484164225606627882256943570605412516 * 10 ^ 70 + 8162593684631618182243505333568609043967397906676565052508292566083520) * 10 ^ 70 + 1809523284743168816026774867127772670422352982788344003066132138836820)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_309 :
Polynomial.coeff recurrence2Scalar2Left 309 = (21811217881162017561966725339793110067348971017 * 10 ^ 70 + 2651847808719873428368147078430063237410601336489739231479557435567620) * 10 ^ 70 + 2067005665244471732919938031897572888397583952807072166049938591901931
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_310 :
Polynomial.coeff recurrence2Scalar2Left 310 = -((2325797623310376436658693188716378044320549337 * 10 ^ 70 + 6266381261308068928762557368676566368363724865568039881510784485584591) * 10 ^ 70 + 2759306002874843704723962519391222415811513542352998399736870436641398)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_311 :
Polynomial.coeff recurrence2Scalar2Left 311 = (136647739161200651045149797600821545520484391 * 10 ^ 70 + 9008566514898823315165599486169512804643967266737958733785907858343787) * 10 ^ 70 + 1281654591058562025185170321742957307497446071327677512390037349766029
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_312 :
Polynomial.coeff recurrence2Scalar2Left 312 = (13045677949910913888442157806857871137025892 * 10 ^ 70 + 9733161959203757341048034716911887235742171075395293842715049615175930) * 10 ^ 70 + 1051940697902288397481470217373433620794602995099675374783167961471624
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_313 :
Polynomial.coeff recurrence2Scalar2Left 313 = -((5814437575274389327540463484239757488567911 * 10 ^ 70 + 7442557862111217464706296115809139728579512755374391579226526443632575) * 10 ^ 70 + 8544347759052424513798040655389308192706087938113986299977420688753067)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_314 :
Polynomial.coeff recurrence2Scalar2Left 314 = (1129999732036585145876513791414335881948323 * 10 ^ 70 + 156564390090394022054025688228816075307259111599022487395572138358833) * 10 ^ 70 + 8595560070002087466510072335712035705565856643575567514940359223245686
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_315 :
Polynomial.coeff recurrence2Scalar2Left 315 = -((157010021059828247529828695111925925132334 * 10 ^ 70 + 8644480273339799108004478359974924795715552693149156471433061410118566) * 10 ^ 70 + 2254351780400617558569348110502447381420679006876841715615829641843801)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_316 :
Polynomial.coeff recurrence2Scalar2Left 316 = (16258239816720147104185807193255100818037 * 10 ^ 70 + 7701579331547910980041586147213971563108440693419785149731633449994394) * 10 ^ 70 + 121524512088547336531003570263763612915908428114696083466656635418055
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_317 :
Polynomial.coeff recurrence2Scalar2Left 317 = -((1081868566915044865799843778097416190510 * 10 ^ 70 + 1152764400497240809206938554880806812554342393050401852943760536758389) * 10 ^ 70 + 7322824978249653531836432114911797156551239536703511678938965276698823)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_318 :
Polynomial.coeff recurrence2Scalar2Left 318 = -((5603484325637920244322785348839540256 * 10 ^ 70 + 6683117480096064880296611848914860956495351588458662804478748043068027) * 10 ^ 70 + 3331524513144730424819611712693244146258442355973018931366225386608007)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_319 :
Polynomial.coeff recurrence2Scalar2Left 319 = (14755256879065474541762386221694370962 * 10 ^ 70 + 3040161338711425506055266232470729541504987559123069791088228528540051) * 10 ^ 70 + 3568191520944972327796569929978833145296372025459908529188668028276019
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_320 :
Polynomial.coeff recurrence2Scalar2Left 320 = -((2642262154490809006080408451161888674 * 10 ^ 70 + 5081537125121599272328336667206662423056188076408183057711555060459706) * 10 ^ 70 + 2485595807789231126679092706325785556654953347899339410617592865888644)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_321 :
Polynomial.coeff recurrence2Scalar2Left 321 = (305323176573217965721892859798717706 * 10 ^ 70 + 2461211442284665142770406952985644688322230710417189817096866602903292) * 10 ^ 70 + 9045250827640743102666592531830106933787529764727824175006996352145729
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_322 :
Polynomial.coeff recurrence2Scalar2Left 322 = -((25237946784593106777591955669402878 * 10 ^ 70 + 57354899652506520182714938271781740706992835865967607194869640781170) * 10 ^ 70 + 7866488650408365021553567996440114034994585626973016828948642943145445)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_323 :
Polynomial.coeff recurrence2Scalar2Left 323 = (1313236656696046941237318570940759 * 10 ^ 70 + 6619078139681762685658364478968612999497767231884211625432575582297104) * 10 ^ 70 + 8183516408045919496428804870217013024480206015795850521669408579623208
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_324 :
Polynomial.coeff recurrence2Scalar2Left 324 = (1738826523886601189278588782436 * 10 ^ 70 + 9532818985632791867786125923373467053947719605131486030257776279003927) * 10 ^ 70 + 2870241125665255379255930807917652068904809130067039712036189841510176
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_325 :
Polynomial.coeff recurrence2Scalar2Left 325 = -((9300957588039264729979674816363 * 10 ^ 70 + 2162876027120660413584319856627098392958685898110994066666661255764355) * 10 ^ 70 + 8736257792635631317643950538810295526950402422400581816509889218030199)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_326 :
Polynomial.coeff recurrence2Scalar2Left 326 = (1193290370068103534739148347938 * 10 ^ 70 + 1131939959983353183678650612195515430577133218372886841983561353092738) * 10 ^ 70 + 6632437181894312028351937885371783119008308873345445831003991723482544
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_327 :
Polynomial.coeff recurrence2Scalar2Left 327 = -((93810370870357213944997353633 * 10 ^ 70 + 1111743789980645134973505117966586828140184775980578937053337283246243) * 10 ^ 70 + 2626435596224305719768829704223768972340512444386153982142051180625485)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_328 :
Polynomial.coeff recurrence2Scalar2Left 328 = (4870641262149088919892898330 * 10 ^ 70 + 6772443745028041794199369913239767886301737433652954198082942467768206) * 10 ^ 70 + 1331617615037230243202280109172211060770943129929183985273997558095672
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_329 :
Polynomial.coeff recurrence2Scalar2Left 329 = -((118875454539409641969551200 * 10 ^ 70 + 2801778841938210328093043431631510739208267729271846524210099652470886) * 10 ^ 70 + 6313585505650102486770298734992352003015391185789280650138804635635468)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_330 :
Polynomial.coeff recurrence2Scalar2Left 330 = -((5932370885721113589441815 * 10 ^ 70 + 4100336578492916718169096965043495277920919647040839901487308836164001) * 10 ^ 70 + 6491778523103845052698624624695953147156066950253356904746195641944724)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_331 :
Polynomial.coeff recurrence2Scalar2Left 331 = (874200760887358420012534 * 10 ^ 70 + 8945910192785023892722523824305791865278998468373005015924559113886768) * 10 ^ 70 + 379097909610616397108877860702589852608720354572912041637941716936628
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_332 :
Polynomial.coeff recurrence2Scalar2Left 332 = -((53599993530036248586564 * 10 ^ 70 + 1212165177743555782784784275730344681052218878455340997086454075295105) * 10 ^ 70 + 6498737090398982518374923145619459786029267716929513085744391330518443)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_333 :
Polynomial.coeff recurrence2Scalar2Left 333 = (1915264089749199042728 * 10 ^ 70 + 7505120066604953498074527400089452226800815305572478226918955818208106) * 10 ^ 70 + 7146500556477696511971300810587031288607377254712300807964466273314911
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_334 :
Polynomial.coeff recurrence2Scalar2Left 334 = -((24864115081069586556 * 10 ^ 70 + 5391911895619003621656791139359026561229292108370605585206750654593404) * 10 ^ 70 + 6112675917276425008397059902742625443360029884353831888647749965972330)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_335 :
Polynomial.coeff recurrence2Scalar2Left 335 = -((1475220983599919924 * 10 ^ 70 + 2679072695426718174592400574546156617127016552537586424926566372659304) * 10 ^ 70 + 16362391214163116723773425233037834481185047065496346703726215738701)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_336 :
Polynomial.coeff recurrence2Scalar2Left 336 = (105264925801848874 * 10 ^ 70 + 9943561275080523127471693936597586652400261290338006148813984747706271) * 10 ^ 70 + 5937304888973648237197458415022668584881833886131483010719278635699181
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_337 :
Polynomial.coeff recurrence2Scalar2Left 337 = -((3172886036126776 * 10 ^ 70 + 6349759271776894359650339091547233509708858736005370181444977789422946) * 10 ^ 70 + 4833149945321765289596473456865036437339758252585612726680561271332018)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_338 :
Polynomial.coeff recurrence2Scalar2Left 338 = (36970308084168 * 10 ^ 70 + 1749555896864692057855549012113368134677854752359501778903845049043554) * 10 ^ 70 + 9442541112782191850181475721211843281645342523645535956635718102659197
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_339 :
Polynomial.coeff recurrence2Scalar2Left 339 = (803893015850 * 10 ^ 70 + 8922187662053065059428633535503589508345448177535954528013423867070326) * 10 ^ 70 + 9091102832308982211037647145413139695308800960008160364821125931221373