Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar3ShiftPart1.Coefficients234To265

Recurrence 2 lookup certificate: Scalar3Shift 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.recurrence2Scalar3Shift_coeff_234 :

Polynomial.coeff recurrence2Scalar3Shift 234 = ((6 * 10 ^ 70 + 8045112059301782945780800692558710711581184574241101631341839838506014) * 10 ^ 70 + 8520659286525495891774749200242768780454407723510359305779171034354904) * 10 ^ 70 + 8818062023040775208207502741479610030940292063453615306095599884844573

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

Polynomial.coeff recurrence2Scalar3Shift 235 = -(((3 * 10 ^ 70 + 5251186836675077885064813179853698429630606207730253459155540266402354) * 10 ^ 70 + 5449933989482978960676790434869531104266916876637859964535052649333430) * 10 ^ 70 + 3040933154233733680974824277701076221937308496909375563919550314594656)

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

Polynomial.coeff recurrence2Scalar3Shift 236 = -((984252315886437165465272901889807588565959753757488067490617742110750 * 10 ^ 70 + 5202068715169340572201285517512607751227985388086345743876669654143370) * 10 ^ 70 + 488964344945328994826940919991387096201882053629932623520875289361931)

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

Polynomial.coeff recurrence2Scalar3Shift 237 = ((3 * 10 ^ 70 + 6963161410301239299304872681862656343919442431848883708379592272340954) * 10 ^ 70 + 4267467853709040147521367714865170854522681558997070000354969883922908) * 10 ^ 70 + 8460609424631224088214293686543475547101383079867429296793565321744804

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

Polynomial.coeff recurrence2Scalar3Shift 238 = -(((6 * 10 ^ 70 + 9072396539457650997187971182897199905956887441849893768295281520732350) * 10 ^ 70 + 9036098248370291390822365854967136855367784572060583601440303000701027) * 10 ^ 70 + 8317755256569570617387742539115807641209539170364893311137980278549862)

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

Polynomial.coeff recurrence2Scalar3Shift 239 = ((9 * 10 ^ 70 + 4353331412208176487728233583895461914830613139315329121573860052358408) * 10 ^ 70 + 6159019028746097716767956109065174709925524353965829468200616952092140) * 10 ^ 70 + 5717788785070567213100829144143253473092864707940573361027736172427918

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

Polynomial.coeff recurrence2Scalar3Shift 240 = -(((11 * 10 ^ 70 + 923930921084437246309583676987449646378936985777748087313132041086381) * 10 ^ 70 + 6572588182323750676847907371948660574399277318249191518483681501248444) * 10 ^ 70 + 3189992927714045832742095880252022295203285215096157031780382970057863)

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

Polynomial.coeff recurrence2Scalar3Shift 241 = ((11 * 10 ^ 70 + 8174640468439531275500698535259594564831135181134516118004254582247713) * 10 ^ 70 + 350579451028221591933414870317184185133623190898836601474297004074358) * 10 ^ 70 + 6939334514467009851456096338407951867654769139474082725266220418962164

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

Polynomial.coeff recurrence2Scalar3Shift 242 = -(((11 * 10 ^ 70 + 6717862858096654344588263454636186454072119356617169279007103285533187) * 10 ^ 70 + 4942971211854935863241420939975459277959300058835856654058807617650324) * 10 ^ 70 + 9057295381041927111175019887813911803171982034568858050493586755303695)

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

Polynomial.coeff recurrence2Scalar3Shift 243 = ((10 * 10 ^ 70 + 8129057234213537802355232294393282881871845513245738775811943967386359) * 10 ^ 70 + 1866036823986771538232463505412492029971086796948266629193612177886037) * 10 ^ 70 + 7960040738799628032383304001791841827418613580917270093364611539460231

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

Polynomial.coeff recurrence2Scalar3Shift 244 = -(((9 * 10 ^ 70 + 4559593539979105971679067176488783463900945285735970384263950695248621) * 10 ^ 70 + 3966962651448622468687510433337958784570281747282111281259581753597952) * 10 ^ 70 + 5463403967046370558207165322924264498923957374620146058007292067616394)

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

Polynomial.coeff recurrence2Scalar3Shift 245 = ((7 * 10 ^ 70 + 8318044631045677750875763542469797164502820223912959584675843287245905) * 10 ^ 70 + 3097533177715394353328045194933119549794669138192910826491098441768200) * 10 ^ 70 + 9221632322922395161840116913453258334659447018954308575277708477838588

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

Polynomial.coeff recurrence2Scalar3Shift 246 = -(((6 * 10 ^ 70 + 1506958671426531711499865630458447543265145300483161930269439805374414) * 10 ^ 70 + 8440842368812900342040048790841922696106614149511324980620351895620844) * 10 ^ 70 + 2263269325705196082084109789736369004434623749193487710849968458554087)

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

Polynomial.coeff recurrence2Scalar3Shift 247 = ((4 * 10 ^ 70 + 5773335898575245331611528533098595660696095249079278732483465375001383) * 10 ^ 70 + 3727656572452565357054868684321081972594711995078232888784673006958584) * 10 ^ 70 + 2681968465656518106530512335977479382681397487857414629300949144634822

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

Polynomial.coeff recurrence2Scalar3Shift 248 = -(((3 * 10 ^ 70 + 2194236926733089289495745494197106512548505723185807673865883664558868) * 10 ^ 70 + 7689943911644543887726056502026791502467228140169446396369794152177863) * 10 ^ 70 + 9072586284494718683411935540378462272158844150796757128914131873098168)

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

