Recurrence 2 lookup certificate: Scalar1Exceptional 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.recurrence2Scalar1Exceptional_coeff_154 : Polynomial.coeff recurrence2Scalar1Exceptional 154 = -((1373493252948827173706131559996215899118646 * 10 ^ 70 + 7562806705554766288854957978747320663710299517694118068844668454162368) * 10 ^ 70 + 1518019080637522245917253189847443283756981199841659566172632984833366)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_155 : Polynomial.coeff recurrence2Scalar1Exceptional 155 = (8881954697975143346347704216353221095855168 * 10 ^ 70 + 5668616654365038815777676201086557641165178594279086915316879494637651) * 10 ^ 70 + 686809756015921444676521499838227791134915290985981718777235880775175

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_156 : Polynomial.coeff recurrence2Scalar1Exceptional 156 = -((26495090865598397781661678233730835404853281 * 10 ^ 70 + 4673274165456656505389341349015248595865418778971349163495379555164582) * 10 ^ 70 + 3377644915356764138245818973614165392742092306785017948672600053445537)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_157 : Polynomial.coeff recurrence2Scalar1Exceptional 157 = (31257238870591873116227485098646001451440525 * 10 ^ 70 + 3658705499547136230511043575620431968948284961798122197466409694209270) * 10 ^ 70 + 2408483238033266746218726002659488569866585568127351575516576362456544

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_158 : Polynomial.coeff recurrence2Scalar1Exceptional 158 = (119949805803655916457636816666883900563279092 * 10 ^ 70 + 5042786716713209539685075516642443189844946560199661237953940000716507) * 10 ^ 70 + 6429504952910308598045058296332388001568771798328752398309801122652502

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_159 : Polynomial.coeff recurrence2Scalar1Exceptional 159 = -((849526857478599543467109868883614851810979484 * 10 ^ 70 + 2588341550542455102337503901887324979849468655016823596700423196265976) * 10 ^ 70 + 3207597155085699026044939917332335712363801914998993996093394414347521)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_160 : Polynomial.coeff recurrence2Scalar1Exceptional 160 = (2720339417659130191395175444617669030784690708 * 10 ^ 70 + 5543402269135565920205301190444443229750633621263394396714225662192123) * 10 ^ 70 + 9039987751054599877012774713463014977842720668859642304963728312236424

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_161 : Polynomial.coeff recurrence2Scalar1Exceptional 161 = -((4431423224135279556027060710951884401334556043 * 10 ^ 70 + 5397836377787826593980352726329841901190916538115131037157802978935718) * 10 ^ 70 + 3546230935854080322243988417347948907150485339277013667633719031266656)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_162 : Polynomial.coeff recurrence2Scalar1Exceptional 162 = -((4719973674120112152520849735936349426694467938 * 10 ^ 70 + 9588546260558987300543161734156825662917796750887837079539220771485343) * 10 ^ 70 + 6846316499907818505711032335879722007422835996630720665435211768218542)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_163 : Polynomial.coeff recurrence2Scalar1Exceptional 163 = (60765235449201829503471343918928360970731987321 * 10 ^ 70 + 1855881424972724152020457213944411421461219906369708560315948027432953) * 10 ^ 70 + 5850026039261926820162015764824525240652660735536323542060187880921566

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_164 : Polynomial.coeff recurrence2Scalar1Exceptional 164 = -((232302538929456729094904168585394611044699249270 * 10 ^ 70 + 3835111791908631114433363199402875266015418192968728706886595308244717) * 10 ^ 70 + 3903388840722008663899984310083895366012928934855376386260338812933159)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_165 : Polynomial.coeff recurrence2Scalar1Exceptional 165 = (524560097846631002560886747466337947178317723416 * 10 ^ 70 + 1662542011642419275180484619422188862424825048816017949849236445386796) * 10 ^ 70 + 5400368775558543192480940925879722853364454032212077153983083707141962

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_166 : Polynomial.coeff recurrence2Scalar1Exceptional 166 = -((411113054862486234187350678413584445788083173256 * 10 ^ 70 + 6738627083355937575840342711991059285793184961434889879264873285075835) * 10 ^ 70 + 6093300318202348510494414440520163898572212692402410577706932849257719)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_167 : Polynomial.coeff recurrence2Scalar1Exceptional 167 = -((2440274905399034755401177829585430719891981039159 * 10 ^ 70 + 1968685891896500635504661097059120956911674140224466184893623068703201) * 10 ^ 70 + 2018300150074470202581904520505112085628800225482030145114914676968158)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_168 : Polynomial.coeff recurrence2Scalar1Exceptional 168 = (14128252541798906017909168827729899602183091440392 * 10 ^ 70 + 9264589660079151870238481392792448850861098136821811359003099290762152) * 10 ^ 70 + 6867340663014652673206313210324519601781101051607372865267249037291413

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_169 : Polynomial.coeff recurrence2Scalar1Exceptional 169 = -((43646537734318663521664359271333010028916606045277 * 10 ^ 70 + 5446969974480947542052511596413434337507687310305301639641251302772485) * 10 ^ 70 + 8786827244888702978153280447517588689761207153266532725832911531164989)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_170 : Polynomial.coeff recurrence2Scalar1Exceptional 170 = (85462128722011923795055515677169340568435443293565 * 10 ^ 70 + 1463553802523428513037347560938904584193398055243123886058285726065615) * 10 ^ 70 + 9612760205380924182142452546498457526700876220426882033461364277944857

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_171 : Polynomial.coeff recurrence2Scalar1Exceptional 171 = -((52396539601262986032882608979124387075249151806007 * 10 ^ 70 + 4408424240749554913241093844396437165069405460235839080786250596179897) * 10 ^ 70 + 6103023157120911950003225793182509827804144916918109538708973149933108)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_172 : Polynomial.coeff recurrence2Scalar1Exceptional 172 = -((388735528455905678451671766049943551566135664416726 * 10 ^ 70 + 9673878039858756399265415092591695300123051770445999363969168535926067) * 10 ^ 70 + 2667530249254765728464667174706241276300704975894801401541480588971558)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_173 : Polynomial.coeff recurrence2Scalar1Exceptional 173 = (2066074020014018313020965896822701136554638652195754 * 10 ^ 70 + 36128059932817229233201905997736331253288173598756191195340030970242) * 10 ^ 70 + 3778523418434271472456780529846114545506355889448709398455113713911059

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_174 : Polynomial.coeff recurrence2Scalar1Exceptional 174 = -((6300686424907731311059745419377910500995775344620510 * 10 ^ 70 + 2888526027741214843977591491192775890337588015978177634006443822932726) * 10 ^ 70 + 2647508150183450716533867250117055026135790131539110513098472485417844)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_175 : Polynomial.coeff recurrence2Scalar1Exceptional 175 = (13391260397417300762200149158407295894206925121158693 * 10 ^ 70 + 1387384426434456594970451158324836195709879208321820072639642271095520) * 10 ^ 70 + 6612318854871595394378841104882335579356655216173147263035576738900893

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_176 : Polynomial.coeff recurrence2Scalar1Exceptional 176 = -((16484919904454953966646133319811696194641828867494488 * 10 ^ 70 + 4096021625529075530302369009524979187443978959017197219588706858694221) * 10 ^ 70 + 2799983596495539660643113350631237266299602111999619147927971234489283)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_177 : Polynomial.coeff recurrence2Scalar1Exceptional 177 = -((14459059572463169769406287573692908518038631359258277 * 10 ^ 70 + 4182661979890603381367899649598697070443398786113676260314219536065618) * 10 ^ 70 + 3014213882009504223950979153684816824598281240646256601103150987326817)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_178 : Polynomial.coeff recurrence2Scalar1Exceptional 178 = (162940362733460266667959881406597214460251216519925553 * 10 ^ 70 + 8222053175575947326991977413964435228727459757014339795283475896634026) * 10 ^ 70 + 6593559119019631111818966329647085710966523292663095786488257667121961

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_179 : Polynomial.coeff recurrence2Scalar1Exceptional 179 = -((600498270884159046211164521310943464908249410509016811 * 10 ^ 70 + 7210431334963577055691112658999655955043459732570338928163119590107636) * 10 ^ 70 + 8979759078612543025261000798854300816021160042539772903487732442295154)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_180 : Polynomial.coeff recurrence2Scalar1Exceptional 180 = (1567503134919388911604580591781482624318952194844059145 * 10 ^ 70 + 7014543504205812569064413211239963893006310007184017327327192227018096) * 10 ^ 70 + 4393638285929470022486792018149216781674931116226060264139652778010268

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_181 : Polynomial.coeff recurrence2Scalar1Exceptional 181 = -((3130079875206175820423179602892716714512991694242285079 * 10 ^ 70 + 8309352171344525860996914647063953790007607092990142053890801560128005) * 10 ^ 70 + 5632850909198255187335883495370200575254981329608103228304191381316911)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_182 : Polynomial.coeff recurrence2Scalar1Exceptional 182 = (4346259161110567277366709303533693509604965153608196194 * 10 ^ 70 + 5873529692185282525909638099899629280490422618878630766957366692616637) * 10 ^ 70 + 1961306233879523185343584348673178886033437909443109889484811878146555

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_183 : Polynomial.coeff recurrence2Scalar1Exceptional 183 = -((1232682173270152121467490137382239827170275015652713687 * 10 ^ 70 + 3277755552408072520410826900799080536767136885003114449850053290748886) * 10 ^ 70 + 8220347481118288211529946162696689538412094098502434759704269693669098)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_184 : Polynomial.coeff recurrence2Scalar1Exceptional 184 = -((17164010980585707010735475746140251832582104036179179699 * 10 ^ 70 + 818789708044215091985058256399454560165966683942531252427069508936927) * 10 ^ 70 + 1080021580963576838820829305769223317432500925974400662725327318906057)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_185 : Polynomial.coeff recurrence2Scalar1Exceptional 185 = (74731973409860346806276890768076565246228176937353039603 * 10 ^ 70 + 4048744152870231544707507840511717865207618705406541144240083096867255) * 10 ^ 70 + 2581708878434630835440982170419326550922636301118884533587382722209089

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_186 : Polynomial.coeff recurrence2Scalar1Exceptional 186 = -((214389207315670277651953702844684846671380844213582869046 * 10 ^ 70 + 3844565397791723437119947582293503216783986770792095653259907789770005) * 10 ^ 70 + 1289268392416191577556728909058283639337346861975260835526997107124358)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_187 : Polynomial.coeff recurrence2Scalar1Exceptional 187 = (497818158347562685935783052113341183870103372727164640731 * 10 ^ 70 + 2991039346028896152159468542738627583390605235814758657967865060330761) * 10 ^ 70 + 3010167723861673776946379043940454319424714365617802970558745380196749

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_188 : Polynomial.coeff recurrence2Scalar1Exceptional 188 = -((984652274463959948638011880348555937491602528831791986905 * 10 ^ 70 + 9056292774040738825373069592326694009945858691100360306544436780246524) * 10 ^ 70 + 1924379627931507979121685904561144233106586931047506921461020898001356)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_189 : Polynomial.coeff recurrence2Scalar1Exceptional 189 = (1667397799975155962988516202127315072960514810752620734123 * 10 ^ 70 + 833989264828153585761856682317460772960894560443705275440812394972030) * 10 ^ 70 + 3210310949249430317482653718151492910252093227449265694970921446092769

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_190 : Polynomial.coeff recurrence2Scalar1Exceptional 190 = -((2332102877967218207092811913787667125052931929792414137062 * 10 ^ 70 + 7761616002786021961788909560628169190704967123563180480812129387835198) * 10 ^ 70 + 1063132003239087788771138568922820799504493907229005716279909929128601)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_191 : Polynomial.coeff recurrence2Scalar1Exceptional 191 = (2322338654350627458024877477233749821405489024164197774831 * 10 ^ 70 + 7264991085135147383893062279632308308465883584085191580945122572137052) * 10 ^ 70 + 4290067888820881032409551863141704833837790159263082575689621969038107

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_192 : Polynomial.coeff recurrence2Scalar1Exceptional 192 = -((221015495369977258910400348240388566268011737627150431743 * 10 ^ 70 + 308333704246272028738170403104009098144377227104272451178390308334601) * 10 ^ 70 + 5378506718413726034558653092512144219259984503523884968607639910362511)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_193 : Polynomial.coeff recurrence2Scalar1Exceptional 193 = -((6453537939647292817962293385399665872604388115153347210780 * 10 ^ 70 + 2821676952328078965223124603428167889289009028607009418211886063189174) * 10 ^ 70 + 7204196656701256128520476927732012928230553163579994479075818309598896)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_194 : Polynomial.coeff recurrence2Scalar1Exceptional 194 = (21309934028706673876531272425461244117437999773846096302448 * 10 ^ 70 + 7379710631795520854550008619761471575040024561142843486693888075771574) * 10 ^ 70 + 163929942117505749034885652409420257046615627732008302309085817577957

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_195 : Polynomial.coeff recurrence2Scalar1Exceptional 195 = -((48521693639861941567431046895235252429962387878426575541230 * 10 ^ 70 + 1458109535521091024888128471998828092557788586981285897901114315454634) * 10 ^ 70 + 1442234633305925308096058983433457502502569061679902582192874799918630)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_196 : Polynomial.coeff recurrence2Scalar1Exceptional 196 = (91146159974294568084419079607255887470010415599843795546523 * 10 ^ 70 + 5179286494491226080652315438150787719249739718075687990976826988139529) * 10 ^ 70 + 8314455145827236779195985447438413305545087907975628514028753751680612

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_197 : Polynomial.coeff recurrence2Scalar1Exceptional 197 = -((147876256809909355505702752155572655170663440057668980350416 * 10 ^ 70 + 2790483059592182363980898251274857964998202566370875839767963325721044) * 10 ^ 70 + 7163004645580808818944544241383298436146167801030202490631805007711075)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_198 : Polynomial.coeff recurrence2Scalar1Exceptional 198 = (208116783543060476053355194885060799512194982624097836975164 * 10 ^ 70 + 4258953016587974423125360684926553974167965449655549415026477378103405) * 10 ^ 70 + 997450759362801768484147133132870718859089209810791821635377626147108

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_199 : Polynomial.coeff recurrence2Scalar1Exceptional 199 = -((246001228971245570792696359956549530178169531375654006268773 * 10 ^ 70 + 9200301625700752149402720337861165482544299109325270790100762620945647) * 10 ^ 70 + 4880803991421966094877304553833064676273823255222950400451335522432248)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_200 : Polynomial.coeff recurrence2Scalar1Exceptional 200 = (215028808671236522828627799428383638248553320035527900657917 * 10 ^ 70 + 5060231533237708204823981052557646844661313165412236646375898579252464) * 10 ^ 70 + 7107499850110152133052671927221310859051197274012226421735156915814787

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_201 : Polynomial.coeff recurrence2Scalar1Exceptional 201 = -((46136525189497440841362388451087210893841382916330292342016 * 10 ^ 70 + 4970020257479637300151733497884728050207420740450099787846680215075217) * 10 ^ 70 + 2287926349075773087090433090481417500003293160615280344146746569423717)