Recurrence 2 lookup certificate: Scalar1Shift 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.recurrence2Scalar1Shift_coeff_196 : Polynomial.coeff recurrence2Scalar1Shift 196 = (109310034217451895953243465362088403914031917398190424032810068 * 10 ^ 70 + 8837531325741924863938712235213348240068542099339432703664961631878610) * 10 ^ 70 + 6069806385697886457116928110907550393815866630382588236099263337581017

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_197 : Polynomial.coeff recurrence2Scalar1Shift 197 = -((348601551614760209354710737546850773224641810430454707712776862 * 10 ^ 70 + 3357009955527402346203027893944767010553650181680082354833409672964331) * 10 ^ 70 + 4574155476839859717054765172012427298107890938537192974261236514253788)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_198 : Polynomial.coeff recurrence2Scalar1Shift 198 = (688454378113464575884155152405352467107781773516423581573057247 * 10 ^ 70 + 9215887800835318492509763279525655743963164795898883036120275615854009) * 10 ^ 70 + 4056895718130356440550627935827003725469040193084704697535612883331676

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_199 : Polynomial.coeff recurrence2Scalar1Shift 199 = -((598088800617504848897726500908842486608390784325046616023673968 * 10 ^ 70 + 5837080369836226243386819217741177614751332311279602974401657192364814) * 10 ^ 70 + 3403238947797974884689890198243377267599010894940061520837836727805949)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_200 : Polynomial.coeff recurrence2Scalar1Shift 200 = -((1685112187379745567148729456764180314443613377206683579815046883 * 10 ^ 70 + 7534270169266898579095595347306056863594567845439759371750428094408128) * 10 ^ 70 + 864440884754584737835092693598589003696973938910899163272540402357940)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_201 : Polynomial.coeff recurrence2Scalar1Shift 201 = (9912082417426194538909488161353213715518100585401878896014192659 * 10 ^ 70 + 7362554105717443862729821020544570497329764325682402657147555881159365) * 10 ^ 70 + 452050896927877277796214593732138208693447923910512928997619069803796

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_202 : Polynomial.coeff recurrence2Scalar1Shift 202 = -((28857461867257253956537922565048525752470034853326335410783785367 * 10 ^ 70 + 9917256180462377078762604663747849512271479829181897531530194424456123) * 10 ^ 70 + 7794422719031466897411659443018184586586236112728936010980210185393011)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_203 : Polynomial.coeff recurrence2Scalar1Shift 203 = (57114957268739537572816815957172804020336058774608849876118687405 * 10 ^ 70 + 3206279089303374189552135355145461643805835826536839945957651611959253) * 10 ^ 70 + 9376005158520209643049526174794158160102789257826042335912383631624446

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_204 : Polynomial.coeff recurrence2Scalar1Shift 204 = -((65573722861799217713957366881611132043991025320062496984922198318 * 10 ^ 70 + 3901030134909939105893350775476485872205933593378565839241272444665629) * 10 ^ 70 + 843025177263450078965258031899422769309531398996272836219022439477435)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_205 : Polynomial.coeff recurrence2Scalar1Shift 205 = -((46966331916749797093682706291302132953210841179784372961418229801 * 10 ^ 70 + 407492990189366885610605441717395224203389051790184594642068489300744) * 10 ^ 70 + 9449023329044006334635201165985558317493455918495323460855742237846995)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_206 : Polynomial.coeff recurrence2Scalar1Shift 206 = (516666272439456061738418862697662913636950552503648061267023061077 * 10 ^ 70 + 869916353133907351068278448993301857131475729975539471687168879443410) * 10 ^ 70 + 2262742442230194851833041967081666536675868461751389464464064859062525

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_207 : Polynomial.coeff recurrence2Scalar1Shift 207 = -((1746263144302360832637855678368976451151653501286500115173960085758 * 10 ^ 70 + 2385709703630428487478730431285820894448142713404650425960089462653306) * 10 ^ 70 + 5547362391617976220826370635791369167623118848240857263418689748334813)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_208 : Polynomial.coeff recurrence2Scalar1Shift 208 = (4152803985897118126592084493388014190937023099519635189030767251660 * 10 ^ 70 + 8200873715088379304589176964817429851248317583205233308215117493267845) * 10 ^ 70 + 3082847109804544658315043137296966235033149579672508734489571989234048

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_209 : Polynomial.coeff recurrence2Scalar1Shift 209 = -((7502508301286458791843966701334695901829939709830472578074047876822 * 10 ^ 70 + 1679074993016199240020528256097665984066883480166476723354693176901661) * 10 ^ 70 + 472760668310530869528807163553285458188806398958267884500730038924338)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_210 : Polynomial.coeff recurrence2Scalar1Shift 210 = (9181227303517182236331247786959388267427711939007983555103182737401 * 10 ^ 70 + 1285894082033339338466943282588482075315111347408869639041805386118440) * 10 ^ 70 + 3944482090748556099520231658604351377352915796645593654675887962149980

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_211 : Polynomial.coeff recurrence2Scalar1Shift 211 = -((703819663533889639969891576660150048038702796175830082225763264421 * 10 ^ 70 + 3382446313235478561658838017214301223704941232549105277350051982633818) * 10 ^ 70 + 2610743511970584577862444656982780454296442309133034777022679691366429)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_212 : Polynomial.coeff recurrence2Scalar1Shift 212 = -((38028523091129704734211138474046345366048381000895050769596011997426 * 10 ^ 70 + 5488322719731911250210648514421214935173367935930884435440072997204777) * 10 ^ 70 + 3458617310986386678905612200311124644342150842475322498608140731685009)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_213 : Polynomial.coeff recurrence2Scalar1Shift 213 = (146224040271168691494075383853284418935442445586469277176676516945038 * 10 ^ 70 + 2656965274576546493659835721921216573058027798623646640842281776920282) * 10 ^ 70 + 4731808643026760400786019470274710862166059895319826073013379534108360

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_214 : Polynomial.coeff recurrence2Scalar1Shift 214 = -((388683459798017568098236258917101831290639772895804498363054902462622 * 10 ^ 70 + 2186156054513959713920358604213115441396112227583918355276376329539004) * 10 ^ 70 + 4038764815424823073779803810391455947842486751472632339161885825168507)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_215 : Polynomial.coeff recurrence2Scalar1Shift 215 = (854681737544603260538946339158594826224733881279674816913673079032908 * 10 ^ 70 + 7334379813113919430004758187342414506028083734933857560675346143956856) * 10 ^ 70 + 4909908507765657969189687319829001242844639798419955589340099427218942

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_216 : Polynomial.coeff recurrence2Scalar1Shift 216 = -((1637662985067158951550185620904255133890780207889948055935646183952436 * 10 ^ 70 + 2229528093467572762803559085576965781688282029282942042969313141619779) * 10 ^ 70 + 8720298174162866693462890140141287339546863907093874571042864106981732)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_217 : Polynomial.coeff recurrence2Scalar1Shift 217 = (2779532905202633315337614569590348013569661181554221947439187172760368 * 10 ^ 70 + 1076882642250053057326866617595999562725291917785607302128637189879932) * 10 ^ 70 + 5925242705310107948020427635217162013099181095887765528786896707454826

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_218 : Polynomial.coeff recurrence2Scalar1Shift 218 = -((4162031687384066921628405456324263484289185531770486438948452103635509 * 10 ^ 70 + 2204060622448003857504245235454193304523839831770858381245043382790882) * 10 ^ 70 + 5183373181011776426791279491493356503414245839784653866137062303901641)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_219 : Polynomial.coeff recurrence2Scalar1Shift 219 = (5333712307931112269683202737361717299034586397903918686976322995269733 * 10 ^ 70 + 9225963174534502820014538307831629024207202214075077322688022112522184) * 10 ^ 70 + 5166081283415289252668331387727507652045611325249117406014187782058934

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_220 : Polynomial.coeff recurrence2Scalar1Shift 220 = -((5278171641336104773487019753934803408593847186668110297782237803374945 * 10 ^ 70 + 8092922429301536156825356600656651053171195951876133601510573681751619) * 10 ^ 70 + 5546391354661949959266149546534161614545472977845988979264619742841555)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_221 : Polynomial.coeff recurrence2Scalar1Shift 221 = (2158568845801317503165898230307271675474794742644200912035618917213872 * 10 ^ 70 + 8151802390456347142673520362324353060298324678825716552217149059081749) * 10 ^ 70 + 3840871250848102576451866056030911445874927442189372644574358088903718

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_222 : Polynomial.coeff recurrence2Scalar1Shift 222 = (6888855195337571396947930486365521132898931981305253284606454497672786 * 10 ^ 70 + 9852444337086443113084878449107053209899206523865839677653027102263978) * 10 ^ 70 + 2566261598404533350449802956949142337306998837216420406374048949683944

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_223 : Polynomial.coeff recurrence2Scalar1Shift 223 = -(((2 * 10 ^ 70 + 5804369158969007176679681159950795013749078646126592810803973113412073) * 10 ^ 70 + 3540524917552257163188042457657072577287785093929018677530138737127348) * 10 ^ 70 + 5311907460176768530158072716066927977549660317938251535639516519428372)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_224 : Polynomial.coeff recurrence2Scalar1Shift 224 = ((5 * 10 ^ 70 + 9373691779196742731823742776932546509200317397345865010608300247506400) * 10 ^ 70 + 1766652524531964847019147309383546495403516745774731271677873039392449) * 10 ^ 70 + 9738563463178531328176293770052141740894940554476670910588645800310849

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_225 : Polynomial.coeff recurrence2Scalar1Shift 225 = -(((11 * 10 ^ 70 + 2614329071507127118604056640817948069631312487002649251956069347133141) * 10 ^ 70 + 6644599272393243036249880019393020976031166676430725646605592002761010) * 10 ^ 70 + 1094646438489309183400011581842944767116274401533929364568014900781)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_226 : Polynomial.coeff recurrence2Scalar1Shift 226 = ((18 * 10 ^ 70 + 9749100844957729406980307232598144424636932853758930047871628837343532) * 10 ^ 70 + 5163096738501377210619945086535998358994003951983346574513555200538911) * 10 ^ 70 + 7217667136219634564404838228426200754909685318749178375133030455204755

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_227 : Polynomial.coeff recurrence2Scalar1Shift 227 = -(((29 * 10 ^ 70 + 2855701498511922381543251619242722764773082363807118078751627727633778) * 10 ^ 70 + 7781585798707203697665630118029159128716612325637455099505823990635074) * 10 ^ 70 + 4543546929688335883179711665969595799216152353490164627608569646555861)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_228 : Polynomial.coeff recurrence2Scalar1Shift 228 = ((42 * 10 ^ 70 + 424117001740409497632790408201772835138026704530444328760652197319845) * 10 ^ 70 + 2926879521232773792745119241627880409032569316371834178070604502893349) * 10 ^ 70 + 1937883455622944825023067178596235372705354903601879039504091871714817

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_229 : Polynomial.coeff recurrence2Scalar1Shift 229 = -(((56 * 10 ^ 70 + 6177679701107528239690697053000390026485002388850135785682680205498589) * 10 ^ 70 + 1507002293116254854352627117135794967351590254991869648962831350725534) * 10 ^ 70 + 290311449403527776006846252090725812555516266397217544554994109080020)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_230 : Polynomial.coeff recurrence2Scalar1Shift 230 = ((71 * 10 ^ 70 + 8566528858394473867793273227416912670060951189206592506640796917151104) * 10 ^ 70 + 3447946079979795366347084173566027376480672231556563046821459026369809) * 10 ^ 70 + 8776012342246927814094201742373707727376933902047673064375429181677879

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_231 : Polynomial.coeff recurrence2Scalar1Shift 231 = -(((86 * 10 ^ 70 + 1281612045528606235770345838544827361145028047759422171207006617678390) * 10 ^ 70 + 6947524328008958452343596177767922574619080775847988681255291986978048) * 10 ^ 70 + 9548707991441217251313487706725193303066471356472914787560149571714562)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_232 : Polynomial.coeff recurrence2Scalar1Shift 232 = ((97 * 10 ^ 70 + 4949948583393093077591424553607827124092946439081400925762878551603438) * 10 ^ 70 + 6919897692360769887421236270783273535901941820029340300928438715509056) * 10 ^ 70 + 4864002599149748112663463194495881760376848243545693259210401617918818

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_233 : Polynomial.coeff recurrence2Scalar1Shift 233 = -(((103 * 10 ^ 70 + 9887395062551281412987670946824809175129853724497895771893673326282568) * 10 ^ 70 + 8501878803766387138914471941968946827196203879108678738370074179296631) * 10 ^ 70 + 1414214509539125408112784758014877100310538980348283447859512036458272)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_234 : Polynomial.coeff recurrence2Scalar1Shift 234 = ((103 * 10 ^ 70 + 9475072519042855632550419061552920960357579657335493459903841576395363) * 10 ^ 70 + 5516632766874966019237472237862191789306948012889554641917110574493190) * 10 ^ 70 + 5333794218300212824592182043859192296974992339934902745440614323510577