Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0MainPart1.Coefficients225To250

Recurrence 4 lookup certificate: Scalar0Main coefficient convolution #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_225 :
Polynomial.coeff recurrence4Scalar0Main 225 = -((((140097805114806458355469202 * 10 ^ 70 + 3385372836537997491965795596973707572746433627514738538060086860375135) * 10 ^ 70 + 4886882402357810141899590656907064850482012041248839566915583757128426) * 10 ^ 70 + 7715507916943339376740406880990713755228326923290478808066262898574640) * 10 ^ 70 + 650722485249590584678295674740330926161151869206713526978113433989531)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_226 :
Polynomial.coeff recurrence4Scalar0Main 226 = (((200732559734524803685068694 * 10 ^ 70 + 4149135063346897559486216107631969167821285562373099710132421296100050) * 10 ^ 70 + 2021277908921346876707997364927774675942116377362248234336703783270638) * 10 ^ 70 + 8307982952253656937974937969994344038866345541617911189063533867252632) * 10 ^ 70 + 5108800412456472550302043527010940831689820328630312329061358730807089
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_227 :
Polynomial.coeff recurrence4Scalar0Main 227 = -((((283107176512928375988451676 * 10 ^ 70 + 5203228446242456175471581271088828114486483753873658284081070308751728) * 10 ^ 70 + 4455562045281244915559597056435928348646287462440419859472544439968479) * 10 ^ 70 + 6489759866342076013934465868945987801979371793088528316964117380584238) * 10 ^ 70 + 8191552612380983982954995846117236971886660192504972435255412625609230)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_228 :
Polynomial.coeff recurrence4Scalar0Main 228 = (((392931714660697324066882935 * 10 ^ 70 + 456436729656667462784910264755748813722321818138894640739399684692654) * 10 ^ 70 + 3713676357276153017101970758242825285596261579849794996200088616741350) * 10 ^ 70 + 3982048184950267714432860405976980034284019778472680499356916705530402) * 10 ^ 70 + 7361378838570936030111285621350041475815611780107258143627979595155515
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_229 :
Polynomial.coeff recurrence4Scalar0Main 229 = -((((536515815879589323963049577 * 10 ^ 70 + 9091960781952156054330086653991352177764759065391087182053102909953505) * 10 ^ 70 + 4613319811921442343064428175391082438741818729406302507559042354390350) * 10 ^ 70 + 115763312927694541057475723978084511667961909053668602619951182340555) * 10 ^ 70 + 147979983537679719700382660810417986779200773827454662594964425288297)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_230 :
Polynomial.coeff recurrence4Scalar0Main 230 = (((720423521989912734934058858 * 10 ^ 70 + 1795727384686597425824667012253365027971247400326452445908103258058213) * 10 ^ 70 + 8370912622252690371259707256225675575628972405399835827305957101921377) * 10 ^ 70 + 3763941193689705258347995983004048739039073061740199312737644429751859) * 10 ^ 70 + 5329136244520933249097313693115471431944281267039754367108416308900346
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_231 :
Polynomial.coeff recurrence4Scalar0Main 231 = -((((950915372675416542635250040 * 10 ^ 70 + 8356700885356546587526265428785367663418625984790582287647954696853821) * 10 ^ 70 + 1306280453540272328247019726669887202055510308874763107233841164220975) * 10 ^ 70 + 8486111555588365616933985483013530449648970199841789535790849709189682) * 10 ^ 70 + 561048960407905590907816673599480104999745164033909290740129739108036)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_232 :
Polynomial.coeff recurrence4Scalar0Main 232 = (((1233140220133989119002057795 * 10 ^ 70 + 4119306064860100819465212037465508470081493533700585432207149549155069) * 10 ^ 70 + 7804449880305015748374012441533737411276159413019674574251815821565847) * 10 ^ 70 + 8833749967114345857984946290210410673408965838057721149948650842433470) * 10 ^ 70 + 2818098698743626407572222814154521546880241799134165155099002511375877
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_233 :
Polynomial.coeff recurrence4Scalar0Main 233 = -((((1570054948954223646715648813 * 10 ^ 70 + 782337612150866440212900165063091830315747974004949845605668933190570) * 10 ^ 70 + 8010977397768913509716422702094718236263276183343752054963232050485556) * 10 ^ 70 + 7717345944170361038287553390818501723498531942617042130156985958128567) * 10 ^ 70 + 7705632605524098504117547919115679673661411058420975184902026792842164)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_234 :
Polynomial.coeff recurrence4Scalar0Main 234 = (((1961076403263019081393583265 * 10 ^ 70 + 8994781590254016014325759175229608927971006044844003580983707867250256) * 10 ^ 70 + 6355373335491911386758380557791461088035674783037897199746734238031097) * 10 ^ 70 + 1948494556926186419187622861288615210550799276558902864186186531768210) * 10 ^ 70 + 9186013926665700220636703625232621978032901019240804403696475292246142
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_235 :
Polynomial.coeff recurrence4Scalar0Main 235 = -((((2400506673596582658453674769 * 10 ^ 70 + 463805546874145345178875635749902685540275408625345247200847870864770) * 10 ^ 70 + 4519770729750880801018445979700755181044863210821942944962019929048853) * 10 ^ 70 + 7057606340084973720291541793125713412291237109322606593030614356986402) * 10 ^ 70 + 5766073654247240964236928999795562966612879030572512437824151612208970)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_236 :
Polynomial.coeff recurrence4Scalar0Main 236 = (((2875819157709807281428921661 * 10 ^ 70 + 6758324308268623233326122468149455236324851468269640541917831327272883) * 10 ^ 70 + 6881750232252837682019933198758590305655820258222306944013147443726088) * 10 ^ 70 + 3533215556912008766316873170902587534398239227865042447788011207121064) * 10 ^ 70 + 3234973777367811443677469075054282697159335915179575258889644466783218
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_237 :
Polynomial.coeff recurrence4Scalar0Main 237 = -((((3365945004846543213295839773 * 10 ^ 70 + 6601680529618940653439841698886093790807233804634632360360038790273917) * 10 ^ 70 + 8637453689976884824061397538469688333237999141400381670760043543779412) * 10 ^ 70 + 1187065319928791214125837093159366657295870063315822026162047418731723) * 10 ^ 70 + 3706462124542919964587199133164158699684935056073277785777606556177491)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_238 :
Polynomial.coeff recurrence4Scalar0Main 238 = (((3839751848235163888633406390 * 10 ^ 70 + 3903720584868259652122261078225603654189560984935053027398858214053093) * 10 ^ 70 + 6797943423632402191390123276150590132577804466377884372824839963312458) * 10 ^ 70 + 2754827491574037272174447395595221492761961434412984540628855858628285) * 10 ^ 70 + 148105140764671354788580894711385745525794040769097483006577845212702
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_239 :
Polynomial.coeff recurrence4Scalar0Main 239 = -((((4254951122408924917040065357 * 10 ^ 70 + 5545974086999427416059568275753418535787451908184225729089620409306530) * 10 ^ 70 + 1426347046920719778000123178590137200837911986381804205343159988240011) * 10 ^ 70 + 8708024666440508359771172272560991153187334267701502726907396154147982) * 10 ^ 70 + 995658312842192386474062033056895510549686850164849789128687741797483)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_240 :
Polynomial.coeff recurrence4Scalar0Main 240 = (((4557697257390557519003770556 * 10 ^ 70 + 8334839157253535594553523145850813228619315584277364436861511654189901) * 10 ^ 70 + 7138946980665257622006354121203354537028673990371371295605396221352597) * 10 ^ 70 + 5368058469654962335604861309866819702151312484489289807149035356054293) * 10 ^ 70 + 154666154002929432461597455475621632374128588501153092048396648649094
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_241 :
Polynomial.coeff recurrence4Scalar0Main 241 = -((((4683141863502441544112566955 * 10 ^ 70 + 7595241660436043927848477416042183493955931844774950010484833542727492) * 10 ^ 70 + 1481237875546321284789781289549374505979697286119597892460053477845281) * 10 ^ 70 + 9376524820824053443746947036712106362067491565369977312013590087635356) * 10 ^ 70 + 6193184747283318917016368032946415461731940496555645206232888228006816)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_242 :
Polynomial.coeff recurrence4Scalar0Main 242 = (((4557170262285831750027954067 * 10 ^ 70 + 6846793741230076706013834997676448943175666268820903912401397338930283) * 10 ^ 70 + 3465407693768194725420162593723271901549055787881651289421218599341388) * 10 ^ 70 + 624875843242158468540830660034250225313364079659974225099824195161251) * 10 ^ 70 + 6683468631017731984532911213766293051534337637698439403829108861814896
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_243 :
Polynomial.coeff recurrence4Scalar0Main 243 = -((((4099471251934925218096505555 * 10 ^ 70 + 164250415368836368636891284397703248345915465115319468092143591117174) * 10 ^ 70 + 8240213650091670174251937739342216261593872778208668923307341178757397) * 10 ^ 70 + 8655468786063499002625302474166011599891854674420401158731151143821476) * 10 ^ 70 + 8537521427307331808992366955036564624493472546305527696998917810405849)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_244 :
Polynomial.coeff recurrence4Scalar0Main 244 = (((3227973810886439310184804158 * 10 ^ 70 + 4995052074833937480539845072261423572436878600424841679482659640647475) * 10 ^ 70 + 1206617096090354550972327026964569856813342131045346250939478179704490) * 10 ^ 70 + 2773422226880694921298282318058615961843847049179017705330406111599640) * 10 ^ 70 + 2741246805675546467197095941503924596880325125966930256634915833766179
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_245 :
Polynomial.coeff recurrence4Scalar0Main 245 = -((((1864533037804197387886230220 * 10 ^ 70 + 7462909865852540049489143663124097697359439101971153035641317157100760) * 10 ^ 70 + 3407433816681927484576095954287477383335948083580456934282184358418485) * 10 ^ 70 + 7666874010236134563152013047676009189222208163682151575473500615492086) * 10 ^ 70 + 4783285341016479091069579819570619139032559715594013519705080243950311)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_246 :
Polynomial.coeff recurrence4Scalar0Main 246 = -((((58424468134759004578128461 * 10 ^ 70 + 7029731726901060440945060712392355614815709467808463891377767427888542) * 10 ^ 70 + 7195683948234038446584492424126300165819887586345253242080706968159990) * 10 ^ 70 + 1014143812847405590950170520816812488147362860725507963343336003267465) * 10 ^ 70 + 2978796614508444886232965141013706409381213272323921907311563318112425)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_247 :
Polynomial.coeff recurrence4Scalar0Main 247 = (((2590758448223446627294169559 * 10 ^ 70 + 3671632993508097040981778023476937503767093843983174691766009425105972) * 10 ^ 70 + 2900230225838578916104897548841503881523650999900655356662391840341137) * 10 ^ 70 + 2833619884611493428274664310694054697812454492095099642114344007702615) * 10 ^ 70 + 1343191221508743014085611952027266093508638443337935695938650571030969
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_248 :
Polynomial.coeff recurrence4Scalar0Main 248 = -((((5757588013082425598326873354 * 10 ^ 70 + 215942138776316726848535388954179983609827544255485907991543500134176) * 10 ^ 70 + 5490926149302739051601165753547242209554240737948613319063380350230841) * 10 ^ 70 + 3131388205910870994014603919720026694315862078979767730212093290921133) * 10 ^ 70 + 7661713667490955445623146490796244254408241064484528638590810984488304)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_249 :
Polynomial.coeff recurrence4Scalar0Main 249 = (((9553092021058903259202409412 * 10 ^ 70 + 6632247870150128687919839742711508416312949054776591982782272742398922) * 10 ^ 70 + 3749104258584417605747792365749130488713020581818311916896383241832043) * 10 ^ 70 + 1178449448511742207087377229186698557504774455387005457064722738044253) * 10 ^ 70 + 8080036872222014346031518627720227089584029513148225423904461841496493
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_250 :
Polynomial.coeff recurrence4Scalar0Main 250 = -((((13935877327629295308042696280 * 10 ^ 70 + 1076926453556179557697547479773277544199213404231177399052240311152539) * 10 ^ 70 + 2302905656897223371521318989622619958188242004239595523865160277273898) * 10 ^ 70 + 7820911279010378460069188937036741574052124019110049299295436337847808) * 10 ^ 70 + 1797780355401107978624061339432919411303849478921014719185758210551761)