Recurrence 2 lookup certificate: Scalar2Exceptional 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.recurrence2Scalar2Exceptional_coeff_154 : Polynomial.coeff recurrence2Scalar2Exceptional 154 = -((2806106664720910916218573612931445933552730 * 10 ^ 70 + 9951770845429668862005332476493156456208846827867805214503443667233417) * 10 ^ 70 + 5788654661659946599894177361624008103519980404843380060978510128451241)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_155 : Polynomial.coeff recurrence2Scalar2Exceptional 155 = (8494463541847381427699963847373453318369544 * 10 ^ 70 + 3574422153281724600882358708550214212508811019998121719604612093557309) * 10 ^ 70 + 266526787711996938740605972031409532129940022243843651149284012887521

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_156 : Polynomial.coeff recurrence2Scalar2Exceptional 156 = -((10358226362487700932629561616055067537061140 * 10 ^ 70 + 467491215929216627516517765572534712181200816856547886393697705513433) * 10 ^ 70 + 1841764327370541377883802534509925390220554384551183228594684690331932)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_157 : Polynomial.coeff recurrence2Scalar2Exceptional 157 = -((36847099803284823176190650879017532672522407 * 10 ^ 70 + 7264886056548739976684079804088365551312437420738834940141269189207405) * 10 ^ 70 + 1988078637537304796578798215088655682199318107945744224390136372926679)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_158 : Polynomial.coeff recurrence2Scalar2Exceptional 158 = (267206168979592724286476842296412264314669692 * 10 ^ 70 + 9343490234948660071683512683327027494304982915524920230810137601498277) * 10 ^ 70 + 2047371840162044737650647617622074509379954825085804040520729247148785

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_159 : Polynomial.coeff recurrence2Scalar2Exceptional 159 = -((859909111976558101190773731361374195656559722 * 10 ^ 70 + 2149600722437866913237843230877467994882166690267372294057743144406129) * 10 ^ 70 + 2640398477095938081070344165718615179189406667516879143383774545113533)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_160 : Polynomial.coeff recurrence2Scalar2Exceptional 160 = (1405334530626904092560044014551178384781808488 * 10 ^ 70 + 3664539236798283775692698709338583801363388072918154578956683904660576) * 10 ^ 70 + 1294466662158104864726938657816534294536421326777065939686303512695090

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_161 : Polynomial.coeff recurrence2Scalar2Exceptional 161 = (1468935481293801469631628947300158805560168999 * 10 ^ 70 + 5578221944466781528092741143382183541895559810900471880872246313759057) * 10 ^ 70 + 1489532549531054925644443345409785726596277267614298865045874237626090

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_162 : Polynomial.coeff recurrence2Scalar2Exceptional 162 = -((19065660531482495617419720482499894069690296267 * 10 ^ 70 + 4047924686905656962950401690431062739863944725885018328142727368043380) * 10 ^ 70 + 9322179849734671908922345677462699980119978780239197800245185079440772)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_163 : Polynomial.coeff recurrence2Scalar2Exceptional 163 = (72673609965197557722690412246050360795477439495 * 10 ^ 70 + 5437093233694659080800509460450005652877642604385745942298801777572037) * 10 ^ 70 + 5168951212510616551139779630123267890554028484801726759046252877342218

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_164 : Polynomial.coeff recurrence2Scalar2Exceptional 164 = -((162917582413117146620629873941783756075776080374 * 10 ^ 70 + 9667677242325812504135322185560252281827659979659321355991421148237070) * 10 ^ 70 + 3727417343600281104176967684089665734425351709534352574068406069177320)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_165 : Polynomial.coeff recurrence2Scalar2Exceptional 165 = (122848457361898237853956035440242404635403753168 * 10 ^ 70 + 8767316111758211110644741408722726141362762992055715716272104240727694) * 10 ^ 70 + 8465385566104980999860751088508853660056415928511636974069487289600666

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_166 : Polynomial.coeff recurrence2Scalar2Exceptional 166 = (775787084000018423219421105495561519546236738318 * 10 ^ 70 + 3315255028180367330763816552898478123518988501763488459180659428409544) * 10 ^ 70 + 9838177333512940689935611335802911777479317862184453822693323819735658

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_167 : Polynomial.coeff recurrence2Scalar2Exceptional 167 = -((4409777048803738797528720692876116032297604732040 * 10 ^ 70 + 4611548640707129886485006552033560133882290900684738970985914965145168) * 10 ^ 70 + 7540139313098958782959235587105697805301174117082385856940826592456383)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_168 : Polynomial.coeff recurrence2Scalar2Exceptional 168 = (13459638057736743378739227455226485037677087392145 * 10 ^ 70 + 881465127104521736374695996830471649759416310316331572150269712304829) * 10 ^ 70 + 4159445195917940568667474053438389191513739349122559085567705102360988

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_169 : Polynomial.coeff recurrence2Scalar2Exceptional 169 = -((25867546046202948336766516313092198110067897154894 * 10 ^ 70 + 5030379440372964457385003962408171949970853059638386022435068910471381) * 10 ^ 70 + 7522275070669751934019301966011154832268617577783545535518924871795170)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_170 : Polynomial.coeff recurrence2Scalar2Exceptional 170 = (14043765571352396042957798769093049392058853096163 * 10 ^ 70 + 5431085282315048255805087287936390616735309352722335168017690246837700) * 10 ^ 70 + 3303258010661954480327168012102040589042500614079599248531427286314633

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_171 : Polynomial.coeff recurrence2Scalar2Exceptional 171 = (124897965427327875681567181531068729227916743397681 * 10 ^ 70 + 1163469193393082347358481575928239049096963796561588644657817525421804) * 10 ^ 70 + 5390527365279710773411931430503465777228119862752021063088157928667058

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_172 : Polynomial.coeff recurrence2Scalar2Exceptional 172 = -((641309915210943696034703298392879033601585783873180 * 10 ^ 70 + 7039625976228219614941956375834664697961302333307038647337864018125506) * 10 ^ 70 + 1179596929621460050131162588550698731423205531073568676419426297051541)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_173 : Polynomial.coeff recurrence2Scalar2Exceptional 173 = (1919730143035505014390488197515819590386034985428885 * 10 ^ 70 + 7642754240455774127182877029168450175310776084251267335897542496340104) * 10 ^ 70 + 5535991765497592285814062797104548468226652866426118406018159395946501

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_174 : Polynomial.coeff recurrence2Scalar2Exceptional 174 = -((3990836665800505202830331647929702386932247825428291 * 10 ^ 70 + 1923952859530167225726289915650646663750322678171639594821243790508117) * 10 ^ 70 + 7212280756597439335892407819381099416462060350180087567747443652112859)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_175 : Polynomial.coeff recurrence2Scalar2Exceptional 175 = (4640448034959988699801888895330618959026518713557403 * 10 ^ 70 + 4766133156292236723515589512453767774021405055274020654346397239155809) * 10 ^ 70 + 2844180115008327033537772361536015781632739188985728079736375466399504

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_176 : Polynomial.coeff recurrence2Scalar2Exceptional 176 = (5403713762442353272164112745304081655389913726822681 * 10 ^ 70 + 2296715839444358008023050696598135370972083297737290916669921614530343) * 10 ^ 70 + 1053257671044162216368720012712903034427096998897667294853438627457279

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_177 : Polynomial.coeff recurrence2Scalar2Exceptional 177 = -((51256622418576347488582553687974357261346642038783837 * 10 ^ 70 + 4638195080551086239225916214234135918302996850483953999730597297016838) * 10 ^ 70 + 4354126889908583425349355447518656360763643352953658020494688563606788)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_178 : Polynomial.coeff recurrence2Scalar2Exceptional 178 = (183085875451615757483896402940932735562318283380457494 * 10 ^ 70 + 411861067441412537342842765042896502751063571436325037801869100463235) * 10 ^ 70 + 3962234479552047377687218768997024508095364048470310514573036660120415

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_179 : Polynomial.coeff recurrence2Scalar2Exceptional 179 = -((467488933816847253204289737021662979448329764867444067 * 10 ^ 70 + 7072980499291041395457843005566138062258976943262578801755370945712246) * 10 ^ 70 + 4606962110092784366822044194014429396373857921583335962320360112861530)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_180 : Polynomial.coeff recurrence2Scalar2Exceptional 180 = (909796249296312642113449875485490207904612086791557687 * 10 ^ 70 + 5293617502201526654631642678640249942988807938495451350384716100379524) * 10 ^ 70 + 3710403344934459510823242726810648153049869885273266153943174814180647

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_181 : Polynomial.coeff recurrence2Scalar2Exceptional 181 = -((1200437603092017196946405584715951663344418019648991063 * 10 ^ 70 + 4555658288372227282746793248676961224377644197434544706835294109107757) * 10 ^ 70 + 7744322275166258135251367815556690449891954204950455504017848412300617)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_182 : Polynomial.coeff recurrence2Scalar2Exceptional 182 = (115469226736888436977221884779348998655225836285278703 * 10 ^ 70 + 5110198882847033619182878716189807859055593520313033096670445820304026) * 10 ^ 70 + 2043115845871004025467325478519383290258409641219749543863102704437848

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_183 : Polynomial.coeff recurrence2Scalar2Exceptional 183 = (5606062701582878010590182406853810276903152072560620115 * 10 ^ 70 + 7461827790878546027458338489099378067847033934786924873550278983950855) * 10 ^ 70 + 9645280977771742070498256734618995149731812266645451825156182072845671

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_184 : Polynomial.coeff recurrence2Scalar2Exceptional 184 = -((22892449640070225957107742052769946262384798187789508132 * 10 ^ 70 + 595253849300626028535227816863694627241571675511208066022597367944408) * 10 ^ 70 + 942039715479264281412661291773982290457876213113084647345702196747804)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_185 : Polynomial.coeff recurrence2Scalar2Exceptional 185 = (63830351223001897544191085660461249654780219249791462513 * 10 ^ 70 + 2647702464172202499359486905248812244016463284287239455257156889323035) * 10 ^ 70 + 778467327150613424142707133078735005730207381930855219935339906889630

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_186 : Polynomial.coeff recurrence2Scalar2Exceptional 186 = -((145029973686066659373453500751799389444635795614923812650 * 10 ^ 70 + 8607253761423384519957187595840835420661046999041973789647714961843722) * 10 ^ 70 + 9487322118294573566868485073880306663745480786413603718547813355107818)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_187 : Polynomial.coeff recurrence2Scalar2Exceptional 187 = (280739443110948497006703150852486653453383674799466748117 * 10 ^ 70 + 4622974353066478462130585202470330273376666057742684003587098357196778) * 10 ^ 70 + 4660812401779796138576841694448278997086019586661785826224127399099527

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_188 : Polynomial.coeff recurrence2Scalar2Exceptional 188 = -((463133393695241615068575381125729030102231934992467634230 * 10 ^ 70 + 5547008678567181454106461261192826256049217492838167191287096469624772) * 10 ^ 70 + 1489183553408548273018059164441515472656655140791505139149345102564199)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_189 : Polynomial.coeff recurrence2Scalar2Exceptional 189 = (622025593035392910853977044446540846383077170232455485407 * 10 ^ 70 + 5702388097005019827298005994476508262294670166644317811107344408150542) * 10 ^ 70 + 4910961460250874455198757992217735894407531687661610601424848994970799

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_190 : Polynomial.coeff recurrence2Scalar2Exceptional 190 = -((559403915146293417568697296170181364626572765389143789957 * 10 ^ 70 + 6971837570148914705500762657728694669308895524664147867576095954717311) * 10 ^ 70 + 7523207249506800867128154520589108282486912030250674580913684863417551)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_191 : Polynomial.coeff recurrence2Scalar2Exceptional 191 = -((134156976365098756220328931103995687017982947643057816683 * 10 ^ 70 + 8658173490077089591982065032759841175285399864856300481930336851192934) * 10 ^ 70 + 1509841073371751496420820069761033834104187587237418272328609455704762)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_192 : Polynomial.coeff recurrence2Scalar2Exceptional 192 = (2150326261839466235638661521320859321618009279093312359806 * 10 ^ 70 + 9166969052015423674228809174833200553499282596792612979807902193017355) * 10 ^ 70 + 5339607769340470754610996307645884978317094557454518100581632272041887

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_193 : Polynomial.coeff recurrence2Scalar2Exceptional 193 = -((6454447781260379121381597295752950300409416617021026675630 * 10 ^ 70 + 6729341494937852902297938334871383551947469630060409876880923443020736) * 10 ^ 70 + 6011973327572287661244731134947602694618613115970126210482452275576185)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_194 : Polynomial.coeff recurrence2Scalar2Exceptional 194 = (14091820939627838510780288291333754822699751381742476613902 * 10 ^ 70 + 6323748890719993890356342124570557388921446384695818650228732019539951) * 10 ^ 70 + 6315405045063832788116740730843479446865346119060931010107815364732048

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_195 : Polynomial.coeff recurrence2Scalar2Exceptional 195 = -((25681165073131094428883946644827236530874225174627831971717 * 10 ^ 70 + 402322980990584324689643265313300067687875219102720807326741089842830) * 10 ^ 70 + 4307991801867619085273201785679766865794059613840715170547969157496325)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_196 : Polynomial.coeff recurrence2Scalar2Exceptional 196 = (40494470487837970186154064619470793232165522875256542871310 * 10 ^ 70 + 2535960322347640425058403644857193462646674577815135017265732858956165) * 10 ^ 70 + 1417719783697822189066759261546947136385179125538660212408205946682567

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_197 : Polynomial.coeff recurrence2Scalar2Exceptional 197 = -((55131683107385546818816300466979013490463661962276824737911 * 10 ^ 70 + 8642837021013706756592391173795947268348192153603103338023633616282228) * 10 ^ 70 + 9130200811113404652461372237567489114483382878391562137281427437196982)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_198 : Polynomial.coeff recurrence2Scalar2Exceptional 198 = (62007113792352502073739761256720181581571345256595210397272 * 10 ^ 70 + 1927177427061221054282404523562430638372724277422501887497432236795991) * 10 ^ 70 + 2715148194523065922043886973305512091507893724077198221141692990589502

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_199 : Polynomial.coeff recurrence2Scalar2Exceptional 199 = -((48147598650427599281768653606961620433109553643891686738918 * 10 ^ 70 + 1265633416505299996666057895979980401236818393361819152587936305006105) * 10 ^ 70 + 4604049910997661579024993597148591640095470785865929209634521183522707)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_200 : Polynomial.coeff recurrence2Scalar2Exceptional 200 = -((4925052715547096221584215347197294949630938974537283612018 * 10 ^ 70 + 2718907704271176789848451392904598805155274774395902501457436041914239) * 10 ^ 70 + 5318495115520932952059985809648163864713291698011330979657209037930202)