Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar1MainPart1.Coefficients235To267

Recurrence 2 lookup certificate: Scalar1Main 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.recurrence2Scalar1Main_coeff_235 :

Polynomial.coeff recurrence2Scalar1Main 235 = -(((4096 * 10 ^ 70 + 2082893075962217283925870183899038880267081796914842052567704199339640) * 10 ^ 70 + 8208772037701378664389336621192250461093026669696366543594001690124137) * 10 ^ 70 + 5229284107722884141487661184382885738051260247198391522464039205433724)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_236 :

Polynomial.coeff recurrence2Scalar1Main 236 = ((4365 * 10 ^ 70 + 1228554065547759951187053549284554733613616263818372361661202640879512) * 10 ^ 70 + 3370020406969512434995770518252849159762763076091154512925018813449500) * 10 ^ 70 + 4425262240106871375142864289951267810563579457038695697008701386037573

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_237 :

Polynomial.coeff recurrence2Scalar1Main 237 = -(((4398 * 10 ^ 70 + 4846644526498622927632321676275701306339611040649402485223152390408107) * 10 ^ 70 + 6749604967290583988210885481155170012591238864466666173225802845155996) * 10 ^ 70 + 7538215389350341011167266922483873841896099364523630369254948226038541)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_238 :

Polynomial.coeff recurrence2Scalar1Main 238 = ((4173 * 10 ^ 70 + 3123262039851427531467883238530326877957809874192193564746094087768289) * 10 ^ 70 + 2531221461915202169739162931695605403184897959075977263575515051876113) * 10 ^ 70 + 4962225696017001320296082023247300734653525571989464812631475656277769

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_239 :

Polynomial.coeff recurrence2Scalar1Main 239 = -(((3698 * 10 ^ 70 + 8714552099617417714007630631154020520438500389518839695086505316709366) * 10 ^ 70 + 1459287388427575209996768620839198633090231378258946271718378715818900) * 10 ^ 70 + 2229261842746312682847357080388618940796920206096950811768926336113415)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_240 :

Polynomial.coeff recurrence2Scalar1Main 240 = ((3016 * 10 ^ 70 + 7174750151902602169821813177094661894253335535783327739948926654310725) * 10 ^ 70 + 7618191956050980954679475222551570391549792296630701311679289766877904) * 10 ^ 70 + 5199257958084223702319867908650425113646733577450907566365939914382293

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_241 :

Polynomial.coeff recurrence2Scalar1Main 241 = -(((2194 * 10 ^ 70 + 7259171196801948911016853764073373984858580486892322253914217831769937) * 10 ^ 70 + 9841622381752400552153353370987281168362166869010049740292819499329954) * 10 ^ 70 + 1303521859500026987237391961947973224885759066919143018479355064294845)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_242 :

Polynomial.coeff recurrence2Scalar1Main 242 = ((1316 * 10 ^ 70 + 2957751062927109707720179160913496359833141726729877963891253647644772) * 10 ^ 70 + 5380562168676708849379216148385781557235997565991669722747184593632224) * 10 ^ 70 + 8381749172388425641001305141595725328045576697793560047577196045906152

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_243 :

Polynomial.coeff recurrence2Scalar1Main 243 = -(((467 * 10 ^ 70 + 426893759347303083965585399500772297037239418338194077189625722913620) * 10 ^ 70 + 8741346845168199569632710101690087079392856696614268179162804170761081) * 10 ^ 70 + 960216759072266519292659453770720829784028666022139912594046385031570)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_244 :

Polynomial.coeff recurrence2Scalar1Main 244 = -(((278 * 10 ^ 70 + 1879638016087133038505487170816926321697686817269377406632633423166034) * 10 ^ 70 + 5934803336903109903450806942807384021388671131733786821946366480427762) * 10 ^ 70 + 1530673222824589491247545417660374943080562193320192118457918129498507)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_245 :

Polynomial.coeff recurrence2Scalar1Main 245 = ((865 * 10 ^ 70 + 3860196388379293984331178414424322874701703948924016712239238807252636) * 10 ^ 70 + 6801121971993166673028024459484719290539974175803397155989199970380615) * 10 ^ 70 + 3534484114450407840413806693731975869787966384742958681303905663523757

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_246 :

