Recurrence 2 lookup certificate: Scalar1Left 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.recurrence2Scalar1Left_coeff_233 :
Polynomial.coeff recurrence2Scalar1Left 233 = -(((3169 * 10 ^ 70 + 8054496941105839786906928034247987481858394383048287606564522466940782) * 10 ^ 70 + 611566354671837828657257874844247154849792920490441289066687532369061) * 10 ^ 70 + 4748385158473687212732992003280836094217871237384672880587519605026397)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_234 :
Polynomial.coeff recurrence2Scalar1Left 234 = ((3745 * 10 ^ 70 + 1065196659936343443196457775481947319436814105918276118469548568649521) * 10 ^ 70 + 5135482349807200700432046771386096088565671423599034844882952749528774) * 10 ^ 70 + 6054369537749525179713835828127229835346437619055632928569368355975872
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_235 :
Polynomial.coeff recurrence2Scalar1Left 235 = -(((4192 * 10 ^ 70 + 5567610654861739732743231314721861663527278108156180773170151076437858) * 10 ^ 70 + 9619154073798772554790993507533621777378077254767479517999101912557278) * 10 ^ 70 + 5544638719317736058008638602322979621020302916863013008017498442551547)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_236 :
Polynomial.coeff recurrence2Scalar1Left 236 = ((4446 * 10 ^ 70 + 1821947140216617058066709115096758941030323318230179326837148260417803) * 10 ^ 70 + 2986101780464096921237355301988178656834307307517149385949433523118355) * 10 ^ 70 + 1891715237624709290532754578431877686342731449924815361664934887558188
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_237 :
Polynomial.coeff recurrence2Scalar1Left 237 = -(((4457 * 10 ^ 70 + 4291969135953104181283828115163335036633956171839850097922843085336337) * 10 ^ 70 + 4084784846195601228156531530625986322238114788893262997788506767155444) * 10 ^ 70 + 9157399880701290159310933586666250879502840874845648346112833098725301)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_238 :
Polynomial.coeff recurrence2Scalar1Left 238 = ((4205 * 10 ^ 70 + 1045479275367687635037218169389401625750255140431508420648624729201464) * 10 ^ 70 + 1915455212701178237864906267529890849027960974964284512925503868019301) * 10 ^ 70 + 2382546669594668069411753097944293117100754015720414996526703888140345
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_239 :
Polynomial.coeff recurrence2Scalar1Left 239 = -(((3700 * 10 ^ 70 + 9410286694357562064886175219950809659916229004394892388147038420360170) * 10 ^ 70 + 4807029240770487458017154931283061171761871477735980120864822479193532) * 10 ^ 70 + 2809116764906284709471623901763729073141408447671963066544902478067934)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_240 :
Polynomial.coeff recurrence2Scalar1Left 240 = ((2989 * 10 ^ 70 + 2715910794754190609658948265698479092045668226467403850520434602238381) * 10 ^ 70 + 900342321290884422752135676568021116439745874428960748583597840253722) * 10 ^ 70 + 6656666836855436403400415630347385104316958364337565174143291829444469
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_241 :
Polynomial.coeff recurrence2Scalar1Left 241 = -(((2140 * 10 ^ 70 + 6433124832439201908143088329383720673772849821271231936276599030855282) * 10 ^ 70 + 7678842963559616522198747539459708200723800628454165222032711430292826) * 10 ^ 70 + 3303491412148893159566294333016541248972922849151717726898009071037195)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_242 :
Polynomial.coeff recurrence2Scalar1Left 242 = ((1240 * 10 ^ 70 + 6411733802679561454508245800987779997557236801248359265367206582644150) * 10 ^ 70 + 2864272077485930560761085514097965022071366808528913560428240361666685) * 10 ^ 70 + 7253970164187545022682510152686036332223729992481540418947355228673588
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_243 :
Polynomial.coeff recurrence2Scalar1Left 243 = -(((376 * 10 ^ 70 + 3098562362188636281520488783465814638627303016919306190981950272200038) * 10 ^ 70 + 8635505269123552841689384583477579312131542633518023566379123214275120) * 10 ^ 70 + 2681598789064655104053917149760857992739399914051641158117391914284026)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_244 :
Polynomial.coeff recurrence2Scalar1Left 244 = -(((376 * 10 ^ 70 + 9543524425208381496695244564018682707868222254783903036488516954342731) * 10 ^ 70 + 1414365009872438480598168636449882613909068445250939596882215154118246) * 10 ^ 70 + 9590967483782745862671055213356192177716768043587601449661048937250955)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_245 :
Polynomial.coeff recurrence2Scalar1Left 245 = ((965 * 10 ^ 70 + 4339289209719667965775444187062256622673803988994994965136550062031309) * 10 ^ 70 + 6600542985319743170151445495139782880490465793266282799784767435211252) * 10 ^ 70 + 8337842075608420522637446458147865987241590236128714114897234987467941
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_246 :
Polynomial.coeff recurrence2Scalar1Left 246 = -(((1362 * 10 ^ 70 + 3326622971737000021816950588724588271304654864301158061476685140052111) * 10 ^ 70 + 1725584930892046242649834278524904782380405224014681636358400832660069) * 10 ^ 70 + 3408620157376932037594268489634335541835566414972377999706381127708581)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_247 :
Polynomial.coeff recurrence2Scalar1Left 247 = ((1567 * 10 ^ 70 + 7567551416923528946686689512012325481842340321208806583732948494215608) * 10 ^ 70 + 6737919318133621595995695040542264179864510361593842871873109479912015) * 10 ^ 70 + 8757675325098055969961724554397497740224191094674715732233834202299612
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_248 :
Polynomial.coeff recurrence2Scalar1Left 248 = -(((1604 * 10 ^ 70 + 1704957703785468016430237885057187492217075588815543783252645603826229) * 10 ^ 70 + 7625253025673792676150255664888233649022804005050551410541627953888144) * 10 ^ 70 + 4122577733937038202455270209275039996064245002710622198535143412941128)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_249 :
Polynomial.coeff recurrence2Scalar1Left 249 = ((1508 * 10 ^ 70 + 9293826798083757337823844548793779257664897958212207645629615559930729) * 10 ^ 70 + 8208309260262303251169511774273394492452566443995982818710982983877824) * 10 ^ 70 + 7801973757329629852460194481256735856258412811222688379255224177487126
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_250 :
Polynomial.coeff recurrence2Scalar1Left 250 = -(((1325 * 10 ^ 70 + 8422172428782820562906444339549609389162112710388436631462699649952532) * 10 ^ 70 + 4857479887044460967220910174409227694895368145250528006099989456387123) * 10 ^ 70 + 1503252353548519431105814906311483268589099144829350421933955727950834)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_251 :
Polynomial.coeff recurrence2Scalar1Left 251 = ((1097 * 10 ^ 70 + 5418332989953185771135718985557285521544312004672030735484205054723763) * 10 ^ 70 + 4224333969950250764621434010207314735113433478041030205661158828769223) * 10 ^ 70 + 4937445204976546311631440957250878165055117548596653475503186920645870
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_252 :
Polynomial.coeff recurrence2Scalar1Left 252 = -(((859 * 10 ^ 70 + 8943747572156194065263613233649633429031852967780140634504060943819491) * 10 ^ 70 + 8293038931523526376616481135034837681119046468167675283589588042121785) * 10 ^ 70 + 3959094156127032891070474222006509159252558593684120698746995336277974)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_253 :
Polynomial.coeff recurrence2Scalar1Left 253 = ((638 * 10 ^ 70 + 9672931125619179150009322595305538921530825242692339449280507513167699) * 10 ^ 70 + 1069233143304254577575849587730549945779460618222841675019230445729428) * 10 ^ 70 + 4822884832102978941651407047538667695725810087897313314382057553714034
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_254 :
Polynomial.coeff recurrence2Scalar1Left 254 = -(((450 * 10 ^ 70 + 4202416430073843744961413483168826219562843968710868719371455578120716) * 10 ^ 70 + 6353383285980304183430610377932765998064189726775605718199648719180852) * 10 ^ 70 + 2382751374601051303707342938581632276785609416317764063183445511882904)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_255 :
Polynomial.coeff recurrence2Scalar1Left 255 = ((300 * 10 ^ 70 + 7292446156662148414391495205289515236851246044017387529702352618293720) * 10 ^ 70 + 7766738379493234387102748347158511187218641343524905730287710109970421) * 10 ^ 70 + 9663433921646354556039800173772735721728886452796544628118664259760242
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_256 :
Polynomial.coeff recurrence2Scalar1Left 256 = -(((189 * 10 ^ 70 + 4594933966617068994542962809233725550863948065950762165484613839039143) * 10 ^ 70 + 7516692330164977208823277395488826991409784793482738696404018849387118) * 10 ^ 70 + 14666152170208823535831928175810308199189427784088905084542544746775)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_257 :
Polynomial.coeff recurrence2Scalar1Left 257 = ((111 * 10 ^ 70 + 8387427674502548004791989943388584445965049581768959428081314706527097) * 10 ^ 70 + 3647621494391842239686139089520339898539713904243160641376772629496394) * 10 ^ 70 + 2720665811995157112647234620375264101752522959337947701481562051838845
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_258 :
Polynomial.coeff recurrence2Scalar1Left 258 = -(((61 * 10 ^ 70 + 719834480644467086252073477822533456551673926038184340000521611465890) * 10 ^ 70 + 1382311295401795321267677891523088766602131830566769034618495017800829) * 10 ^ 70 + 791431934925821194851957647952590629326701220018518586810431911645056)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_260 :
Polynomial.coeff recurrence2Scalar1Left 260 = -(((12 * 10 ^ 70 + 6092616600547973416352182281572099817128119911988650077150749031444933) * 10 ^ 70 + 7911493360179255818364690851180254163138549536201634704802284857606493) * 10 ^ 70 + 6341335829417278572664041186286901424764950423078431140762669435792684)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_261 :
Polynomial.coeff recurrence2Scalar1Left 261 = ((3 * 10 ^ 70 + 6879495031668399096757960344690221519413750640085440568143864139446050) * 10 ^ 70 + 1419732044904425250851766375002451773168455764250362678214901247360013) * 10 ^ 70 + 6743728345056188993787879120611695235881502161580829436418801653253095
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_262 :
Polynomial.coeff recurrence2Scalar1Left 262 = (2478710433128340043155950681408500356287770169517978222805485407249652 * 10 ^ 70 + 9039647921092957080725661537526313829497725919877147590080898886557737) * 10 ^ 70 + 8632275979435833128160426614004252951301221631381348656539328116366334
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_263 :
Polynomial.coeff recurrence2Scalar1Left 263 = -(((1 * 10 ^ 70 + 5519625997817215318626803069680089883260145893202369189716286761053902) * 10 ^ 70 + 9659945492983908445995209859250419469239424395545149321197856965879069) * 10 ^ 70 + 349450278089356164730077865738894223063191685460252814838635257338640)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_264 :
Polynomial.coeff recurrence2Scalar1Left 264 = ((1 * 10 ^ 70 + 6440155804614089583879435833201156049495338071775734082180433058681645) * 10 ^ 70 + 2951035539616493064873531322434736419836880791966033597290233572193000) * 10 ^ 70 + 1772445641914477628262136016896216150685041111532962834528107509998638
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_265 :
Polynomial.coeff recurrence2Scalar1Left 265 = -(((1 * 10 ^ 70 + 2979157741361611886742071983203247109727004543576632977400467656867026) * 10 ^ 70 + 2752796533683642232439637623861468678332323549247526337839666228554879) * 10 ^ 70 + 4548335305395564505416811820771824831320418501883162016796040303063656)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_266 :
Polynomial.coeff recurrence2Scalar1Left 266 = (8835381455406739903132285925487919161237530117094702174700058855380774 * 10 ^ 70 + 4487843474909870741756311378196936433782866079655051035904945991176249) * 10 ^ 70 + 2787721577498536892177987522883228483028049064664768416428167517214110
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_267 :
Polynomial.coeff recurrence2Scalar1Left 267 = -((5435019470086859697924579686403042153148828339718732635517597070004291 * 10 ^ 70 + 8736637925230442476349270662185484100218906334605295424705438586429639) * 10 ^ 70 + 8097873202385680981226998193459970399978239966583521762261882770849889)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_268 :
Polynomial.coeff recurrence2Scalar1Left 268 = (3082065026992658807629127581151635250121272225628196381677925629106423 * 10 ^ 70 + 2475824227834833126588951665792038687291172349194457370883001763167180) * 10 ^ 70 + 1437030209372052349975452731376895427146510419870293695709358406380770
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_269 :
Polynomial.coeff recurrence2Scalar1Left 269 = -((1625838700867706413624784124382574414109081782782683078915427436020166 * 10 ^ 70 + 6333351108959295370217021708007177569256013443729479091265150848848955) * 10 ^ 70 + 1186043281788949618440988384681044449014965878514117540551570224546451)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_270 :
Polynomial.coeff recurrence2Scalar1Left 270 = (800350822543625409336209441698269432977026031224480136215285499448243 * 10 ^ 70 + 1842300180810549443277903134924432230941705621914696251618950825519305) * 10 ^ 70 + 3199471418300678238685093954390592913395092787051236543274472841040261
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_271 :
Polynomial.coeff recurrence2Scalar1Left 271 = -((367229220016802072578494042652869533920163216783039565621731960668970 * 10 ^ 70 + 2836088853775229836412677895484193930341716645230763130931085134109479) * 10 ^ 70 + 7246899367427257376714700271972415785877862749276072434910705366266314)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_272 :
Polynomial.coeff recurrence2Scalar1Left 272 = (156146855280538911276324665320504448690159201964216598940760290201617 * 10 ^ 70 + 1721280570498632212860920325262798440179590146721091356520739775164053) * 10 ^ 70 + 890374467855508762769821007068546313997541357102990161302461919315426
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_273 :
Polynomial.coeff recurrence2Scalar1Left 273 = -((60749384200820798609431327315998323042943877885565354139137794395429 * 10 ^ 70 + 1064538580702300018242052460779100341706559687152508346005361012641872) * 10 ^ 70 + 9967351630064969253807306942541127930904145559610453347029176134190753)