Polynomial.coeff recurrence2Scalar3Shift 249 = ((2 * 10 ^ 70 + 1285363256010973058383140410945403464926806384951216589266513157671900) * 10 ^ 70 + 666148262442981777625470300041432060275988889978427958161744269143774) * 10 ^ 70 + 5265862028066264395391507486466602444921785188451364687025831689414764

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

Polynomial.coeff recurrence2Scalar3Shift 250 = -(((1 * 10 ^ 70 + 3097892661814497713285262287490107815660782258234770001150623753093058) * 10 ^ 70 + 5967321878347539983074509457215553394945623137879911638487715526778832) * 10 ^ 70 + 1323003940529454134571513053499959107752863789061232534727592280162596)

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

Polynomial.coeff recurrence2Scalar3Shift 251 = (7360224859718040417402655663425804284306570643082329452095655459692366 * 10 ^ 70 + 6497884352461941395658075584646840837521508282983454152325469314733933) * 10 ^ 70 + 8126343533578355334508000651674390630187397199833956124414261377070789

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

Polynomial.coeff recurrence2Scalar3Shift 252 = -((3624957825526599451431771535649959566173903707574013306075113029799292 * 10 ^ 70 + 2580241263299541169678615973961616724717419440574894569180251750408672) * 10 ^ 70 + 7159893312326737544414159828823660125178806588343610196869244555798778)

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

Polynomial.coeff recurrence2Scalar3Shift 253 = (1392888845477761998976544713546866413719294633855691071633021945153591 * 10 ^ 70 + 208347392063773286153975511803929087542774307512638318804872519218409) * 10 ^ 70 + 2138472311569613670030100087539589497799169805836711412409500649875216

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

Polynomial.coeff recurrence2Scalar3Shift 254 = -((199893631578718522613034946648294576563547879190859459062639050843008 * 10 ^ 70 + 3417025723397558525480151907266355802575290651014386891827652515398397) * 10 ^ 70 + 8960012038931590285114301307495211073893705850163130121288304355381592)

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

Polynomial.coeff recurrence2Scalar3Shift 255 = -((335069410781554841584343714977542234950644045131385392377908981566794 * 10 ^ 70 + 9989534184391702339633320603375998733662476589312614535838316573789320) * 10 ^ 70 + 2511207740010961577353290034011587155462643616475761814513947761925617)

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

Polynomial.coeff recurrence2Scalar3Shift 256 = (494250009998212231706990034622879093975352592580998828976097989031774 * 10 ^ 70 + 673316659607892043555148874154810227377725728452018868279220957306278) * 10 ^ 70 + 6089995855997920932660201596179830217288867223242849518109513041632378

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

Polynomial.coeff recurrence2Scalar3Shift 257 = -((467344076984016909215660691612052339201419348116219163204089072078001 * 10 ^ 70 + 9258899321271034131121148837295496295040795252148709397754906307514480) * 10 ^ 70 + 4228945999837492975085774415617559482424292265009228821312567689656423)

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

Polynomial.coeff recurrence2Scalar3Shift 258 = (369276234898076585446257959226395237216526671389265382563085627207147 * 10 ^ 70 + 5345410757683098587917550165821808827291758824195617269554531030987643) * 10 ^ 70 + 9870230700816445995463126641424190238382276469000917932033356141784564

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

Polynomial.coeff recurrence2Scalar3Shift 259 = -((261316781596460011421887814291232272715811947005139684063427600949727 * 10 ^ 70 + 3856920586473306548025595918293139271346580834846310325061971459242374) * 10 ^ 70 + 9622164551836938980967811776648379710298694147652412667637188231508063)

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

Polynomial.coeff recurrence2Scalar3Shift 260 = (170321424225756766466611502444353512136477469813944023499247451372974 * 10 ^ 70 + 8820743660107055081602232114749259648737306171431310011552305861571731) * 10 ^ 70 + 1335315738975679790359944180743487075160639055884253501372709638035144

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

Polynomial.coeff recurrence2Scalar3Shift 261 = -((103646902410212983992206825950174210730084065637612008527997830718464 * 10 ^ 70 + 3535752693528520527029331072655792735635997022657401558116528770326358) * 10 ^ 70 + 9736875138625978434843764386578201630314159531313450026590134027853202)

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

Polynomial.coeff recurrence2Scalar3Shift 262 = (59297558041482507808099918298639257394377847646181755717358564416758 * 10 ^ 70 + 3904574044954808157391637433808366041070399952348734407448780257284361) * 10 ^ 70 + 1478987875120665723473856803116535009703740113081178822171605972846598

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

Polynomial.coeff recurrence2Scalar3Shift 263 = -((31994520742208810021337784450820105089111286458391130181207449221784 * 10 ^ 70 + 5489961893990492759501410536706195203245437219803112675898647218520010) * 10 ^ 70 + 1219844117910104713476337933226459435378944900875342378838986873855060)

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

Polynomial.coeff recurrence2Scalar3Shift 264 = (16287897578842022291783637759802897905549022013695655596584546463002 * 10 ^ 70 + 5328717529721306833318807642801189631945269241027164512856303703218541) * 10 ^ 70 + 5481156193249220171953146455181912619641743999787071255013183922394052

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

Polynomial.coeff recurrence2Scalar3Shift 265 = -((7807326802297351195630673231149276767836519066037224975947649281772 * 10 ^ 70 + 1103065408295855748673119391301120436699896863127339434741061711361556) * 10 ^ 70 + 6949968591200129453837454015279662326064000650762366199477825749592534)