Recurrence 2 lookup certificate: Scalar1Shift 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.recurrence2Scalar1Shift_coeff_235 :
Polynomial.coeff recurrence2Scalar1Shift 235 = -(((96 * 10 ^ 70 + 3484717578812104269677688796001658795728047916189201735102609300962182) * 10 ^ 70 + 624966814672203935414241457535320389235703599963284260788586824690207) * 10 ^ 70 + 9238178499975802403095978784042685746163787830893008156189509631366917)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_236 :
Polynomial.coeff recurrence2Scalar1Shift 236 = ((81 * 10 ^ 70 + 593393074316921027608406742977787432690065616324887312603043295040860) * 10 ^ 70 + 9694465376379476607633747701084908484832602856533580989268844550235706) * 10 ^ 70 + 2518901410816918094993987034972073184113841862659649414262405437785809
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_237 :
Polynomial.coeff recurrence2Scalar1Shift 237 = -(((58 * 10 ^ 70 + 9445324609038172165734062486114933271551241843775246114110945267330655) * 10 ^ 70 + 7816758410685583673428316653032293579718715418696940008241815924677963) * 10 ^ 70 + 5083469110808353267861979059792007467288098483312874447485120412999243)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_238 :
Polynomial.coeff recurrence2Scalar1Shift 238 = ((31 * 10 ^ 70 + 7922217235146544895569359243360094762683202198149890241321032213258714) * 10 ^ 70 + 287480270616432643320415240740536373985036756114390829630288933789988) * 10 ^ 70 + 5244587599352438982462385796195050374685966038846955364258829636797923
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_239 :
Polynomial.coeff recurrence2Scalar1Shift 239 = -(((2 * 10 ^ 70 + 695734594461655728333251547210832881760623491206342528715614747861517) * 10 ^ 70 + 2768624055169191550895790212024111289427322607650847797284829259419991) * 10 ^ 70 + 7164061783079552120555504855361519829856209258914143719124679484980054)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_240 :
Polynomial.coeff recurrence2Scalar1Shift 240 = -(((27 * 10 ^ 70 + 4458839357332496031897660012661676778052884549999887214913172184146525) * 10 ^ 70 + 148836882616849456620159688196200352506347034573962444341556135808000) * 10 ^ 70 + 4093855276136399615120933066294141896524402112240124348916770174165591)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_241 :
Polynomial.coeff recurrence2Scalar1Shift 241 = ((54 * 10 ^ 70 + 826046364469761228375845614326265022960608275144588723128091800853651) * 10 ^ 70 + 5716084905044629039051172690004304352757779147763905388172416474611946) * 10 ^ 70 + 7439354821270418096185379269559106055973128326707652796065747569047906
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_242 :
Polynomial.coeff recurrence2Scalar1Shift 242 = -(((75 * 10 ^ 70 + 6546017260300816438408643235421168651191666757578856503835542328964914) * 10 ^ 70 + 3677340879711084132767855658101544235247644694545221512980636722183507) * 10 ^ 70 + 3657922005882900548105801718627750007739727792516021750202382539364820)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_243 :
Polynomial.coeff recurrence2Scalar1Shift 243 = ((90 * 10 ^ 70 + 7328331397179326858723791984424425968921205970450602064136175116451668) * 10 ^ 70 + 4859644485329067535918655580677848275409781806051720427825537070342783) * 10 ^ 70 + 9678908429968798063384981833197235182454336062600415333224833148522817
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_244 :
Polynomial.coeff recurrence2Scalar1Shift 244 = -(((98 * 10 ^ 70 + 7663886409124956618101602889040572623480259477815370096579896574053419) * 10 ^ 70 + 3631987575745932773025146214910989253578360918070027686725060804156281) * 10 ^ 70 + 8714242632643812707097696265816529212027525017540273855177654562527698)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_245 :
Polynomial.coeff recurrence2Scalar1Shift 245 = ((100 * 10 ^ 70 + 479092821337045604481531576924234326575997605860019838869876969710606) * 10 ^ 70 + 6283410947421131253947509177538512290117525592091525344298677757586692) * 10 ^ 70 + 9802124863332978044168704043598853947028089950182747118491155541357982
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_246 :
Polynomial.coeff recurrence2Scalar1Shift 246 = -(((95 * 10 ^ 70 + 5508400332649772155696213632229986093587591476365520221970302621017255) * 10 ^ 70 + 9882241544468278381984104984056394863821907933996732175271093921736097) * 10 ^ 70 + 2962326429804302031122375560944583940564148890937831702220382947711549)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_247 :
Polynomial.coeff recurrence2Scalar1Shift 247 = ((86 * 10 ^ 70 + 6880296558643878068335221743657256379567562107312414700497966240259303) * 10 ^ 70 + 7098130854375262834188042756918581206798069404368260109524148172174232) * 10 ^ 70 + 9930810831145095518498013386533709664982245078466933415589502339870183
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_248 :
Polynomial.coeff recurrence2Scalar1Shift 248 = -(((75 * 10 ^ 70 + 482325782438218668182786889333316411050948626135008150544441485575826) * 10 ^ 70 + 1621348849897646343495344707506859845403976000162224443189070552955419) * 10 ^ 70 + 3383860008620993956456462251144782353476026574166602370018582390334877)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_249 :
Polynomial.coeff recurrence2Scalar1Shift 249 = ((62 * 10 ^ 70 + 1602959383921383861336461839818498537370769721679093896588299561631186) * 10 ^ 70 + 1193029701578648041191321880879448589991554341728710109553783511697395) * 10 ^ 70 + 102337450116657417674384790547293124804674880735622890257176953792098
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_250 :
Polynomial.coeff recurrence2Scalar1Shift 250 = -(((49 * 10 ^ 70 + 3187394867180060881898915181432918150818195592919926691974712478305666) * 10 ^ 70 + 9604900106151726267543615098791889553775610366517378352384202125854975) * 10 ^ 70 + 7669156666079364162102762190805324767001254886747632439608089805531591)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_251 :
Polynomial.coeff recurrence2Scalar1Shift 251 = ((37 * 10 ^ 70 + 4849712274566393532908473149126204506165711818530949284950040572298253) * 10 ^ 70 + 60881903467538844818985425944715352047507682177315378342616295068745) * 10 ^ 70 + 3982697486533657600635232840946490378604014689898708123929931763822727
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_252 :
Polynomial.coeff recurrence2Scalar1Shift 252 = -(((27 * 10 ^ 70 + 2608543573824986935350238714743580108105725628766620259374088062777961) * 10 ^ 70 + 2434133142987385158135977044301358948862531517374548883121069620709127) * 10 ^ 70 + 8556453244338287932378100629084683647258566311592473321013681443429384)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_253 :
Polynomial.coeff recurrence2Scalar1Shift 253 = ((18 * 10 ^ 70 + 9191826668835279971140865907071779895331775212850202793069450255199421) * 10 ^ 70 + 8972001698033672766458783526109244210616359263986217300698162543559978) * 10 ^ 70 + 8227987707214992767402104454830117459068068941809925886790485078988505
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_254 :
Polynomial.coeff recurrence2Scalar1Shift 254 = -(((12 * 10 ^ 70 + 4699804549497340266594540505121408265379902062049368376513098378564657) * 10 ^ 70 + 9203783388054047402784133893255566240754102713949151826544401135135375) * 10 ^ 70 + 9038089083951152093593667234406501625164663126704454065265073753629610)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_255 :
Polynomial.coeff recurrence2Scalar1Shift 255 = ((7 * 10 ^ 70 + 7416701833723312772851526657683327060657010669295347584686423185130917) * 10 ^ 70 + 2722925170666785834614064659894557558546419160351720552829371570982982) * 10 ^ 70 + 2695309298230283313674519736102659901375928914783307246917144788156277
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_256 :
Polynomial.coeff recurrence2Scalar1Shift 256 = -(((4 * 10 ^ 70 + 4601978997947637868876119492065875135115601997553244737897106105750744) * 10 ^ 70 + 8591141030713793458914776490670085854437179695934064111288533457927303) * 10 ^ 70 + 6388528602715380279262255030106249358520465224821517069314813812160158)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_257 :
Polynomial.coeff recurrence2Scalar1Shift 257 = ((2 * 10 ^ 70 + 3150554376668383364611119098114497072663961081262620587386738947993460) * 10 ^ 70 + 8061977863965891950529523453659950965447137752587202220373468919273597) * 10 ^ 70 + 5256175478780274260965696855259186994151361942013529894845146651665565
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_258 :
Polynomial.coeff recurrence2Scalar1Shift 258 = -(((1 * 10 ^ 70 + 70105323585018599251832832134811064187453614216379673769359880085740) * 10 ^ 70 + 2099475772432148288662793009489296115843413892695252337703827109956697) * 10 ^ 70 + 7250233486728409406838640977437675457714857202607384575912254929027760)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_259 :
Polynomial.coeff recurrence2Scalar1Shift 259 = (2771039330040028663010828350999171959545563384290667109997646697726799 * 10 ^ 70 + 3535662453734003999718209245160479318586048812003921566237501235515991) * 10 ^ 70 + 422366466767509728058338469394564530804087538709170016137359957223252
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_260 :
Polynomial.coeff recurrence2Scalar1Shift 260 = (803978640672244478718633561997806941193423005798021445680149666729001 * 10 ^ 70 + 5833464275165179048158025002899659707865319298699600948814599416739275) * 10 ^ 70 + 6812874543742519420071054117452607564481100159676983025888703203022712
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_261 :
Polynomial.coeff recurrence2Scalar1Shift 261 = -((2168797692300353286441443357649223643029930910508017631824385178937271 * 10 ^ 70 + 8341418019492297662804771317697722321703238519060866712727018490709064) * 10 ^ 70 + 3319317660083569225355664990651994283585571957660154215629112206448090)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_262 :
Polynomial.coeff recurrence2Scalar1Shift 262 = (2356271255661626949613909805350819947552262485077708068274027114918018 * 10 ^ 70 + 5274620525288010827192254927350322773962120717973716668754430583229569) * 10 ^ 70 + 9540992262190070910247987004058823671918591286191279126266822584443332
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_263 :
Polynomial.coeff recurrence2Scalar1Shift 263 = -((2015852154748102692927597152613867166692192962358288235405105400151705 * 10 ^ 70 + 2593383237713782798681831978951285108742885983738951314637657863377207) * 10 ^ 70 + 3937458994830197698029209993537125923021482214155759489485686419858573)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_264 :
Polynomial.coeff recurrence2Scalar1Shift 264 = (1517757368616306667961140524881346086753429139828956278100249991145740 * 10 ^ 70 + 5145031675306300839988696224739964826983785509360036364703749529932888) * 10 ^ 70 + 5303857964754657178950731823742518673349867484119581705877445849604821
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_265 :
Polynomial.coeff recurrence2Scalar1Shift 265 = -((1045970409752584959354711391062765139793655640033111940493433450606567 * 10 ^ 70 + 3345931766415168513998165722627062889880849997410702220420360408493135) * 10 ^ 70 + 8251925554557820724198637044663617016988618461428493936737214034909845)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_266 :
Polynomial.coeff recurrence2Scalar1Shift 266 = (671677192903006990703862282861431206391572846215817712610013104107740 * 10 ^ 70 + 1376040958435818591915124816817140313349985691923691187729425714607656) * 10 ^ 70 + 5438488683466812705327192327726234508053215290302118009506094861043963
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_267 :
Polynomial.coeff recurrence2Scalar1Shift 267 = -((405526565691597300887807699257210297626836156982414501178738562651509 * 10 ^ 70 + 8726184432520824535412862268563624531308028653523205802054489285870520) * 10 ^ 70 + 690652747275663219556444759452937872806180816841865440920526940191946)