Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1LeftPart2.Coefficients298To323

Recurrence 4 lookup certificate: Scalar1Left coefficient convolution #

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

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

Polynomial.coeff recurrence4Scalar1Left 298 = (((298505724106808136595033 * 10 ^ 70 + 9709070564831079664314730560616275766885773761699838349703577911722979) * 10 ^ 70 + 4666039651821535305502248030938525385327437302797961535128400837660293) * 10 ^ 70 + 3076206769853532853719875287437604182688447762052683526057340356187198) * 10 ^ 70 + 9734875493012384103754336620891399471814561020121095015024767676855276

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

Polynomial.coeff recurrence4Scalar1Left 299 = -((((158246961392889599965573 * 10 ^ 70 + 1216253707406683204750469025865964402697930956704691617816226931606470) * 10 ^ 70 + 1080540260055573928553431531236933834091400398154021413528755258736985) * 10 ^ 70 + 5901675602514607872988715347256236689340256790781050653333692685973440) * 10 ^ 70 + 7144417128423498455681695701727084821554659165287102354043109532969528)

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

Polynomial.coeff recurrence4Scalar1Left 300 = (((79212140155311631548758 * 10 ^ 70 + 8318656244861817499403356616477524120221511835825944084321468890731517) * 10 ^ 70 + 1139793058659837384801232105355998205643372947481290899317571179300769) * 10 ^ 70 + 8703991623657761256818610640072311990112097702845452128929001135376218) * 10 ^ 70 + 9539223415309285859339998869029309396018774143208271854086544226152903

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

Polynomial.coeff recurrence4Scalar1Left 301 = -((((36479106844970464686947 * 10 ^ 70 + 6060617661163451945429089100024049049348580869188810352245111552075367) * 10 ^ 70 + 8392706079995106294282159454344517900373390393003522949531259058444068) * 10 ^ 70 + 2794335450082803143889822674753117730773615007443654386223258780896549) * 10 ^ 70 + 2045683004396889839692918999601834050142169063510937638994335807456927)

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

Polynomial.coeff recurrence4Scalar1Left 302 = (((14550145322564285157226 * 10 ^ 70 + 7476216100452526860544829139974260693790515193845072551228715438784690) * 10 ^ 70 + 5034468966329809721840029465682181417758637032740902828752322500728999) * 10 ^ 70 + 3241787280063746293096774391189328490138559206596621712678357903246758) * 10 ^ 70 + 535181431131280234098859506187247379763479850185053957091836774996546

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

Polynomial.coeff recurrence4Scalar1Left 303 = -((((4082481589372699592769 * 10 ^ 70 + 4784468977610538497695348203399379621685163164704765878886257426138894) * 10 ^ 70 + 2647997032559623389320163877996168790110694197622225772677114508243859) * 10 ^ 70 + 2649670812239917990817666714387071015074353503325864293235989616133037) * 10 ^ 70 + 6328880940571725237956212947197804226784565545349673074298899888793313)

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

Polynomial.coeff recurrence4Scalar1Left 304 = -((((369168070521994027473 * 10 ^ 70 + 7672226584054724927715799839667052894822486621720303606285271588618594) * 10 ^ 70 + 9451747702104204983618348523991233326182274459202175314620996091582874) * 10 ^ 70 + 2856806268678165405229282196710342636676754816280858677749267372191369) * 10 ^ 70 + 9172973200354116715773504865652486246223097998060647218396549503617272)

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

Polynomial.coeff recurrence4Scalar1Left 305 = (((1859537029476705585357 * 10 ^ 70 + 796946414303068938343561506973300116966155446538464636644736558482045) * 10 ^ 70 + 3970942586642570259065183909432489858492521259579157776830585170161592) * 10 ^ 70 + 6282628412520803241718606318555312057821228666169522215504037705604768) * 10 ^ 70 + 2416693839448386715553191491707851852681497633999829315651823630599259

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

