Recurrence 5 lookup certificate: Scalar0Left coefficient convolution #
This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_331 :
Polynomial.coeff recurrence5Scalar0Left 331 = (((1950083349234973605235406178935135163725830049740434758 * 10 ^ 70 + 4529475961993783113032950772823184975242334524468936439173799233387633) * 10 ^ 70 + 1384327263038667435680819438809829464429064307311110100932829344569393) * 10 ^ 70 + 4578140733798539447717912063586745374060732761164442059143687780232444) * 10 ^ 70 + 7799167481855943572210442731872737300900726073791649412465669208651171
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_332 :
Polynomial.coeff recurrence5Scalar0Left 332 = -((((916914037481422170235090235861683659323034383349959509 * 10 ^ 70 + 9397186417506572625840915637490121114333234754339879906193331746529218) * 10 ^ 70 + 2069731016416616833453269831325691075648773472676686482519679515141982) * 10 ^ 70 + 7099632518191674720548377598829331165208624663127116995881695263318392) * 10 ^ 70 + 1979835801152609856500859916076760906171015268387553269597170888105216)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_333 :
Polynomial.coeff recurrence5Scalar0Left 333 = (((424958548136031180749402751661568260059158677989925738 * 10 ^ 70 + 683693225139648274375213121256517545669379881711457940182343950643517) * 10 ^ 70 + 9230651061021016326065520453326720485524008743969361409025052762231690) * 10 ^ 70 + 4506550192910770380860324799953536124641246028922116403606100933166166) * 10 ^ 70 + 5719873247705944289704915346044506752127876686512653262816817364884882
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_334 :
Polynomial.coeff recurrence5Scalar0Left 334 = -((((193436491809578144428751943630534060921806616484245911 * 10 ^ 70 + 7104072397538608038499888555265128377264333076110590016139468525614492) * 10 ^ 70 + 9837038044682317656453938186374911354781562090777579513396050420554652) * 10 ^ 70 + 9523862055255476646987067980721005073164477273389030808998261446262291) * 10 ^ 70 + 9000249623734147565282237679801494047108388080785367024813810702421581)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_335 :
Polynomial.coeff recurrence5Scalar0Left 335 = (((86284149112451693187851671993243165138322797770314301 * 10 ^ 70 + 4242298712291618592569553398566946069825419111920830911740234448523956) * 10 ^ 70 + 6546768377352257160621846140541022835619859781602241269475674926857920) * 10 ^ 70 + 2098343688030320978547831932798342365486599095754653036659123051336674) * 10 ^ 70 + 8396222653702279387143424078227168344686687878086766473573649276373112
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_336 :
Polynomial.coeff recurrence5Scalar0Left 336 = -((((37666644419826888921557858151316755980047080130224023 * 10 ^ 70 + 1967193646388141531157021922545834365685403081262171846137785497804237) * 10 ^ 70 + 7819932709066084214583136759790484023679200174605685536941374929031270) * 10 ^ 70 + 3946198793867021392377229200134515544676732561819146603345138414523194) * 10 ^ 70 + 8841351816557892076165257518004328826986091641051324782250425943805985)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_337 :
Polynomial.coeff recurrence5Scalar0Left 337 = (((16080784886895706933952695845435546593529134683594136 * 10 ^ 70 + 2056442287900716861531572490960021419855282211877730014739352219647219) * 10 ^ 70 + 1022702523004434097053403514270586437151067444017177009715095414585707) * 10 ^ 70 + 7888648155156223312435791500852906843243967126354953341537813120657628) * 10 ^ 70 + 4769793225132958710867009040398689586848409990490845577487572893935378
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_338 :
Polynomial.coeff recurrence5Scalar0Left 338 = -((((6711609028359905113959351836372222786082164532371756 * 10 ^ 70 + 7855100678506628725395666829438049534436791370724572539804057918683425) * 10 ^ 70 + 9615943807341192785107634520900717462430772568950188507240652700889505) * 10 ^ 70 + 6724103497553292579457186765723651250419529412503212337950499460565249) * 10 ^ 70 + 3725975391935935752600604557560220202005390075552345817541979305923960)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_339 :
Polynomial.coeff recurrence5Scalar0Left 339 = (((2738048859253106189787070831689736525648085398516192 * 10 ^ 70 + 7917535458788734302730985015325853848643869739487031078878534890458323) * 10 ^ 70 + 295064626344512052720572563979483425796035926399562558249148807489036) * 10 ^ 70 + 967015371970058874186034952029838842590855214252107949238020848284542) * 10 ^ 70 + 4402003215609962482656393839841498594551707636754785063470537683649028
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_340 :
Polynomial.coeff recurrence5Scalar0Left 340 = -((((1091714116899343337922542061468702018456906339166359 * 10 ^ 70 + 8417918966440797463739370263355479901189656028754398554925996886349803) * 10 ^ 70 + 2988234803333149036863604432665166758071604390631954757816665011730699) * 10 ^ 70 + 7296247684201606241399847362263288578793378332310752020933759620424108) * 10 ^ 70 + 4358712214397997006621425250715825701716832202013954252069019213353966)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_341 :
Polynomial.coeff recurrence5Scalar0Left 341 = (((425388435897654470777195228682946191040598513172545 * 10 ^ 70 + 9178665163715469904772142083636993156268262198998456388024060727774309) * 10 ^ 70 + 1984343052924658097841020814315795747325761244455453212901920761499185) * 10 ^ 70 + 1677450555210569980689697105234340432764974304501912950837827374762178) * 10 ^ 70 + 8597998117723361557089880694506250535873126912558475215086713917337136
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_342 :
Polynomial.coeff recurrence5Scalar0Left 342 = -((((161957168141125779423597157919452534100611533928081 * 10 ^ 70 + 2959217890660905925471949871060176790747293129939293604305188052772009) * 10 ^ 70 + 198720125939553337358109265375150016418198530901941906667982576003243) * 10 ^ 70 + 6568830017135470735083858243763312554724264570214774599058775564990177) * 10 ^ 70 + 7407788651797552755651690396653240394951039665163123835460452586408445)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_343 :
Polynomial.coeff recurrence5Scalar0Left 343 = (((60232951965623436850002172050525418814435943108994 * 10 ^ 70 + 372604453980484999970908312955765050113743018520782372466327609087951) * 10 ^ 70 + 3102935736018626298876138381508319497249648492934787216221759102434697) * 10 ^ 70 + 5517223614298052665093666365248370748999439552390309922351886289720854) * 10 ^ 70 + 5704347780381980829550404696129967975843481886166208555843304936464306
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_344 :
Polynomial.coeff recurrence5Scalar0Left 344 = -((((21872773653825969353990552842041869818102505878691 * 10 ^ 70 + 3540894706725533093851870786116623711967007957105065541778036473946281) * 10 ^ 70 + 7581530554624905229415724493813093843626361108912827519315367970768353) * 10 ^ 70 + 7163327215056190151990947780088106324905498391552176424656486898975285) * 10 ^ 70 + 9334025512371420618380687607046594708833539939198386170438212582146006)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_345 :
Polynomial.coeff recurrence5Scalar0Left 345 = (((7750669259986380030399133670226590817240360808811 * 10 ^ 70 + 7836387444253291913347767569994983480435571012068171463184826877874816) * 10 ^ 70 + 985652629565057473762516932044390215986589942219455214511575975617756) * 10 ^ 70 + 7315810156405011146285227991724736537179609023061566899279830416772719) * 10 ^ 70 + 5046595779295865215751759022075544120510486422808311025493211910365864
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_346 :
Polynomial.coeff recurrence5Scalar0Left 346 = -((((2677661336138677747910914193684987059123916670593 * 10 ^ 70 + 5400312074654906558987448481296176537160717834005236743205562517587750) * 10 ^ 70 + 5596580572310220930127114814764330144184933551928551264059094444330426) * 10 ^ 70 + 9990840983427022520378010553954605138971805111370690105364752273201465) * 10 ^ 70 + 205507215371095054204414470528914838295518095333493478145473428742782)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_347 :
Polynomial.coeff recurrence5Scalar0Left 347 = (((900765368112635491366457107184521028219155303891 * 10 ^ 70 + 2543913862326727516821287191766921354429989118997626835433660112144772) * 10 ^ 70 + 1367055125464674699188856818417712837731904247518950312406153721416080) * 10 ^ 70 + 3564026460395408431431799477755204821993174198998714391788104437025940) * 10 ^ 70 + 5931020976962079524025707542188352178809008630189034905185942438298148
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_348 :
Polynomial.coeff recurrence5Scalar0Left 348 = -((((294536793670391276724313303490745395003012916531 * 10 ^ 70 + 9141797216115657796352819870702794638193940257458109938848709436298211) * 10 ^ 70 + 4745550967921920350299995228354179576582990594393867902457330957818184) * 10 ^ 70 + 9705302075829753466970062844124396150526690660034004290384570547032715) * 10 ^ 70 + 6523044166347992966515555172024820145412921145238570907003742861035409)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_349 :
Polynomial.coeff recurrence5Scalar0Left 349 = (((93374105433637686768136637805834887273365547826 * 10 ^ 70 + 9087224172351656344663100083132225234121674461830609935706841651675705) * 10 ^ 70 + 3684688432273389471325437347238841263039227693504867356004590815778738) * 10 ^ 70 + 3135385979826887906272415454029226063336510659541694945425688199873150) * 10 ^ 70 + 7950541156648675983720940958155781762425381459363743992326445574761158
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_350 :
Polynomial.coeff recurrence5Scalar0Left 350 = -((((28589062639742545506205525889545404851430383012 * 10 ^ 70 + 9262534225354482539618279405643349981598305026377651455542340565982680) * 10 ^ 70 + 1626317352691810424579933199718959470467111548076526433814142563528690) * 10 ^ 70 + 7695610208058970950586698684917690220314055679326567099742688689088198) * 10 ^ 70 + 6927177152075575783722993103872885164892884427512286928036583085071934)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_351 :
Polynomial.coeff recurrence5Scalar0Left 351 = (((8402615965256606666553700842238360044312829138 * 10 ^ 70 + 4532503827041421817097395950190298438990266824523133530824905756066075) * 10 ^ 70 + 4944382036586391953241442734802047920244288088332165619877170615279036) * 10 ^ 70 + 620473221740441804908863440761958696797200395697758855639609858286809) * 10 ^ 70 + 7339871453291351294850115649249971937901777209932462886316566543158716
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_352 :
Polynomial.coeff recurrence5Scalar0Left 352 = -((((2346289498475325663262113612002199720964923689 * 10 ^ 70 + 1955872878160488908648128400094913577163970643263920434142857676028361) * 10 ^ 70 + 1048746397207146059211346004483752174843628829501292770824107788793112) * 10 ^ 70 + 4133028436010222818857135609322971147256185344058054481479939552605664) * 10 ^ 70 + 1255279508736509441247251543684015884362158184802137307832199443436060)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_353 :
Polynomial.coeff recurrence5Scalar0Left 353 = (((610498595252305402878012962944759774107801034 * 10 ^ 70 + 6982509467962306516060113401663447235348523392114917685498831575945948) * 10 ^ 70 + 1283383702244332695336571324731637729117047878127432890178096232930825) * 10 ^ 70 + 6807822066233168677909498601690927935747812735004234494765594921539394) * 10 ^ 70 + 7492647767888701978756627257435445984136551434564167989455633748076412
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_354 :
Polynomial.coeff recurrence5Scalar0Left 354 = -((((141866901424745152563001830062219744070245291 * 10 ^ 70 + 1045596958607796207945658099822778062409336854199539794543751208929155) * 10 ^ 70 + 7556061583334508046556402425454631012724867918062867920338868483976049) * 10 ^ 70 + 4701784508695676315752985132593175661479148452786925500221001627975512) * 10 ^ 70 + 90978244843441706221631475362407319001353611717619122680829744052145)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_355 :
Polynomial.coeff recurrence5Scalar0Left 355 = (((26002417964176006053077378497663148472905506 * 10 ^ 70 + 7111231570626789555998744853903574224214679551949908465401110766093619) * 10 ^ 70 + 1293389833004107865324037256569949339878855581143970217394517218822979) * 10 ^ 70 + 2746682030350558982299352755213191092186664364169785250417732471775782) * 10 ^ 70 + 3374754186759274382636639353558302541320368235268846010313905769152100