Recurrence 2 lookup certificate: Scalar2Shift 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.recurrence2Scalar2Shift_coeff_301 : Polynomial.coeff recurrence2Scalar2Shift 301 = -((308984761107351702072276557666125552507509314238114 * 10 ^ 70 + 4116765914874078873554423309210855917217928884197955090750262315410804) * 10 ^ 70 + 6286924977909789077253883868188357249894585107116947696072410579277033)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_302 : Polynomial.coeff recurrence2Scalar2Shift 302 = (56531109356958453874531121119323598325459748983966 * 10 ^ 70 + 8316472959906479442332476946656867109838124538321817707018742359918171) * 10 ^ 70 + 8066406139219832808766293792405957181339400972135857184254937033046232

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_303 : Polynomial.coeff recurrence2Scalar2Shift 303 = -((7544756191348171920929456221251964924730286781909 * 10 ^ 70 + 2950150716553270286444822890883120730390972250145605857636141913576026) * 10 ^ 70 + 3761886901368318984426454369039493321209082760776297243279346635278212)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_304 : Polynomial.coeff recurrence2Scalar2Shift 304 = (387380667874796710521320457194671748300738857128 * 10 ^ 70 + 2091634420008123802251864738993649379815316313453366437042376799201194) * 10 ^ 70 + 1822011167082817003517582399480634266011359199921605843608580857904590

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_305 : Polynomial.coeff recurrence2Scalar2Shift 305 = (159555135070741614655828881815535224123031875525 * 10 ^ 70 + 7696059041571811926278595588189926128671543300947072995211029734439181) * 10 ^ 70 + 7905495944488155896172107018974622542850413770905800237087762732192572

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_306 : Polynomial.coeff recurrence2Scalar2Shift 306 = -((68702290666267382153232313904396274235866057601 * 10 ^ 70 + 7021140785149825760817480430482859031168684309635685736921926252159169) * 10 ^ 70 + 4848297443980890621990537762309732557924477542347210991540872468508720)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_307 : Polynomial.coeff recurrence2Scalar2Shift 307 = (17149049075139393637146495841863569550378830320 * 10 ^ 70 + 8381573722891833794045170378086597133351963052872924577183260376740194) * 10 ^ 70 + 1741860589025847166479227923510907594436020581532827830274090940532810

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_308 : Polynomial.coeff recurrence2Scalar2Shift 308 = -((3245525526901188806512110997853544485644439413 * 10 ^ 70 + 4998573619693989138344167545311364965022665241411066202539368622520535) * 10 ^ 70 + 2832328357876301809005604769582749081945054335880280335554115066219173)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_309 : Polynomial.coeff recurrence2Scalar2Shift 309 = (481706024861809648528995913492470820104661990 * 10 ^ 70 + 3773368187555274450903869050959203632605621251334527213901957045699693) * 10 ^ 70 + 2650124013820675682282245062483239812558895509008327559077095170935481

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_310 : Polynomial.coeff recurrence2Scalar2Shift 310 = -((52059813765743852628365948970171631776348343 * 10 ^ 70 + 8075348634891490799636986600321135991795557176058475034457172701031885) * 10 ^ 70 + 4440823655813582594160177442275468745900523042764435677946777107596216)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_311 : Polynomial.coeff recurrence2Scalar2Shift 311 = (2433207032017117137571786631794502380034617 * 10 ^ 70 + 3869829144524447137340178968027442130190556215130319814787030031442878) * 10 ^ 70 + 43494300965351079630564850098837114008184795338554355608573951235453

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_312 : Polynomial.coeff recurrence2Scalar2Shift 312 = (552253338483753230971940742182184109041044 * 10 ^ 70 + 3260808331657794729910267747726535815334164664376155713289587852950759) * 10 ^ 70 + 2408397929585044503289071487417892937877889719148890009603437478841343

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_313 : Polynomial.coeff recurrence2Scalar2Shift 313 = -((191316924085719770471773105292836587814895 * 10 ^ 70 + 1477233637540735107050300345649276905851981780528575088819279363768364) * 10 ^ 70 + 508705477146453816208226159760507833056750526781210734579008145894063)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_314 : Polynomial.coeff recurrence2Scalar2Shift 314 = (35372006347470969764424346186130586463586 * 10 ^ 70 + 5416904328157552745139622371491243713784456981892242337285504433663775) * 10 ^ 70 + 1120236855636385185805699096343770516649227268866085753782295968706641

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_315 : Polynomial.coeff recurrence2Scalar2Shift 315 = -((4687691783439434701264128590790780063500 * 10 ^ 70 + 9513347855353960634825700068642905487390277675974391053623717153125173) * 10 ^ 70 + 2385079246905586379418379645470994455551345544634949218320864419220375)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_316 : Polynomial.coeff recurrence2Scalar2Shift 316 = (439117346704483048115107244616843087021 * 10 ^ 70 + 6167517558429231058159161927920357276447022068307547887428612442376850) * 10 ^ 70 + 2591159178637809445571734918006943021373079441727803506797780367074763

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_317 : Polynomial.coeff recurrence2Scalar2Shift 317 = -((19682267087557350951279478090097942619 * 10 ^ 70 + 9871152599794562337929624641592131467187783304486405449285797886162589) * 10 ^ 70 + 3231958577541271222722875638303472788405219405432377988921778330144310)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_318 : Polynomial.coeff recurrence2Scalar2Shift 318 = -((2326210158239207663862690204725938040 * 10 ^ 70 + 4898021237607022641794877533501001037849913017045592572730756641615882) * 10 ^ 70 + 5524020885552983886641519386894244152008938453465199318498592570884982)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_319 : Polynomial.coeff recurrence2Scalar2Shift 319 = (702446444250908903225852632599603971 * 10 ^ 70 + 3066908883895583051335865780549200622888620749158934321241640980960129) * 10 ^ 70 + 5848574213447606071242001156368288630806221842676956076933277660610049

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_320 : Polynomial.coeff recurrence2Scalar2Shift 320 = -((99422209210133751821668422989127460 * 10 ^ 70 + 1623978028687040045440283649118293809320862258881599861701205535142471) * 10 ^ 70 + 8018120980144001408239338497868998714200841593965782327833309675058434)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_321 : Polynomial.coeff recurrence2Scalar2Shift 321 = (9374327130842815664345925489198151 * 10 ^ 70 + 407008103649330820304402064511619409455115853103170718915619842612087) * 10 ^ 70 + 9639215219911845930661543516728279322599738696872529447828994037285196

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_322 : Polynomial.coeff recurrence2Scalar2Shift 322 = -((527770931051918216721934122690443 * 10 ^ 70 + 6495069927212679012062925000509861669815221490611524410584122552301705) * 10 ^ 70 + 7016139721406402658493316151853278548911400976725023317405993083828085)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_323 : Polynomial.coeff recurrence2Scalar2Shift 323 = -((4831186900238517649925686875102 * 10 ^ 70 + 9719272068437578285670068465336807538863770375022658741930829441182007) * 10 ^ 70 + 475114684321079618524459650551711748682227850003698371766914645058800)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_324 : Polynomial.coeff recurrence2Scalar2Shift 324 = (5179095443412610486433425237779 * 10 ^ 70 + 991892921105293519106374072918471717489675623588866485722462927158611) * 10 ^ 70 + 856303977639058272880287090635799183008449368724831800344771826533351

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_325 : Polynomial.coeff recurrence2Scalar2Shift 325 = -((688560609863678863819723030329 * 10 ^ 70 + 3686336797237342458385215730784315529602885874358881629107950201257175) * 10 ^ 70 + 4280948168775818928906125876346804668257904500563115395159863796415462)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_326 : Polynomial.coeff recurrence2Scalar2Shift 326 = (55489993721153613290326674223 * 10 ^ 70 + 8077194139110870451974413625050627124778409865526352229241924864070761) * 10 ^ 70 + 462792593391765566135041558536878666824191596842946944325027311463981

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_327 : Polynomial.coeff recurrence2Scalar2Shift 327 = -((2696997217982737922739758747 * 10 ^ 70 + 8206548868280415927991922120391839994232261176709073145202668553286301) * 10 ^ 70 + 9032007640423395782943053326948057001901645373661510091608869691330845)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_328 : Polynomial.coeff recurrence2Scalar2Shift 328 = (16539826368328404698973650 * 10 ^ 70 + 7219012765741742283664578363035362823096872311543550226230865339631628) * 10 ^ 70 + 9931381535146830633680470375131260819857996519710383218793319990688477

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_329 : Polynomial.coeff recurrence2Scalar2Shift 329 = (10608904176994182022051160 * 10 ^ 70 + 5238515893417758346514938210014703947282117087829664143350191683763678) * 10 ^ 70 + 2687452371452695322686209784714743067553647912074321433472031675314138

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_330 : Polynomial.coeff recurrence2Scalar2Shift 330 = -((1098230217067524219234117 * 10 ^ 70 + 832701535493644889222215137815601612248618322536932546639530050085237) * 10 ^ 70 + 239014009338948994443425650834983578248185630089096610225628342794058)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_331 : Polynomial.coeff recurrence2Scalar2Shift 331 = (61730037861214972356897 * 10 ^ 70 + 7670779974175721622072331451350063519577108811745434266232993580206194) * 10 ^ 70 + 1462151228522504023351144277142548269113391514605376760461183566824629

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_332 : Polynomial.coeff recurrence2Scalar2Shift 332 = -((1818859585508881544805 * 10 ^ 70 + 8114633831259786331837490077521776498892273041456404035792614258144265) * 10 ^ 70 + 8661011615392757543590286927919225782763658234902355269264931852674278)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_333 : Polynomial.coeff recurrence2Scalar2Shift 333 = -((18007146556516504884 * 10 ^ 70 + 5297807813097462985415101148662278407820299047768087384910925825251240) * 10 ^ 70 + 2528673481278790046667032504264084112574486670494498984814824045273328)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_334 : Polynomial.coeff recurrence2Scalar2Shift 334 = (4924469564155364067 * 10 ^ 70 + 2774412947658833058114994007229914366427414041458956291634043707569307) * 10 ^ 70 + 4839273396835234514608801128432044262450424747170712236489823984326647

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_335 : Polynomial.coeff recurrence2Scalar2Shift 335 = -((258701784841772862 * 10 ^ 70 + 2801413076615569301493041318135533229774468441909551069072413500878601) * 10 ^ 70 + 7857917252830296382607908205666493480165915970858196558108927835234134)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_336 : Polynomial.coeff recurrence2Scalar2Shift 336 = (6553731471795901 * 10 ^ 70 + 7488093568946334491625027899028998469182070668326607201797126154378401) * 10 ^ 70 + 6504905033126892418163682176215273690079010766514651285875351312160569

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_337 : Polynomial.coeff recurrence2Scalar2Shift 337 = -((4661966371210 * 10 ^ 70 + 6358311362669926762088481247006399561379513501003755830676065553411314) * 10 ^ 70 + 2915043026508386236816455701008223170500617146435178524940180894998275)