Recurrence 4 lookup certificate: Scalar2First 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.recurrence4Scalar2First_coeff_198 :
Polynomial.coeff recurrence4Scalar2First 198 = (((17981800883634325917 * 10 ^ 70 + 5597837219831737644581508983296334184295008773452243104907952456108251) * 10 ^ 70 + 3178407149561320417904694653886577304347087886997404659742078500900972) * 10 ^ 70 + 5045356571734003913173992252506307292394662247439279837375262108552853) * 10 ^ 70 + 6715164874295896769698289554635764218698128662084433092173659711468074
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_199 :
Polynomial.coeff recurrence4Scalar2First 199 = -((((37172458629946459862 * 10 ^ 70 + 3874746709755947164233195566730674376435335321414921907215222139058379) * 10 ^ 70 + 9699053525727588531069174676820844730073885374540263146484886265255699) * 10 ^ 70 + 9370216485702678250542505380179545628002111520374490651642469268481104) * 10 ^ 70 + 5730320196947465600442561396809514614079317487632381302066592040951762)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_200 :
Polynomial.coeff recurrence4Scalar2First 200 = (((75768463674414466377 * 10 ^ 70 + 1177534146027818680017935282648983912952387072823995010469239028200047) * 10 ^ 70 + 313334460873391990874644126272781698087741715417601565140932322835510) * 10 ^ 70 + 6783675141106409097526178914052769010934522513910005985365987566495808) * 10 ^ 70 + 6210370921492968555189147908799439495594837840651363142051126795488218
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_201 :
Polynomial.coeff recurrence4Scalar2First 201 = -((((152279726252937940591 * 10 ^ 70 + 7139258558591258740732161949221464960031158468804670387632582207009758) * 10 ^ 70 + 8176352855993746017069265838371558249414283862206363315566326611581289) * 10 ^ 70 + 4319009448348153225238362910298318812931779544980968413266449813703657) * 10 ^ 70 + 2240075478563194328914282197216884726527771568563367309541930677687196)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_202 :
Polynomial.coeff recurrence4Scalar2First 202 = (((301778842787117668334 * 10 ^ 70 + 6209149473179599613952114836602458901334113952320600239569875181355671) * 10 ^ 70 + 7762917365260796740934869748388027927137699466758423253646565228999036) * 10 ^ 70 + 8056582331066139214069463096764261449839098776784124593883891452945569) * 10 ^ 70 + 3248916124961193115948099421398915620958987670313735787627642465889302
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_203 :
Polynomial.coeff recurrence4Scalar2First 203 = -((((589704745700436225499 * 10 ^ 70 + 8916843706277633828753412748318102020193459180657722322356541711678719) * 10 ^ 70 + 3005214416631780874118136060505856761493144149092810649198068074293650) * 10 ^ 70 + 3746577329802613832084399105211823221000526655268151770924317363232871) * 10 ^ 70 + 3289657423228482511751689136137318708436752043144265441626973510867216)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_204 :
Polynomial.coeff recurrence4Scalar2First 204 = (((1136278966547240786560 * 10 ^ 70 + 5751916421942941370857499635852082764782996059090262373928888941378639) * 10 ^ 70 + 679505686596104281307613179847351543921746591792917262503603569563269) * 10 ^ 70 + 3355320283671240019450592544293179129437403921522183395050347249379337) * 10 ^ 70 + 486100562487008833549940523184745498684499962566937050120110373253007
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_205 :
Polynomial.coeff recurrence4Scalar2First 205 = -((((2158959662621271113350 * 10 ^ 70 + 6550319745176940943565737540365195448306171092884714715454079239235422) * 10 ^ 70 + 342026788912890260291799941745162364135079062985963611136783797808951) * 10 ^ 70 + 8254395944062540018774293027597804444801458654872905133809549402015952) * 10 ^ 70 + 4944696961354604287479733137796955601941153901661746078765029202949790)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_206 :
Polynomial.coeff recurrence4Scalar2First 206 = (((4044988766566391573057 * 10 ^ 70 + 3409754119631711876232308493673772547853916194372924898125039693313920) * 10 ^ 70 + 3382721452037831919355435448299366178876780879750567545070174551930842) * 10 ^ 70 + 533959590994752307940284947891121868933249137112893497779932775980506) * 10 ^ 70 + 3411272102117879728444419673756290441097749711346590967931959380449237
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_207 :
Polynomial.coeff recurrence4Scalar2First 207 = -((((7473200769485924971257 * 10 ^ 70 + 9112942971196124214984095353589889496265841916940384519161112266083349) * 10 ^ 70 + 8135429077399843810439665217744606601037390851169945372621696246877015) * 10 ^ 70 + 2678203610981629460100391002814253167030584661489906514459017664634875) * 10 ^ 70 + 7825096069133829463081147504844729997320701084829033904884727295497722)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_208 :
Polynomial.coeff recurrence4Scalar2First 208 = (((13614920077391491170262 * 10 ^ 70 + 7926170818151656479564573445154108949985488479788244685009415817118067) * 10 ^ 70 + 1711396761041619483857858419776955443731045721400427082779874893582104) * 10 ^ 70 + 4199431651150430714531045706909427829535931471256654084771367230607441) * 10 ^ 70 + 8381384110978199836684267516572680817663116205566561891483247167077303
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_209 :
Polynomial.coeff recurrence4Scalar2First 209 = -((((24459325956868675701067 * 10 ^ 70 + 8707978723596833597132404403808509872231630351605821295470340552376991) * 10 ^ 70 + 3512405702866753071176069386526645784562509048614857823717217755112033) * 10 ^ 70 + 1273571692385627868876477946612903303643946406523796208397729110910468) * 10 ^ 70 + 2450937152427759641558566695520356395728405018910863287933882732614440)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_210 :
Polynomial.coeff recurrence4Scalar2First 210 = (((43330715623304941128575 * 10 ^ 70 + 8174122254909542825262708772626554582706042683564617604236727525963484) * 10 ^ 70 + 8134068746948832225539257299268158273759344087488162703777964783551987) * 10 ^ 70 + 5564860903344986520547954823931492478035528505177484751082526838099252) * 10 ^ 70 + 6348840640779873392171661747316774527780779894497694624314459820664247
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_211 :
Polynomial.coeff recurrence4Scalar2First 211 = -((((75695395926241056621948 * 10 ^ 70 + 4679899215521235573715962238582800704340218294755795081223293952049527) * 10 ^ 70 + 1411534319657067862762664646640060950634141558003328221036714653217699) * 10 ^ 70 + 66359916697198503308450257842462715341313269034252669734434688614486) * 10 ^ 70 + 3310333422722086159950577976318159612698222913484465583984797204484550)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_212 :
Polynomial.coeff recurrence4Scalar2First 212 = (((130396126466926827388243 * 10 ^ 70 + 9033918841559550878415962284800095479272621071544632708244742989620557) * 10 ^ 70 + 9783811100644915709790327749363020569583182507430035292069524746727002) * 10 ^ 70 + 4061559202339075390250359534698402893759050751170605139685559257542738) * 10 ^ 70 + 966113351967678758135884586119181628838177327892583699509103092814719
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_213 :
Polynomial.coeff recurrence4Scalar2First 213 = -((((221503225772764221502861 * 10 ^ 70 + 4672086535330222425780579537320533093942921668272815081861120304851049) * 10 ^ 70 + 9235516925811839819736809854083483124937402802939446117777186342031017) * 10 ^ 70 + 6473052591345935328836085498854910760436208871902111403872544109330251) * 10 ^ 70 + 7793582146416987416733774718406899653971253847898313546286937773406944)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_214 :
Polynomial.coeff recurrence4Scalar2First 214 = (((371033527751041197518677 * 10 ^ 70 + 5322596729602391977620289232941704585637035649241998523434743092147527) * 10 ^ 70 + 7526414200195868821285190147408560760463765517006675950794377041268308) * 10 ^ 70 + 7301179560178224868548770335222677189144738976980275840893944029576034) * 10 ^ 70 + 426731706917512996073141121742660214768939278226636275302934205523430
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_215 :
Polynomial.coeff recurrence4Scalar2First 215 = -((((612859073946950802176481 * 10 ^ 70 + 4017405209681113248505824826173442890502434621952856014173066231733405) * 10 ^ 70 + 3282070556980793734827084147135515075048592910710851376973754690616511) * 10 ^ 70 + 9500613753535340544975985523999642238202275437354097942987691257434014) * 10 ^ 70 + 665977210641141831077897001677826992645008006066671294363915529342293)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_216 :
Polynomial.coeff recurrence4Scalar2First 216 = (((998201137153705229323591 * 10 ^ 70 + 6367016644669083499933647766354656571423963089581645315865053289303566) * 10 ^ 70 + 6224308716601301528707314082896239309559187798863941372445188030461894) * 10 ^ 70 + 8474009816277827455239212670725806740729342368598095202094201445064435) * 10 ^ 70 + 6782277976214501957729717363813002319061215731201529992092204378497627
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_217 :
Polynomial.coeff recurrence4Scalar2First 217 = -((((1603171585948136767583266 * 10 ^ 70 + 9870158947676006095304655808151779270130305072652034942920599637991994) * 10 ^ 70 + 9527742153403666848690831091146481309587800844679505312585998945616546) * 10 ^ 70 + 2078736951407937061669014372205731611897555364027942971118802230631498) * 10 ^ 70 + 7699755695344374002783249718050010777316645717611447503229116248484267)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_218 :
Polynomial.coeff recurrence4Scalar2First 218 = (((2538866411499086330260692 * 10 ^ 70 + 6694778556095126737110273065382522472738828416742817512746659599816606) * 10 ^ 70 + 8757002389505999325176545099362174413845927333245199152825986867549513) * 10 ^ 70 + 4104387554121144153952237969957601211793851419440057075985618978736880) * 10 ^ 70 + 3681831809183666509568932628399917503055134556012072217093285705227150
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_219 :
Polynomial.coeff recurrence4Scalar2First 219 = -((((3964512233143580857074480 * 10 ^ 70 + 5689306122604809189653582538364754240481163213565079970494222601257835) * 10 ^ 70 + 6982148174830836269110226461983446642636360295724653399121162902233618) * 10 ^ 70 + 13650568289338999291784982898381602106880280971860771854382441458101) * 10 ^ 70 + 9563266133788526737864321396672264476748196496546520598951930210284800)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_220 :
Polynomial.coeff recurrence4Scalar2First 220 = (((6104085627669237854129247 * 10 ^ 70 + 2429996712571950999301238569036991821369067925604701442642812784914646) * 10 ^ 70 + 5302986894978785549720015668612649928781607647745859284919404597160270) * 10 ^ 70 + 4285620390705116888699075505383018256905908390897985780465446435251377) * 10 ^ 70 + 3486398509300654129883147737071726918217766540231984299401469675753022
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_221 :
Polynomial.coeff recurrence4Scalar2First 221 = -((((9266631563220101755744247 * 10 ^ 70 + 3390932299398648263878200613877670546572172165262444190833603621860490) * 10 ^ 70 + 2911666505344401393044291469934627160510265129749472795531842536016266) * 10 ^ 70 + 2504240393620584272770549685043661775961843444793441502195848245160156) * 10 ^ 70 + 4863930629307816507156689059281342422405841756884014147904427971226558)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_222 :
Polynomial.coeff recurrence4Scalar2First 222 = (((13870163546674461713521455 * 10 ^ 70 + 1639151535790779271802110704419698528445558826952052275853956441943642) * 10 ^ 70 + 309653722925783480386785676503252838173322751697268177720297959099019) * 10 ^ 70 + 1057658916143710246719612470044199350191191787459475392624789014652827) * 10 ^ 70 + 5526921089756000719889770377193701570171495688218026323140425272487242
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_223 :
Polynomial.coeff recurrence4Scalar2First 223 = -((((20468501142502867527110461 * 10 ^ 70 + 3814984279308184411288014955187465350116572044767631306244556308749138) * 10 ^ 70 + 186165951897968798447672823696173237533066601370178836532723892774952) * 10 ^ 70 + 1544119750448488559372497831737684588604106058324867209396625930557996) * 10 ^ 70 + 8499238239141576819397283133866445711911899407092094528076466909098735)