Polynomial.coeff recurrence2Scalar1Main 246 = -(((1266 * 10 ^ 70 + 7818222639082220061548081444366896061247767873936473964944648265085278) * 10 ^ 70 + 642590285234650917113303942022774723141074563844722060554757327793110) * 10 ^ 70 + 2137488634118456882139317825857482661885260226963458150715781173722457)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_247 :

Polynomial.coeff recurrence2Scalar1Main 247 = ((1481 * 10 ^ 70 + 687254858275304530983205424094291878962991375327780014233061968368612) * 10 ^ 70 + 8311387159441788030319055552169690566233340268084338064822920772280305) * 10 ^ 70 + 3949606266953113163450254238750045930252214595699867194521194279289594

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_248 :

Polynomial.coeff recurrence2Scalar1Main 248 = -(((1529 * 10 ^ 70 + 1222631921344218095908298059669534454361775402519916178532092928854801) * 10 ^ 70 + 9585385378914822994770750695662770674941396976531026836493399246185424) * 10 ^ 70 + 116614403702666379246055804708705909723564022960762282482327616378239)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_249 :

Polynomial.coeff recurrence2Scalar1Main 249 = ((1446 * 10 ^ 70 + 7690867414160543739158735822650505593113268751101046854280090741299778) * 10 ^ 70 + 3345089461569930828609777082939762041912538399302293854875469550995310) * 10 ^ 70 + 2267859939979553433685549613537982840381535896652882960149597327062275

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_250 :

Polynomial.coeff recurrence2Scalar1Main 250 = -(((1276 * 10 ^ 70 + 5234777561601781795754860277391254667588774227184444647377734162679694) * 10 ^ 70 + 6752198657933738949530159997604305781844629922199693004238507683219042) * 10 ^ 70 + 4373831110238916169889909548498603719349480410289889036190785948994457)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_251 :

Polynomial.coeff recurrence2Scalar1Main 251 = ((1060 * 10 ^ 70 + 568620715386329557866361609665440268909060039266759682327439143171782) * 10 ^ 70 + 2325674044821404730317595140517469338245296497638407755895491986859343) * 10 ^ 70 + 884288103008557681286720008999216863122760540971833229015543599902858

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_252 :

Polynomial.coeff recurrence2Scalar1Main 252 = -(((832 * 10 ^ 70 + 6335203998331017620528901509070821721967047520518059119012924781949110) * 10 ^ 70 + 2472730033802644284460267660724740548456242535694697320244523711947346) * 10 ^ 70 + 5651846938533329372682850896931035026046641867598407289890562206148931)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_253 :

Polynomial.coeff recurrence2Scalar1Main 253 = ((620 * 10 ^ 70 + 481104456783836600579715738040454982949973850308420024351777497263927) * 10 ^ 70 + 5677923532597774045821977018109733251062508771514123290892627541726859) * 10 ^ 70 + 3993760438173654796290753395320765754942924904979561646302418584234075

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_254 :

Polynomial.coeff recurrence2Scalar1Main 254 = -(((437 * 10 ^ 70 + 9502611880576491169244681548255851152016598821153084737891185043304793) * 10 ^ 70 + 1769083358691779947450173968031283399176718809089738178774068827263282) * 10 ^ 70 + 9585751366840788661223592125632362849903552165604377214774219431115512)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_255 :

Polynomial.coeff recurrence2Scalar1Main 255 = ((292 * 10 ^ 70 + 9875744322938838782461310955308129692840460309273389578899259352773211) * 10 ^ 70 + 3813852389009589465873872575207991546782745119045943757867077066621274) * 10 ^ 70 + 1712976776133858232354225820154861462380352831497199113183191416183096

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_256 :

Polynomial.coeff recurrence2Scalar1Main 256 = -(((184 * 10 ^ 70 + 9992954968669436493859390187158866714438074486230893174119246683392511) * 10 ^ 70 + 6690351718490959125493662913762934754228138681997779662044542022837124) * 10 ^ 70 + 4437581902483706269458794292398986406155358628187330100286311498854594)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_257 :