Polynomial.coeff recurrence4Scalar1Left 306 = -((((2026042089798332336952 * 10 ^ 70 + 6432080467971793745308605821339139514532404939982733930819982498317648) * 10 ^ 70 + 282669405248144980200964313187547147893903877311104731482149343307758) * 10 ^ 70 + 9713839725568718309101970910286350966200172672729820422152890520352283) * 10 ^ 70 + 715181517929347403498883080991904558265328950127282837556163709515548)

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

Polynomial.coeff recurrence4Scalar1Left 307 = (((1696735036231757251746 * 10 ^ 70 + 2420890270346940762540037196783706893631541114824589988325720676140663) * 10 ^ 70 + 1191827800205712545904531059006353579831390670086194820335161137971832) * 10 ^ 70 + 8796226236613906785297490717400322641978500842468503631929064580469472) * 10 ^ 70 + 2572912031689111273778532774464187752110975917867796626905006414663568

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

Polynomial.coeff recurrence4Scalar1Left 308 = -((((1257140970557205035620 * 10 ^ 70 + 4770028208996739799469408518665084731939471968557761291693479721638946) * 10 ^ 70 + 343801552997333197480156656570752018934076070629382542578513095063919) * 10 ^ 70 + 1613005631304499124739646278116947523272315071425693372153850452165419) * 10 ^ 70 + 555609995333404639463643876686215612472492927465386992744495226848229)

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

Polynomial.coeff recurrence4Scalar1Left 309 = (((863491282783739514710 * 10 ^ 70 + 5591784514389128494857092640253431072213224957778974853759703500864172) * 10 ^ 70 + 6544454920159385851113427430918552074178032977388407105416366308367601) * 10 ^ 70 + 8571481984611945626189308705315650625470059462714329507104459202431292) * 10 ^ 70 + 3356004166097881767138082470903288483534154300040451499456865192479708

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

Polynomial.coeff recurrence4Scalar1Left 310 = -((((561553586257572158609 * 10 ^ 70 + 1839671801071905134771103594237629948074327840354518799160488395249127) * 10 ^ 70 + 4841062925298853631283340780635091542466358248801734090340175938229421) * 10 ^ 70 + 6280168585059875157048164987598727415528917205861502812470043274292936) * 10 ^ 70 + 9247913402830320682534681983087353471043363046775178405982357536910517)

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

Polynomial.coeff recurrence4Scalar1Left 311 = (((349593815646457863343 * 10 ^ 70 + 5495145637222492748476783392231546024141785898347157278096192791332984) * 10 ^ 70 + 6552164595939665340813723219009392872469347847191031685643254322485980) * 10 ^ 70 + 671856386751952679876397146571529042270718524337401060751197277886752) * 10 ^ 70 + 2646657320210134104910856538518972109471416905619995932817825700243163

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

Polynomial.coeff recurrence4Scalar1Left 312 = -((((209619174859093697046 * 10 ^ 70 + 8331644631619242327366167341350649340480321721755106551944897746817968) * 10 ^ 70 + 5179119869480648552280431814551932723034174519083154782032553250007769) * 10 ^ 70 + 1849000508150264951792584650858384634336550571923773808784507477325060) * 10 ^ 70 + 8976247632440756811291935753252261001418377740436924650865763106630076)

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

Polynomial.coeff recurrence4Scalar1Left 313 = (((121459228004893647603 * 10 ^ 70 + 2456349906761169319628765615836977995949764128550205121061379155555057) * 10 ^ 70 + 8471745697117898359844386617301861309032545027621007065322271910812193) * 10 ^ 70 + 430390088747260975250543535394131180209341956581109943958894769285386) * 10 ^ 70 + 8772840115739799248516244883642363973044898775880722936931259852232281

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

Polynomial.coeff recurrence4Scalar1Left 314 = -((((68104318182377182089 * 10 ^ 70 + 2014856911550883284172963380195767051399223554035061370822659592101842) * 10 ^ 70 + 9240413996225561456552996522072589195598070544113961410672924425169457) * 10 ^ 70 + 1515582100908098576543178884572535465171504255955163328617993606373865) * 10 ^ 70 + 4889238901952129708482603497951867030369869895619234295683275828390529)

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

