Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar3MainPart0.Coefficients152To192

Recurrence 2 lookup certificate: Scalar3Main coefficient convolution #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_152 :
Polynomial.coeff recurrence2Scalar3Main 152 = (31155902323561879166588726801992628309973 * 10 ^ 70 + 5859933665711478086349533498334934182465017153177548420893726147263941) * 10 ^ 70 + 5132287319139431603136909950436291581845910118960126699624399654417125
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_153 :
Polynomial.coeff recurrence2Scalar3Main 153 = -((626346134245919073862412718408090364684590 * 10 ^ 70 + 1073641627632721100074008098672630793873010795657667366853563152560197) * 10 ^ 70 + 1936863641021630409459917505491410637413798767312532761320778647472103)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_154 :
Polynomial.coeff recurrence2Scalar3Main 154 = (2021365242858217329613662209713478251613971 * 10 ^ 70 + 8451964765081169377509112632476821089378602329604871189879798111051828) * 10 ^ 70 + 1111633806080650274658261429507323456801148635277753898188186432591793
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_155 :
Polynomial.coeff recurrence2Scalar3Main 155 = -((466867460138513294080647170806320166574387 * 10 ^ 70 + 8265045114787587226998616445428811838030541643838001750223904439391443) * 10 ^ 70 + 4792058459539226567531684871126054160341911639595962410525420179124232)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_156 :
Polynomial.coeff recurrence2Scalar3Main 156 = -((20384511314122723217915829756383538015750427 * 10 ^ 70 + 4551852486737883298757008088380429997629606922273874446578449563167865) * 10 ^ 70 + 6637616111710634383053036684047578007637102104269285455951990708989007)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_157 :
Polynomial.coeff recurrence2Scalar3Main 157 = (77006005024165561009242362760480695769232779 * 10 ^ 70 + 8667095747459296252803707707653605700044259230668063088369396506638230) * 10 ^ 70 + 5502348156229684359865386147105761705592377822663750005690941779120046
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_158 :
Polynomial.coeff recurrence2Scalar3Main 158 = -((52140371786254635752314467262647103519195092 * 10 ^ 70 + 6246011103750974053808243272228861948948268622104187558922030899588002) * 10 ^ 70 + 5937947197021381798757002329485207625257766340992622429482859163507089)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_159 :
Polynomial.coeff recurrence2Scalar3Main 159 = -((623487910897617841552067200953201715807407266 * 10 ^ 70 + 9189074984967884107386841521894807331469891857978569019864408478295402) * 10 ^ 70 + 7198576992371261792691395111907804895677199244729871289805562725329656)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_160 :
Polynomial.coeff recurrence2Scalar3Main 160 = (2622674053308970856040366943252435638934121098 * 10 ^ 70 + 2385515920281665914853508812940256440723126408774775569247683463761958) * 10 ^ 70 + 1340696732676770639226293018588241924453156106796845616607633936406129
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_161 :
Polynomial.coeff recurrence2Scalar3Main 161 = -((2169616168288012802174581716478738014680242103 * 10 ^ 70 + 1957206329809454184252652410548030861040278770147770734360732627561027) * 10 ^ 70 + 9112295516456625540146105811765112834114826983846964982406695960829640)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_162 :
Polynomial.coeff recurrence2Scalar3Main 162 = -((20788345887391282642976567057754539428300018514 * 10 ^ 70 + 7751700266140420569817951672957673415791428189346897965443385661317194) * 10 ^ 70 + 819109726152223012551297749095592713272777036052032102161617663570541)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_163 :
Polynomial.coeff recurrence2Scalar3Main 163 = (95198755141560674141963367117689625523516111155 * 10 ^ 70 + 1139384895790821223039681084546338844561590810855271724302015399449679) * 10 ^ 70 + 8924356602615153387565702444070565997451754835194056929355854507824080
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_164 :
Polynomial.coeff recurrence2Scalar3Main 164 = -((108037713737241653665098640286763166593632734974 * 10 ^ 70 + 4298380206073111456409342745544996989443642450523962641360862320313637) * 10 ^ 70 + 857020927911759759287102693650052378765509161013996487976283896800411)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_165 :
Polynomial.coeff recurrence2Scalar3Main 165 = -((656196011045536059976450592097276762740054135105 * 10 ^ 70 + 7595087660405195078034491642738585993766934041276061976558895424195859) * 10 ^ 70 + 3115003067827365439686638197191726637828129078507804875099935157466462)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_166 :
Polynomial.coeff recurrence2Scalar3Main 166 = (3620019065607129036962741302621935897792194524503 * 10 ^ 70 + 2214103071095799128747580442145106359256245353483510050843814680827752) * 10 ^ 70 + 2361718376948472023095990603356596413398550079744675735544207769462771
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_167 :
Polynomial.coeff recurrence2Scalar3Main 167 = -((6624186303711728732212275751968027211265582044037 * 10 ^ 70 + 6217399416645983959456426667698182209884330369427609693432366426343466) * 10 ^ 70 + 2074765044612298930587835478158585072905526622115985167000585820862954)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_168 :
Polynomial.coeff recurrence2Scalar3Main 168 = -((12824517184691660280849859561142337338837003771625 * 10 ^ 70 + 9585299859704980540688002234657171880349357669721078742530622418248635) * 10 ^ 70 + 1763941857088662506820128157099202663529426550164930127813098420474620)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_169 :
Polynomial.coeff recurrence2Scalar3Main 169 = (117475725449067778655000822031355172476357674201927 * 10 ^ 70 + 1092607555301376455611649124101857800865856836140215365354608366386982) * 10 ^ 70 + 966686392110633721143120358151976109545204537938443760264596148468419
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_170 :
Polynomial.coeff recurrence2Scalar3Main 170 = -((324624036413727647721103078544435999498327576821930 * 10 ^ 70 + 7500092954223616389669578456093635673485778465815141326337190579364500) * 10 ^ 70 + 3810711981175240114306672165784797920675583119116987189279570835141660)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_171 :
Polynomial.coeff recurrence2Scalar3Main 171 = (105720314695561731024157053911811822029240212910999 * 10 ^ 70 + 7174507450102430272629454984334471940709359751526531149494705297848114) * 10 ^ 70 + 1347050465554633625501931121264839686538961941866254258248316436343041
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_172 :
Polynomial.coeff recurrence2Scalar3Main 172 = (2676642613153712837414575867047189828342474586760515 * 10 ^ 70 + 1759747835295855901117936522462036257920684704176595016434459817782580) * 10 ^ 70 + 1614325766484407539390748812533250375035234573268426041300499882197298
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_173 :
Polynomial.coeff recurrence2Scalar3Main 173 = -((11233798566024202579456157032640825851243627578135744 * 10 ^ 70 + 3295023587778605519624509169961637296146862127775936430473975389927864) * 10 ^ 70 + 776413054743378211413223565659739289584563575481495794360618372765125)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_174 :
Polynomial.coeff recurrence2Scalar3Main 174 = (18661290051481535262743539295206806707673994492117647 * 10 ^ 70 + 1297077754168022124200506087847822801209234116431885519425969750170047) * 10 ^ 70 + 1293005080851361804135248672354556219513320831759783391555097624671156
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_175 :
Polynomial.coeff recurrence2Scalar3Main 175 = (28453697598929416458665535450712861704034119503534313 * 10 ^ 70 + 6297490025611086034590869675083447077907073983685079458786400972504402) * 10 ^ 70 + 734562827957627524517230473260462996251292787722780813376319007251382
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_176 :
Polynomial.coeff recurrence2Scalar3Main 176 = -((269644916056950727320742910198692481387446263062309303 * 10 ^ 70 + 407162238798962675143453513856161520763767427072420724610314350955012) * 10 ^ 70 + 4264860536838800627708475954947210604012082214367665165407901732350031)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_177 :
Polynomial.coeff recurrence2Scalar3Main 177 = (777005840037157884923088569682186939665470105166206852 * 10 ^ 70 + 5101883323078277839085403140011623812361760355364286028712280516194338) * 10 ^ 70 + 5794587037555428162263723228248387461948223620029848270456307010779357
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_178 :
Polynomial.coeff recurrence2Scalar3Main 178 = -((675144027943994330173024991469090453961928212389346264 * 10 ^ 70 + 5440800338283662161430442229073775411111876173833301205595691195943338) * 10 ^ 70 + 4399081153543126045359699099111424963693875417443312836899441834585212)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_179 :
Polynomial.coeff recurrence2Scalar3Main 179 = -((3861163034700429878423062189586748245499432406405479077 * 10 ^ 70 + 2093984432578550791576793023951955116945894988649274674554710334164509) * 10 ^ 70 + 2563083709036260744100422109801117783119710133025779876448382395166611)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_180 :
Polynomial.coeff recurrence2Scalar3Main 180 = (20091187815133324059360823004104370479394935838046441612 * 10 ^ 70 + 1344598664152211073557480363628643968004602346205930152152760581621509) * 10 ^ 70 + 1983789461077733005780773709364690098426152234717976395453474728613741
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_181 :
Polynomial.coeff recurrence2Scalar3Main 181 = -((45183786026659436427081474112862166213245165858313659692 * 10 ^ 70 + 412353725675379459913235033611308322783834725348718435362858369082457) * 10 ^ 70 + 2557261004860104902639092577366642547451580746226102698884009263743816)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_182 :
Polynomial.coeff recurrence2Scalar3Main 182 = (12978259246160078033593743843587508520664860644271628563 * 10 ^ 70 + 1340067907487255606253908381551560826138869616466656304543777739382515) * 10 ^ 70 + 9025001165259789316381163999930117337319741539797642809861711975082675
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_183 :
Polynomial.coeff recurrence2Scalar3Main 183 = (301846316629198700747596594764516633495214386537217537416 * 10 ^ 70 + 6506814083778171613663796063828658770966027205609825736658304710622987) * 10 ^ 70 + 5465611033611994091806384340831883731330848855205412151371237644925652
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_184 :
Polynomial.coeff recurrence2Scalar3Main 184 = -((1250977696902708446286072791373296150842194877922726004710 * 10 ^ 70 + 6234698233223007421655815472322829131176988998455529324969191996025824) * 10 ^ 70 + 7086601215769106425669924577556625246572549261105349378743065099391433)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_185 :
Polynomial.coeff recurrence2Scalar3Main 185 = (2512160189630570368654721704159366159332510159310412692852 * 10 ^ 70 + 3603420778121636925602459384885972988871865444524989205208159731135102) * 10 ^ 70 + 9072535231388703337367862454749936096267753976674239711599648107204421
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_186 :
Polynomial.coeff recurrence2Scalar3Main 186 = -((373570193514700442555636286380849826525447891821915441273 * 10 ^ 70 + 4596662641368696612218675651839952768838344597642626827997272288984275) * 10 ^ 70 + 8348844664715124525109811202271975947786892978363795803248316994804124)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_187 :
Polynomial.coeff recurrence2Scalar3Main 187 = -((16798354631833669072124888945368218349514598376743376016777 * 10 ^ 70 + 386051908051530369650672034423951515790509348411779404532631875059430) * 10 ^ 70 + 3806173950880359269452830635508189569705407378742812763089894515244098)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_188 :
Polynomial.coeff recurrence2Scalar3Main 188 = (67076836583370618777443061257268228597229605264739959906748 * 10 ^ 70 + 3849198176040826412427554444284215075903623086955145354444457261982285) * 10 ^ 70 + 1934380784259057822495216819065659514756694950025568619019606298726609
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_189 :
Polynomial.coeff recurrence2Scalar3Main 189 = -((139826287769266632616288799394781309316890901821984554083723 * 10 ^ 70 + 4725049169528630307471185223035130695427491932239774192797714139632076) * 10 ^ 70 + 6725715067556203839356265147607258336167046279075352750667653934934472)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_190 :
Polynomial.coeff recurrence2Scalar3Main 190 = (75957469240409178580776775392698719132635492073991671701503 * 10 ^ 70 + 8979571627133718418809237614050261755514871356823432228646757793440415) * 10 ^ 70 + 7366923943045723897752563243722066580375520310353779038685018986618075
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_191 :
Polynomial.coeff recurrence2Scalar3Main 191 = (651189022506494288630058012942151837922777553264360969206814 * 10 ^ 70 + 7451545496406432576445095306764843606135077680665414942461644840512089) * 10 ^ 70 + 5257972154241405516068499084572530920409194735401965103198510130691483
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Main_coeff_192 :
Polynomial.coeff recurrence2Scalar3Main 192 = -((3003210161840119728712963600377263213500596299857648836527159 * 10 ^ 70 + 1211373378738377830581626360153320202328077227009672605549073747428825) * 10 ^ 70 + 3977447757428099110890441282452892848018531054364708655808653831102934)