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_458 : Polynomial.coeff recurrence4Scalar1Exceptional 458 = -(((1159882075880680663 * 10 ^ 70 + 6177991783263941942547087105231269263389114686465703349221550395284304) * 10 ^ 70 + 8335386703173334767639551752251849874950319115952483426265575759964416) * 10 ^ 70 + 6451623138791142360780930577838288650076613459661060950394725441855867)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_459 : Polynomial.coeff recurrence4Scalar1Exceptional 459 = ((178576555968421764 * 10 ^ 70 + 6822656398144545550755335983764998781638128549295733072069604856788394) * 10 ^ 70 + 2043190721006894067536604870146128391563599352502600541713696280512173) * 10 ^ 70 + 3285277276348689988276114987402313321462540863269681566546317000672630

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_460 : Polynomial.coeff recurrence4Scalar1Exceptional 460 = -(((12730931210288179 * 10 ^ 70 + 7512752298864473365188853336650801670045207185012611637442945804941967) * 10 ^ 70 + 4296761405268428670415653103701015178826656000637355305056820147482204) * 10 ^ 70 + 1157440951009116247417566810463037068028115687771876421614154436454168)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_461 : Polynomial.coeff recurrence4Scalar1Exceptional 461 = ((109627124103007 * 10 ^ 70 + 3847319186244893064606165571124297299984962396776207781661499257993517) * 10 ^ 70 + 839331312072012883740841345809626616000770070889006726528432135117146) * 10 ^ 70 + 4664462524881750342710093663599673047378681389654334418522860763353458

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_462 : Polynomial.coeff recurrence4Scalar1Exceptional 462 = ((79361601428302 * 10 ^ 70 + 5822009749887516717005551592273685790697386311757012890049202726807966) * 10 ^ 70 + 7433936318343660051682071515302700862551653943259650117633753664852788) * 10 ^ 70 + 6820082106957771950405059114381902654630872303149685414570875351056882

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_463 : Polynomial.coeff recurrence4Scalar1Exceptional 463 = -(((8843060297664 * 10 ^ 70 + 8325353416264147110994081650010326195784660685024224893754197827702834) * 10 ^ 70 + 3606363707469766397177017248871774625029186052587143503132904468963661) * 10 ^ 70 + 9994036759089488114510381548733019454645067817067516454085016376006115)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_464 : Polynomial.coeff recurrence4Scalar1Exceptional 464 = ((358237517589 * 10 ^ 70 + 3997283419741407734663961174799953172447112765613546415397179166944642) * 10 ^ 70 + 9663521563804720650279484060314287045935048110443303168743651500210441) * 10 ^ 70 + 4353256879387551263956390420480979242380369287471265714878039353726800

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_465 : Polynomial.coeff recurrence4Scalar1Exceptional 465 = ((17433473663 * 10 ^ 70 + 5064477574781163647814577148997398393404549489819233866524692633665731) * 10 ^ 70 + 3702507961247296602634696923482231428770332334805902113982510658757810) * 10 ^ 70 + 8203579836555561291194073524839751257465067289708146823243869465008029

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_466 : Polynomial.coeff recurrence4Scalar1Exceptional 466 = -(((3170784786 * 10 ^ 70 + 2332912225758195758452039580819070640160121258301513645264750977637796) * 10 ^ 70 + 8925994480279880395842338752636029272643363764936285657593472107257154) * 10 ^ 70 + 4996521928932141667228593389143758204938098187658664929415213770061970)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_467 : Polynomial.coeff recurrence4Scalar1Exceptional 467 = ((148792286 * 10 ^ 70 + 5980903895155158028027947910383626100398937805195226784327831114715540) * 10 ^ 70 + 6546511137467335129078904215467717048210886467698938550686674337230592) * 10 ^ 70 + 1237456933024677964892678914852947407955622891372260806162036310989006

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_468 : Polynomial.coeff recurrence4Scalar1Exceptional 468 = ((3386132 * 10 ^ 70 + 9892209873401029579126046356117930938040546654626857583992655726739430) * 10 ^ 70 + 8855688248425670354135882717415271078883448058900038635034628419846727) * 10 ^ 70 + 9711437163530483082609472684181388902761163391009425864392263815005003

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_469 : Polynomial.coeff recurrence4Scalar1Exceptional 469 = -(((742119 * 10 ^ 70 + 678472644670985095895755881997689120694206793776030397900471794707427) * 10 ^ 70 + 4895954661588434738306210785375810931708511886421580585508770741085694) * 10 ^ 70 + 2952749263820107307025299123562713677437633203032551962990508331990636)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_470 : Polynomial.coeff recurrence4Scalar1Exceptional 470 = ((25839 * 10 ^ 70 + 3310408858395645383762570026529234517706286557099182529484051475798442) * 10 ^ 70 + 2014571531209168361376913432198206936486854476434412331480563307396445) * 10 ^ 70 + 7172384521656166393488725189056053296250023084705844769827852558307368

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_471 : Polynomial.coeff recurrence4Scalar1Exceptional 471 = ((1099 * 10 ^ 70 + 6317629491777711552831616804808818306190694855631479451570427246053989) * 10 ^ 70 + 6308750221462750938719544557875781003375165647966304447455815784266442) * 10 ^ 70 + 9370934903188757463836405995098015605328687158792267483403216342491574

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_472 : Polynomial.coeff recurrence4Scalar1Exceptional 472 = -(((108 * 10 ^ 70 + 4972697791453582204347284223863341647685832936973986853865878957833737) * 10 ^ 70 + 6828308556375838287761396229070963299081083309790144740468319839374889) * 10 ^ 70 + 4084161215165187124836402012241193605201554791841620922285675310235411)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_473 : Polynomial.coeff recurrence4Scalar1Exceptional 473 = (5667451028363976035077550494568203176653186889462620253492812546633629 * 10 ^ 70 + 2986726253339470288533727956458124255560728112256907195192180473461160) * 10 ^ 70 + 1342140559918573497147158337728584873857296546491422336263951847747852

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_474 : Polynomial.coeff recurrence4Scalar1Exceptional 474 = (2168692204379747848199723358282715236230903034569488728216737389388318 * 10 ^ 70 + 5375196616854925757382635465387447042843480161524260782492236289901807) * 10 ^ 70 + 994464934625610138854741714071986507302987954697120876765686163924716

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_475 : Polynomial.coeff recurrence4Scalar1Exceptional 475 = -((45990075860489582893381791059194114731099269732470019876839831345593 * 10 ^ 70 + 4804897259986769464189140438516186345388753147333514335091007779575799) * 10 ^ 70 + 7426323652016413326301380157464076127736004623883315392941167510201877)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_476 : Polynomial.coeff recurrence4Scalar1Exceptional 476 = -((3156060433670065619328225879692325890279038183323999169121177067843 * 10 ^ 70 + 5383734457679116547683519145790692363549444317815532193291641320070125) * 10 ^ 70 + 3496963682411849065860110990205149368853358172935858903913212304637825)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_477 : Polynomial.coeff recurrence4Scalar1Exceptional 477 = (80125690147855018644270650229550049709695690891728734550632303462 * 10 ^ 70 + 1638775290758582736990379839724309515424508121581465452673675137188810) * 10 ^ 70 + 660669965240481449448723622845579408646360621103946854923060911405224

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_478 : Polynomial.coeff recurrence4Scalar1Exceptional 478 = (4269811907579749141997586763313639205922843288374886295677766558 * 10 ^ 70 + 2632960483308507846946420942242854698008997963345557562516436005546173) * 10 ^ 70 + 4091942435817734987381366271009338357486174830436761216247729535652557

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_479 : Polynomial.coeff recurrence4Scalar1Exceptional 479 = -((58330672301131239365497806399289902117134742371015606444904545 * 10 ^ 70 + 6731167955439490456184403152374590941000016308207588636771056793069223) * 10 ^ 70 + 1176537025134688514838511045080083342937546849130205026886012251780556)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_480 : Polynomial.coeff recurrence4Scalar1Exceptional 480 = -((5077389193269732359675298544962926879861679155265635905201498 * 10 ^ 70 + 397119998228922851351531370703449590874137340222027595143424586809499) * 10 ^ 70 + 4348548255638297150141858366900770362999123959966227963520793959765611)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_481 : Polynomial.coeff recurrence4Scalar1Exceptional 481 = -((44314752784628604038936492935738752314484713728336606701504 * 10 ^ 70 + 8138671782391326840040584112730626240379705083230885727228445937826841) * 10 ^ 70 + 6272219464158548378228789032746511904048044933047980024412523010879465)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_482 : Polynomial.coeff recurrence4Scalar1Exceptional 482 = (2843144209820886122213137969581903119891099228271814613955 * 10 ^ 70 + 313858717062534976670299625914507001316090111948580230881750702915353) * 10 ^ 70 + 2414426210466922020786022580226935039587154616131808252871835616857070

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_483 : Polynomial.coeff recurrence4Scalar1Exceptional 483 = (112525381270924657698311394151515330138594674182318301353 * 10 ^ 70 + 8873793556326748193605982669933733310360188603324759858232273799729851) * 10 ^ 70 + 5025991958710342984402047658262389815080484142034908671933383947089342

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_484 : Polynomial.coeff recurrence4Scalar1Exceptional 484 = (2166947783736965217425565816670288068923863876817644565 * 10 ^ 70 + 8202772094702821305488330698723237889251434614707399344191006150342035) * 10 ^ 70 + 1073385183888527820723615474436584147288487428970578390382572178759997