Polynomial.coeff recurrence4Scalar1Left 315 = (((36948426982327170076 * 10 ^ 70 + 3601279215581879238799779652646571353737580489061752204471702736280739) * 10 ^ 70 + 3234713243810729818299694555331884144823182941569352849207972906446067) * 10 ^ 70 + 6899041736251438948920337997315099165021757507440930512499417721453651) * 10 ^ 70 + 1981618009557710882532743453829212555632362953630269099884637314264510

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

Polynomial.coeff recurrence4Scalar1Left 316 = -((((19360972730896280550 * 10 ^ 70 + 7096990024385375530333986732965278068608414382990322094611804430715058) * 10 ^ 70 + 3665714241812979666561098094280703279173550212260325658557507018316092) * 10 ^ 70 + 2460357662418097049669412800438119675162680020280695419379103292545904) * 10 ^ 70 + 7521509977925338710235884672830376362237675176086061027425780279318842)

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

Polynomial.coeff recurrence4Scalar1Left 317 = (((9761243882719601944 * 10 ^ 70 + 6335390937723085314303607880278762335377650006194309027442586813763280) * 10 ^ 70 + 6800399030420649191302554073367127539819154124288276664196261137568642) * 10 ^ 70 + 1978382025350514596233492732767897402890382659848640192029846731316906) * 10 ^ 70 + 2527745912975204884642070843961885176842496225478183498500624948817541

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

Polynomial.coeff recurrence4Scalar1Left 318 = -((((4702011145023603980 * 10 ^ 70 + 6268850673254962672991696401337116028477776604098098581808147001874200) * 10 ^ 70 + 3790541266222064536866767987913763561859773912188118125798667265013541) * 10 ^ 70 + 7764421250811643631872168876690671020163945953789203191983956339761615) * 10 ^ 70 + 4951879260308005330402026867989015409432722344014099163023413312996115)

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

Polynomial.coeff recurrence4Scalar1Left 319 = (((2136494512867850827 * 10 ^ 70 + 6870269382161906340383038330313703500778090136531198044689069462584957) * 10 ^ 70 + 2528552868296909733008737140426381534725689647271987982966474905187541) * 10 ^ 70 + 2979713950961268078204461031037261954020429971838456039143114484748122) * 10 ^ 70 + 2581943774800699592007319476747179551621515694711015773802147569033624

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

Polynomial.coeff recurrence4Scalar1Left 320 = -((((892826103881173593 * 10 ^ 70 + 2137026365276225792491258434718053432360875063751983228269611454243709) * 10 ^ 70 + 3036239565655509262309113613869312346537686287455547412694817633537568) * 10 ^ 70 + 9347302800067742999885528039744086082365130066010172958180232295481789) * 10 ^ 70 + 1574081103910193743781974059625702986754038862570993724110463480862176)

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

Polynomial.coeff recurrence4Scalar1Left 321 = (((323311104175079773 * 10 ^ 70 + 4785318480861609991942195428572516260843429682761632096471556580071508) * 10 ^ 70 + 7175531584465729455885839151376836671157754934082985279011820317426060) * 10 ^ 70 + 1062685667292467618172156370614033281259625072730015360744759251237643) * 10 ^ 70 + 9514699749735564367783374195341548966780443297830418918324775803334517

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

Polynomial.coeff recurrence4Scalar1Left 322 = -((((82619800082825421 * 10 ^ 70 + 1881583189052069792686692525964221260879475934144143124866579118491288) * 10 ^ 70 + 929944633517737212387703209249595876372511849906002542015411960993314) * 10 ^ 70 + 2087977763805953528434713136174070209375048699112830165135307768417252) * 10 ^ 70 + 805725930502623783729860507011302397141344438388118180663843220058670)

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

Polynomial.coeff recurrence4Scalar1Left 323 = -((((6372292869014522 * 10 ^ 70 + 717129633836327006759414077743692762757433843255140158287865141817898) * 10 ^ 70 + 2585544596918897858433650241731296071573846783229443380644666592416606) * 10 ^ 70 + 7478099577599895415400349223685516922296535218551711553907894670770694) * 10 ^ 70 + 9975010158599862727109872980414066784435421047149911709701097081147714)