Polynomial.coeff recurrence2Scalar1Main 257 = ((109 * 10 ^ 70 + 5236873297834168545340052253345608532846633893358869548301436328476599) * 10 ^ 70 + 7248388347975856056527139757966563885985341037167637719202502356065792) * 10 ^ 70 + 9237659754198656735638774091080802301060718626587140946988508748841859

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_258 :

Polynomial.coeff recurrence2Scalar1Main 258 = -(((60 * 10 ^ 70 + 649729157059450671504987947721047001853910349732250635022413225633181) * 10 ^ 70 + 7848020241915006927974130802587642336492745423484340626666071797849312) * 10 ^ 70 + 7310902725618307775271725449605949460689357023194237327976743859785084)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_259 :

Polynomial.coeff recurrence2Scalar1Main 259 = ((29 * 10 ^ 70 + 8076623382197473795128201189299096517012096844989337520554655546301268) * 10 ^ 70 + 6927240526015813556089794920275642279999094787728143079545244098769719) * 10 ^ 70 + 7366851870530670708720421375783106778528030823131543644871330165705078

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_260 :

Polynomial.coeff recurrence2Scalar1Main 260 = -(((12 * 10 ^ 70 + 6896595241220218332555925626656016082650362496570612366955087053457687) * 10 ^ 70 + 3956507535059168826701575441998323901844928126964904689627800983820954) * 10 ^ 70 + 8482246946901842827804443226425551042098906747882484858202320835906286)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_261 :

Polynomial.coeff recurrence2Scalar1Main 261 = ((3 * 10 ^ 70 + 9048292723968752546727977571896232149945324728233453415127148506760213) * 10 ^ 70 + 6841932475415129372657520959856791820578455428144162102208853265507555) * 10 ^ 70 + 5810661485132578165266039025794795277499409346293015401566134591551809

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_262 :

Polynomial.coeff recurrence2Scalar1Main 262 = (122439177466713039702019100012575315120519123173191214586796690951314 * 10 ^ 70 + 7688468150864059466032312552727757515647187182063104528838034663963605) * 10 ^ 70 + 1179816400556569128527466852867594468534323058019467865221042201412529

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_263 :

Polynomial.coeff recurrence2Scalar1Main 263 = -(((1 * 10 ^ 70 + 3503773843069112610896951935998250211632970567919154067187127931267501) * 10 ^ 70 + 1309348005585294287179681624660235644602837850884263027876110674656217) * 10 ^ 70 + 5537086886249322861029125893081512692975768522003922367188581157431869)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_264 :

Polynomial.coeff recurrence2Scalar1Main 264 = ((1 * 10 ^ 70 + 4922398435997782913308460092033835487528414500252538918347807655645173) * 10 ^ 70 + 7334803721633759903139326733646582238205338954756552710083596894931149) * 10 ^ 70 + 9434797459870710346919439439059321054641660139102421976383462142884682

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_265 :

Polynomial.coeff recurrence2Scalar1Main 265 = -(((1 * 10 ^ 70 + 1933187331609026927893435433166409094642894249486465959187633635909486) * 10 ^ 70 + 2097803706427840563755802620512311583202676082412430403545111674280149) * 10 ^ 70 + 9191895774106835087834406625783327447298827746955959899058376396805626)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_266 :

Polynomial.coeff recurrence2Scalar1Main 266 = (8163704262503732913354300215683498571593836810073344753061547979364445 * 10 ^ 70 + 8082272965896262011490984943422064422831050276466493048650103190119226) * 10 ^ 70 + 8785647793872775018835325571878255712229514629182571440515883998369988

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_267 :

Polynomial.coeff recurrence2Scalar1Main 267 = -((5029492904395262397738265546831104388201411728900319851851764503001455 * 10 ^ 70 + 3341328064315923855600578466197325237117224155850094475532576771963732) * 10 ^ 70 + 9060743664591000106746956322801999954583864440966394413590336252584061)