Recurrence 4 lookup certificate: Scalar1Exceptional 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.recurrence4Scalar1Exceptional_coeff_183 :
Polynomial.coeff recurrence4Scalar1Exceptional 183 = -((((450418022346 * 10 ^ 70 + 8082303849485945550754107761165667315715292618747083419576596986510706) * 10 ^ 70 + 339439772445674946519258937955373051286340806526736719115497666285216) * 10 ^ 70 + 52208819047618032839916223004039086199878282494256132332390564718195) * 10 ^ 70 + 3858272122371808459426235052594919747754312498113137517813282754885483)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_184 :
Polynomial.coeff recurrence4Scalar1Exceptional 184 = (((1264892717438 * 10 ^ 70 + 5469675591598438564061010005035547145964281111700787327074347718225880) * 10 ^ 70 + 4323324002961695002248148733496051957239071843483836995050952299715217) * 10 ^ 70 + 1043072030412557359621965315931367764995552110124048003288082117073690) * 10 ^ 70 + 6816242171706640245741079993374321803994399170088679249814439331742231
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_185 :
Polynomial.coeff recurrence4Scalar1Exceptional 185 = -((((3495883087480 * 10 ^ 70 + 8569555973244083285638433747282797679979705481796118625115978055199776) * 10 ^ 70 + 5401183156178840929813459261934498266310082017015107774938196410760865) * 10 ^ 70 + 8311726362776462310557877284691787537989775036661112338590868794806001) * 10 ^ 70 + 9183528333971176357684994711794909148137710337509638461968682174297931)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_186 :
Polynomial.coeff recurrence4Scalar1Exceptional 186 = (((9509938186458 * 10 ^ 70 + 1927770385667517458701791415684749965145609027658224332761613172890782) * 10 ^ 70 + 1529592827845433355403504416314249860673263471397831075747205637365408) * 10 ^ 70 + 4354666120628526546394203873587426797321184623135824133864237910965262) * 10 ^ 70 + 4952424548145844422126945640110218168177093969445868728988285342725592
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_187 :
Polynomial.coeff recurrence4Scalar1Exceptional 187 = -((((25466305768267 * 10 ^ 70 + 9667783562344898895868124458079572866797019681653268525070591507796145) * 10 ^ 70 + 5400128544300889429863259580508965138485019983585077081468598393508559) * 10 ^ 70 + 1651461294220336227479371143884318660236639752955237216086144806040148) * 10 ^ 70 + 21166976929955088728393550075446929217843717265779625870960885260425)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_188 :
Polynomial.coeff recurrence4Scalar1Exceptional 188 = (((67138137230604 * 10 ^ 70 + 5468645872041613536001757446614023961678703195935075954515888608841166) * 10 ^ 70 + 9820797927217924383428569674549387760578008434399964455764659463113311) * 10 ^ 70 + 2280726234785589680111000423446821016202069668227698365513813432312075) * 10 ^ 70 + 3264069759437462225718023350827233882737070054226584032829932044798872
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_189 :
Polynomial.coeff recurrence4Scalar1Exceptional 189 = -((((174274256779095 * 10 ^ 70 + 4246596764701138958515543337838632269096547729353548046064994802034981) * 10 ^ 70 + 2259377417957881297317392407197594710587262314832536083597840887880741) * 10 ^ 70 + 8034338046479086814810695073106095328417789245058881709392194932186302) * 10 ^ 70 + 2756822870442732711393892852280158899795467837706082893166908732030625)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_190 :
Polynomial.coeff recurrence4Scalar1Exceptional 190 = (((445452488562642 * 10 ^ 70 + 5183848462733386335999570134496983649701032689402720300943813556765131) * 10 ^ 70 + 8164205680061930524923755407370561593679637003539688731298206446700531) * 10 ^ 70 + 2224426483532633206207385171981577083914390373427742375777489648968798) * 10 ^ 70 + 7202329494542158767191777735305041292149658018356253082033139125919820
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_191 :
Polynomial.coeff recurrence4Scalar1Exceptional 191 = -((((1121283695312016 * 10 ^ 70 + 2327076605124482169761132701323779388448146841153916793782680577147628) * 10 ^ 70 + 2683991509448513955328447966656709678094151443651606358261285091077636) * 10 ^ 70 + 7254118470735422692533544164950043539841596561068844679572948383273910) * 10 ^ 70 + 4969248723466527482805147666902527529486244695590837288814816275433986)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_192 :
Polynomial.coeff recurrence4Scalar1Exceptional 192 = (((2779813518424250 * 10 ^ 70 + 7148137826801893371149906442589752204957387222577817285663184039605329) * 10 ^ 70 + 8439566380423620106920482625768542575414641781436975942698224238499253) * 10 ^ 70 + 2530702931025315547399892132284379199918401177221551418872771203854246) * 10 ^ 70 + 3178898361227638393103089272610055144853019862718542048242628283665033
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_193 :
Polynomial.coeff recurrence4Scalar1Exceptional 193 = -((((6787976560522579 * 10 ^ 70 + 1553214965086813833066115642359194621596723354563502467411536077342588) * 10 ^ 70 + 7267697550522336807211767024828110456245908036604466395434201805392387) * 10 ^ 70 + 9347581922321443345826930106384788858819047024558600734767884809593049) * 10 ^ 70 + 1539702288527895903434989918185723726531222815039640911355568998335547)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_194 :
Polynomial.coeff recurrence4Scalar1Exceptional 194 = (((16327756023804062 * 10 ^ 70 + 8370579136336663780738695884282135195177789972126557878496499391393202) * 10 ^ 70 + 4225777452988758926037183998355506661771022604000511513592322397382100) * 10 ^ 70 + 187220403566126524645515733691461485351846523157427977211657507425253) * 10 ^ 70 + 1295389649568266822934965461514998830303978028704855217615597227637735
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_195 :
Polynomial.coeff recurrence4Scalar1Exceptional 195 = -((((38690980772806841 * 10 ^ 70 + 9990698911030130224227822980462321421967646416922933526390130600936019) * 10 ^ 70 + 9841712315638134946841336451436212747189253562393997764540491855419188) * 10 ^ 70 + 4111791493636067065763779491023156350393028708559917132855712555095165) * 10 ^ 70 + 1536658039902948795157961915524920107780873412841683677287068950682787)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_196 :
Polynomial.coeff recurrence4Scalar1Exceptional 196 = (((90328392860429250 * 10 ^ 70 + 7649808417870296064420697919681902145290123949894837022524007998409219) * 10 ^ 70 + 5731284112073627086857834207843832505341418172129630735330259097056320) * 10 ^ 70 + 7158487789557352713695537390743866350584389651048610057500845446664815) * 10 ^ 70 + 3619182845639203192849045447113379052315846450542715736850484038917990
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_197 :
Polynomial.coeff recurrence4Scalar1Exceptional 197 = -((((207779701020449656 * 10 ^ 70 + 7017713482120872903191334382341256709972440528541472760190439776152345) * 10 ^ 70 + 5061517972250609699582851600484220404265104191247922583543170474604959) * 10 ^ 70 + 3081558255856669312598755998393083867380107725220412237610410341543059) * 10 ^ 70 + 3719879993197611370415958672857339554065960803859079028161845052289870)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_198 :
Polynomial.coeff recurrence4Scalar1Exceptional 198 = (((470953499115382570 * 10 ^ 70 + 7728231198694697200833296064742393647764463382959230101080398110549002) * 10 ^ 70 + 3300874817768007778478345815743028164940383068126226104363096081903791) * 10 ^ 70 + 828923448986297900673683360570033414545666884475258113863737546703828) * 10 ^ 70 + 5117010405486565496808875998654370359793328002217265128640894979706074
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_199 :
Polynomial.coeff recurrence4Scalar1Exceptional 199 = -((((1051912633987965812 * 10 ^ 70 + 3475139372643520259786163593396137862837482694252641580684321242478904) * 10 ^ 70 + 5284593898697652061880612957910596097664620326125393412996136737364036) * 10 ^ 70 + 7545121453431183722048134541339726399165758620983847329002528969685931) * 10 ^ 70 + 6414142608704039336001891940415313999640210799257494882042005687712507)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_200 :
Polynomial.coeff recurrence4Scalar1Exceptional 200 = (((2315461819659547640 * 10 ^ 70 + 2203993738586398359466918840703099020901224898157692856509061561862264) * 10 ^ 70 + 6826077620836301535913624016110124737921696056632151804444587326027622) * 10 ^ 70 + 6003459507255056656694692484348716481432929717658468948058749194495120) * 10 ^ 70 + 7859526622310443484711408307593037080284019032547695812854848286780034
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_201 :
Polynomial.coeff recurrence4Scalar1Exceptional 201 = -((((5023199623102878113 * 10 ^ 70 + 5317641575023789970755595123897737856793539918001255211671152135065921) * 10 ^ 70 + 2686379367014216145491503391401759899966112345761255325296638422648898) * 10 ^ 70 + 7622272115602396517000043727096718673028192296040057837076212920623608) * 10 ^ 70 + 5914365622814251147431110304393136947140245406841886966188260459970877)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_202 :
Polynomial.coeff recurrence4Scalar1Exceptional 202 = (((10740776551994997096 * 10 ^ 70 + 1284113598763881997519443868117628784679081933377358046827917435563127) * 10 ^ 70 + 1832001042397767553407153303500259558569606863303237457870381351382881) * 10 ^ 70 + 1237330839351269353301450257384875897259897925752775667353443776734271) * 10 ^ 70 + 3094643357178269887166287564970926404359631258970059173231503954254552
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_203 :
Polynomial.coeff recurrence4Scalar1Exceptional 203 = -((((22637579622777536778 * 10 ^ 70 + 8152791752679591116467220867574985342241299548741985493021637612802462) * 10 ^ 70 + 9714697333435905576930018484420376631760544358166728449682305754117944) * 10 ^ 70 + 5220189406462048072810240818372000533157846246895019280728568720601409) * 10 ^ 70 + 8803668187418924788271963245919281000225370596304453877002590595261297)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_204 :
Polynomial.coeff recurrence4Scalar1Exceptional 204 = (((47031529419747877083 * 10 ^ 70 + 978497111602233218521161115404719492326961374706693844566913154049341) * 10 ^ 70 + 7604930184355855905136465036252403419881295861525877603913148096555960) * 10 ^ 70 + 4651787651942990937332404335420097007312947240558517134477976045819684) * 10 ^ 70 + 8672509946767454535633176234223263026691764376781853831220444725599582