Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar2LeftPart0.Coefficients93To143

Recurrence 2 lookup certificate: Scalar2Left 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.recurrence2Scalar2Left_coeff_93 :
Polynomial.coeff recurrence2Scalar2Left 93 = (110750537 * 10 ^ 70 + 4995669635804239534296981406371286107366875798566907658045346855113144) * 10 ^ 70 + 9961038416884765583141452005691749693937861754762286756775966311017216
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_94 :
Polynomial.coeff recurrence2Scalar2Left 94 = -((480618954 * 10 ^ 70 + 4187930798802087809635982444135270656968560902869196564171259162137220) * 10 ^ 70 + 6174566730615133035107483511756973278118252330677627398312176458221574)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_95 :
Polynomial.coeff recurrence2Scalar2Left 95 = (1995867994 * 10 ^ 70 + 840208892115475319013622326370805407553491351947249768036286983324307) * 10 ^ 70 + 7689112499589817929270241077084499237235259541027655908562686125084557
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_96 :
Polynomial.coeff recurrence2Scalar2Left 96 = -((7908057620 * 10 ^ 70 + 5540486363738516240764921395181744783010647754621221727860199039553092) * 10 ^ 70 + 869870350454211197482112877424361627301460337982884906691874443523109)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_97 :
Polynomial.coeff recurrence2Scalar2Left 97 = (29753391637 * 10 ^ 70 + 9208967099318128650818189559640235414801776678576127776354989385551877) * 10 ^ 70 + 6195738902538895848883022449654068233916569077860059210327873913635797
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_98 :
Polynomial.coeff recurrence2Scalar2Left 98 = -((105486408693 * 10 ^ 70 + 2920197326985262472210806823126484681852550358619061222431689618576429) * 10 ^ 70 + 3943136503327418033177315439347098628016557348539220542693472902592476)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_99 :
Polynomial.coeff recurrence2Scalar2Left 99 = (348109772068 * 10 ^ 70 + 646987760169022218681587676120995559056535529934714767638287019410791) * 10 ^ 70 + 2669835253533309567857371731028383703159144750910044415363662242083572
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_100 :
Polynomial.coeff recurrence2Scalar2Left 100 = -((1047388959452 * 10 ^ 70 + 3055630043844087336680505867862132319865875767805601909475097568192790) * 10 ^ 70 + 3431851935758510073060857296576852761961172693490102403278436093222549)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_101 :
Polynomial.coeff recurrence2Scalar2Left 101 = (2759123793250 * 10 ^ 70 + 4436006089038523505925148985959553812096876590694670963202441663407749) * 10 ^ 70 + 628203879068108087827573582239337744839225002103720888719262101308628
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_102 :
Polynomial.coeff recurrence2Scalar2Left 102 = -((5711470699689 * 10 ^ 70 + 5158524814152394345425984306369581810406162587924040042301374351188106) * 10 ^ 70 + 394851372440432662140215652624315386459180399768460869826228336819673)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_103 :
Polynomial.coeff recurrence2Scalar2Left 103 = (4939439120261 * 10 ^ 70 + 9214326135780747739736328897531505014302339485480813741884711227284589) * 10 ^ 70 + 4183911130841754581632373643363411306133412278359290830920179140895469
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_104 :
Polynomial.coeff recurrence2Scalar2Left 104 = (35049060282897 * 10 ^ 70 + 2901016378588714825129821331176752722315325777710256676487647625038608) * 10 ^ 70 + 7308906080731874383029978262060384437649980135216089853261286922892291
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_105 :
Polynomial.coeff recurrence2Scalar2Left 105 = -((294628083892778 * 10 ^ 70 + 6006164529103424179656909038303619906236925636469584085515981038333577) * 10 ^ 70 + 2580695116794888719482095224986045507210826777996240641303292567170666)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_106 :
Polynomial.coeff recurrence2Scalar2Left 106 = (1577523997002417 * 10 ^ 70 + 9117567535738913962118180721964072162974932058298931315316106994591869) * 10 ^ 70 + 3355470332640236053138468571821038117955276715918668349389258879251319
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_107 :
Polynomial.coeff recurrence2Scalar2Left 107 = -((7146726586652096 * 10 ^ 70 + 5678653428112982920323280855893833776989619865215998929346623405182403) * 10 ^ 70 + 9631302511395179571262401985709145371607260371671471282905814246198465)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_108 :
Polynomial.coeff recurrence2Scalar2Left 108 = (28783499981503978 * 10 ^ 70 + 6061486868497233682523057676129888152826969463640896078788572449709904) * 10 ^ 70 + 738872766876882472301154626611621610389298905559873378853614077290511
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_109 :
Polynomial.coeff recurrence2Scalar2Left 109 = -((101539121113156348 * 10 ^ 70 + 7551868558879037525371044358408408385431791899266583882654767909788972) * 10 ^ 70 + 7371097839370509223539173719557982337513715143044423376681893031554326)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_110 :
Polynomial.coeff recurrence2Scalar2Left 110 = (295147199332691408 * 10 ^ 70 + 6575454669281788409747840779553667543902256425917434202233117153526619) * 10 ^ 70 + 9980086912351720366981592961184720245342316469841236934139682445478348
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_111 :
Polynomial.coeff recurrence2Scalar2Left 111 = -((603037210445030539 * 10 ^ 70 + 8227675897735096385406038407284231872541427648185817486553350361090549) * 10 ^ 70 + 1570479626503393551660407044313768720304062641578076550695770513256975)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_112 :
Polynomial.coeff recurrence2Scalar2Left 112 = (327214845053100867 * 10 ^ 70 + 1580667912212795392157941570719431702306275607904707287058759273899971) * 10 ^ 70 + 609270008216939799828996486583890000795941047273016516240421730449547
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_113 :
Polynomial.coeff recurrence2Scalar2Left 113 = (2791505203595608298 * 10 ^ 70 + 5528195553966971435825822525347589861253251093973111743621044911786202) * 10 ^ 70 + 6788592377349290524621659500044288112934555299615143212147988331285603
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_114 :
Polynomial.coeff recurrence2Scalar2Left 114 = -((4660965901662127327 * 10 ^ 70 + 8777928592814333301248571977023417480918390189081219233959475632516827) * 10 ^ 70 + 8898011189322819150696292997825436835463339639547806066270346644658103)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_115 :
Polynomial.coeff recurrence2Scalar2Left 115 = -((69356656309833083646 * 10 ^ 70 + 826803773469910416112990821254987699794437632654296944374562513857922) * 10 ^ 70 + 6390696744432411506557306054353767820589073038035436283524808636260083)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_116 :
Polynomial.coeff recurrence2Scalar2Left 116 = (591132049616009560185 * 10 ^ 70 + 6590226633526149816552916329684546839585370209540193680058702546052107) * 10 ^ 70 + 3784603046274956313558621377840132212035268893423044296023231626034381
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_117 :
Polynomial.coeff recurrence2Scalar2Left 117 = -((2385268315679782208304 * 10 ^ 70 + 9619326207313067030350194096600439232876111796361525938364391242972826) * 10 ^ 70 + 5653362794518184824257584791692427398496528370806349974059788756661638)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_118 :
Polynomial.coeff recurrence2Scalar2Left 118 = (3675673711831537910988 * 10 ^ 70 + 3791040414879583335198097374498096964061972867794117835691204812487774) * 10 ^ 70 + 3434106324657396082072659228927284180030034670691417330198418681004654
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_119 :
Polynomial.coeff recurrence2Scalar2Left 119 = (20387067810673547168849 * 10 ^ 70 + 2220420644227886232639114249008983642245671186290737387161215869415913) * 10 ^ 70 + 7861293374270301008539667309477790390209869211934343126684498483924420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_120 :
Polynomial.coeff recurrence2Scalar2Left 120 = -((188948693330150072889785 * 10 ^ 70 + 1392628616119334836411130944592224070753835678261221294291490240892257) * 10 ^ 70 + 4704850616212331059073504804557281272072908562380980248039415156396368)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_121 :
Polynomial.coeff recurrence2Scalar2Left 121 = (819959092267795427192817 * 10 ^ 70 + 9235292478001085304336694895261968060681278354681758661526348029911634) * 10 ^ 70 + 2023394560513237542538648576152916041439527149873261022352306795300590
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_122 :
Polynomial.coeff recurrence2Scalar2Left 122 = -((2000008450998648168560548 * 10 ^ 70 + 6581300383602922494153546917506757369613900102431661475936919386709525) * 10 ^ 70 + 9195455862955669011682070767945545032174573412049912564592067282257073)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_123 :
Polynomial.coeff recurrence2Scalar2Left 123 = -((286508625990672102212959 * 10 ^ 70 + 8793813994707414679390281830315290321806533839920546957429868227156841) * 10 ^ 70 + 344284976658183777352780190472584319004302064102064610814931895404806)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_124 :
Polynomial.coeff recurrence2Scalar2Left 124 = (29477000068265375264372521 * 10 ^ 70 + 937182434223207626460541791191179667919572250625278307341911154336151) * 10 ^ 70 + 7250286497600628544817710693240273732534047600838729981873295385151395
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_125 :
Polynomial.coeff recurrence2Scalar2Left 125 = -((159436638158268716271420359 * 10 ^ 70 + 5656698873865363659162885164590177463811342622338465201158674421820510) * 10 ^ 70 + 2497885193493708807802537077890337017641258571705239226462225192590515)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_126 :
Polynomial.coeff recurrence2Scalar2Left 126 = (493727847568537859441292417 * 10 ^ 70 + 7958873600993537205471979384721145814201773190332412507254403595179098) * 10 ^ 70 + 328195972880713348463279165809311186666230691125682409316924532132509
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_127 :
Polynomial.coeff recurrence2Scalar2Left 127 = -((804274598873378963028854377 * 10 ^ 70 + 909997052603731307768899730880621486042812572690308178093381035434539) * 10 ^ 70 + 2838337364406448984081501525083507732603263662328557055134241370810749)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_128 :
Polynomial.coeff recurrence2Scalar2Left 128 = -((610417412017172978239604666 * 10 ^ 70 + 6134059342812843007596453179919163718362284638473768392928946242953415) * 10 ^ 70 + 5002779087565077849172843115592670902549381672359327471048817362041434)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_129 :
Polynomial.coeff recurrence2Scalar2Left 129 = (9970112345969774779205332378 * 10 ^ 70 + 427880742014842656109938676771765916157948240316682894036222050094118) * 10 ^ 70 + 9242332488349824889947062339511606444365282033203281972743293407336589
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_130 :
Polynomial.coeff recurrence2Scalar2Left 130 = -((62167275467623010426248473771 * 10 ^ 70 + 1202274939820260169652011961515732767701993362514596554388925258731775) * 10 ^ 70 + 6096353495467994665822142847580782463560293006422070907282566680856615)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_131 :
Polynomial.coeff recurrence2Scalar2Left 131 = (390202708230716084851433544787 * 10 ^ 70 + 8012708605404110295415912745530882881709475787491474040176882981134684) * 10 ^ 70 + 4684516646374927399022830306504620954028037055958046274269966192522011
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_132 :
Polynomial.coeff recurrence2Scalar2Left 132 = -((1948607952975093306933102461500 * 10 ^ 70 + 2937864640010854569433067082555523561831556975536007331949089967146097) * 10 ^ 70 + 1584457896185144552164998392145693277881411611521433559135005813749721)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_133 :
Polynomial.coeff recurrence2Scalar2Left 133 = (5338129563563850753221627419211 * 10 ^ 70 + 9705819205502101935653100792594129925882340132698988506543157209798291) * 10 ^ 70 + 2083032858523910509815395626188073444106837653671710104420975584455814
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_134 :
Polynomial.coeff recurrence2Scalar2Left 134 = (6915140193779832442769052647651 * 10 ^ 70 + 28311585555640404353729164193514892793430160866001612064321551945990) * 10 ^ 70 + 913026241269676191034529579976316393581756031436065450096431847535802
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_135 :
Polynomial.coeff recurrence2Scalar2Left 135 = -((142406237510490359732166699053264 * 10 ^ 70 + 3384186904319565676234206083806277749193503682252932792821996529565260) * 10 ^ 70 + 5589932306325415316067291954743848663247857971235773587186820938829983)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_136 :
Polynomial.coeff recurrence2Scalar2Left 136 = (641575748012554940701639866672881 * 10 ^ 70 + 5790810425655249490388209686558088162461313506021313593787508135914965) * 10 ^ 70 + 7590401964461333625102557322189403394520187499622515570929911952328377
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_137 :
Polynomial.coeff recurrence2Scalar2Left 137 = -((943121543616786591393813185590696 * 10 ^ 70 + 2201342167019073145014932844853658428846234407280807746675939210815219) * 10 ^ 70 + 75683049687187329430670233365665819226702251572103151537500912098620)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_138 :
Polynomial.coeff recurrence2Scalar2Left 138 = -((4755637732811673907958559254412108 * 10 ^ 70 + 9697892379630623126233099901548506000017071830528037777169079188120417) * 10 ^ 70 + 9036164980065071099619181968516041924510413315132771504871821626763213)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_139 :
Polynomial.coeff recurrence2Scalar2Left 139 = (31373410101635322863183060631842496 * 10 ^ 70 + 8120012600902031883455110294726681325154926449630785075410883095521754) * 10 ^ 70 + 1017870071978803278832513834338848301556075767353236041906971327667493
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_140 :
Polynomial.coeff recurrence2Scalar2Left 140 = -((56117131295889923502930875219832196 * 10 ^ 70 + 6381979460124733977416949170232516870197983816163565399525607666054774) * 10 ^ 70 + 238440523107569280260552476502169614678774819515091626738967775126452)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_141 :
Polynomial.coeff recurrence2Scalar2Left 141 = -((198555272826095366479696891782858040 * 10 ^ 70 + 68489366005921229416792238521561484643754569744706359748244894485004) * 10 ^ 70 + 8296443245048227937575866219921471982817683847045285603679664852006390)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_142 :
Polynomial.coeff recurrence2Scalar2Left 142 = (1377377562692175692561221473915166192 * 10 ^ 70 + 8632652763232251234326377030118023676917135364430026864167351942242425) * 10 ^ 70 + 4115661039536121228532264650646430320159761030850824244895647511752674
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Left_coeff_143 :
Polynomial.coeff recurrence2Scalar2Left 143 = -((1955264128165858640711612130657937225 * 10 ^ 70 + 5520466555153254858174517115275788996897671860354858506105593400661382) * 10 ^ 70 + 2351529906746694783423131813659959665684036431689525391355945379163171)