Recurrence 4 lookup certificate: Scalar2Exceptional 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.recurrence4Scalar2Exceptional_coeff_450 :
Polynomial.coeff recurrence4Scalar2Exceptional 450 = ((28314147841209632009102 * 10 ^ 70 + 1986520005985919458389779400292650625368168031705825365078808030466761) * 10 ^ 70 + 4329173552996007995696733831313683421961149035851312305423497469938316) * 10 ^ 70 + 1785724174495463489016217897543200654798357250465753920911266328187533
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_451 :
Polynomial.coeff recurrence4Scalar2Exceptional 451 = -(((1503893266684341152797 * 10 ^ 70 + 7756642597658637568331951676769236636916266656245237623634120124446719) * 10 ^ 70 + 1385925518049440196763348721567357577226549263541121207325559971967828) * 10 ^ 70 + 5449999450598550675043979451510049753939509168820184596410819263062984)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_452 :
Polynomial.coeff recurrence4Scalar2Exceptional 452 = -(((79987386467794273986 * 10 ^ 70 + 9228989459270151050969457563342986813705442859085166981030401824198803) * 10 ^ 70 + 9281436895131984449616267086502000332097588192296009663519532178117390) * 10 ^ 70 + 6240193243223786689631403354545705372892615224376977523126065756906672)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_453 :
Polynomial.coeff recurrence4Scalar2Exceptional 453 = ((28998575763742349467 * 10 ^ 70 + 5454518338758035995498718878471001551319418157792680348359711224678874) * 10 ^ 70 + 6481125331257749125574690671829708783173369471623710133274916078511901) * 10 ^ 70 + 525139626161116994131723766740686064471898930147774647451260459338134
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_454 :
Polynomial.coeff recurrence4Scalar2Exceptional 454 = -(((3525556380850161672 * 10 ^ 70 + 3290779860621765997623750397928250621854773181244206713421131757707371) * 10 ^ 70 + 1941817723857909484720550562409128168396446779833541446959829523067669) * 10 ^ 70 + 8860892041607004916061208460918513439500609824278389318287383921874420)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_455 :
Polynomial.coeff recurrence4Scalar2Exceptional 455 = ((226222901950331308 * 10 ^ 70 + 504881497110376623410675767711812283890645173099636298545552709132464) * 10 ^ 70 + 8904711249472637312504075375594638064285107595101428431037842690676289) * 10 ^ 70 + 6476493441207322881515230921112877710589762945924135217758162785579710
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_456 :
Polynomial.coeff recurrence4Scalar2Exceptional 456 = ((327850011368492 * 10 ^ 70 + 3214708735166239439376688244869163620710259711080758292784688826775118) * 10 ^ 70 + 6199632980959288119724807474323110142677660053645028296271154080086858) * 10 ^ 70 + 609133368500748539497271935097930542076442875364062520587565379470048
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_457 :
Polynomial.coeff recurrence4Scalar2Exceptional 457 = -(((1822116922485952 * 10 ^ 70 + 6094146544057355066154532704003051840911074380005966874188450712741766) * 10 ^ 70 + 6629650549964847927725196610784524999779631542226795791422304667596397) * 10 ^ 70 + 7136129290637353823569592093817491901585104899254697027685732218600296)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_458 :
Polynomial.coeff recurrence4Scalar2Exceptional 458 = ((207661258754602 * 10 ^ 70 + 3608529380733579572353351288677095652189661186108686184047608645342812) * 10 ^ 70 + 9280902972773687257767091446925049029382802357698370564778758687573457) * 10 ^ 70 + 4406057820951617762829654712054090311183009357451591283135406223639786
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_459 :
Polynomial.coeff recurrence4Scalar2Exceptional 459 = -(((10185856443297 * 10 ^ 70 + 540225376720431785209683061511245951459232267658810029812479507544505) * 10 ^ 70 + 1418349735469317738412938385229805456158672998403974934371913443706241) * 10 ^ 70 + 1545526449216713480187675666311387876524706313435594617139701148751933)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_460 :
Polynomial.coeff recurrence4Scalar2Exceptional 460 = -(((245775244042 * 10 ^ 70 + 4902866114629863100942581979297102883456811151242665213969797191540326) * 10 ^ 70 + 6040003996272766685561394818981938962589082843582266336159444582075848) * 10 ^ 70 + 1652793928701049734795569365449674211023736026438108523040476072313941)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_461 :
Polynomial.coeff recurrence4Scalar2Exceptional 461 = ((78525433744 * 10 ^ 70 + 2797099274761919153299151141155902872508648430896470843413227382899186) * 10 ^ 70 + 9672439299569614569293939951388841562073058704597999753373554391767861) * 10 ^ 70 + 36648544638008428373068087211533647219707379088789470926973100430166
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_462 :
Polynomial.coeff recurrence4Scalar2Exceptional 462 = -(((5330232239 * 10 ^ 70 + 8240958435327624862305384742522446656365637817047131462915095017833458) * 10 ^ 70 + 9373673172258077690181126448874278677511520094854179179740342016567837) * 10 ^ 70 + 1672564354387674900439825891495240226506784278887859221121016206063319)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_463 :
Polynomial.coeff recurrence4Scalar2Exceptional 463 = ((49465417 * 10 ^ 70 + 6114300721682894662184382041551866257826833722719311756661340379729292) * 10 ^ 70 + 5437563410286367575620154300868287770659172341167247742526069597210897) * 10 ^ 70 + 4522237171169652887186820654662467009189447506440943323334293399606003
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_464 :
Polynomial.coeff recurrence4Scalar2Exceptional 464 = ((18292182 * 10 ^ 70 + 8919533653261341416639736650222721516671488694380069982278068554461832) * 10 ^ 70 + 4450657458795168175273153917305976543335563691797576985628007938323426) * 10 ^ 70 + 5056336407327484932778054592278003187425751655838738866581171343918571
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_465 :
Polynomial.coeff recurrence4Scalar2Exceptional 465 = -(((1284827 * 10 ^ 70 + 88772861625531441457826102792519203886745488665361363784890291384261) * 10 ^ 70 + 87254194874983680627998119824594871797809331273577014852666059913431) * 10 ^ 70 + 8251248997287653936846132955542482106569864022389636391178734881038534)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_466 :
Polynomial.coeff recurrence4Scalar2Exceptional 466 = ((7909 * 10 ^ 70 + 9414001053601790431797020415427813554521721457516702662787342633959628) * 10 ^ 70 + 8134114592200292632826889872980318993609064330893730281081757128965023) * 10 ^ 70 + 3895962680853947984442584354906302518862105894275138379896804222131392
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_467 :
Polynomial.coeff recurrence4Scalar2Exceptional 467 = ((3427 * 10 ^ 70 + 8496199788387046442798404762091456827008439695433833419284758628214328) * 10 ^ 70 + 4179919576367944796362070195640420687211277909544348263666898045768806) * 10 ^ 70 + 7334494272130484971190832447158637595772180282191489963609971688878889
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_468 :
Polynomial.coeff recurrence4Scalar2Exceptional 468 = -(((153 * 10 ^ 70 + 6697955462629679405096121708933084344513101891826001628487963786950881) * 10 ^ 70 + 4397825021281584344012809214819930114178285350252496752858117610699214) * 10 ^ 70 + 5657518471831012692923803432445667527542213480132970995791060827976100)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_469 :
Polynomial.coeff recurrence4Scalar2Exceptional 469 = -(((3 * 10 ^ 70 + 1817512410528153078502826649983210257921354798107368213145092129804653) * 10 ^ 70 + 7959628248044464937830383933846539387555534336350547512147267765574505) * 10 ^ 70 + 9658262227577521273500513034707036518617304107007127004900904570197561)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_470 :
Polynomial.coeff recurrence4Scalar2Exceptional 470 = (4025489490301918115825219485964795218710608336363189039081378408022519 * 10 ^ 70 + 2343449862917462361133992029523611392526999298063604751295398184448406) * 10 ^ 70 + 108499904340520308290004082084418811918856936002029163545666012092745
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_471 :
Polynomial.coeff recurrence4Scalar2Exceptional 471 = -((15508506311584031816191079042181862986175366934506812925375481825585 * 10 ^ 70 + 9635969278717583036539664457089308120710538349574214770366493530676387) * 10 ^ 70 + 1569399834575431786282044667228361022880963785572023404958492823062157)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_472 :
Polynomial.coeff recurrence4Scalar2Exceptional 472 = -((6468078761512087065022703221211071198252802778782862663179047758978 * 10 ^ 70 + 7806525976422269827685840469607263436140601042113947669962043441713023) * 10 ^ 70 + 3082106721074153554054756231613210967350081189783874414792878377205693)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_473 :
Polynomial.coeff recurrence4Scalar2Exceptional 473 = (61543466727160600901701403309587693721663329298797010745003277730 * 10 ^ 70 + 3005625715002612524597531947030331661926773018648657879519638487832850) * 10 ^ 70 + 4233569296699372158497447158824906997089473316386657273945677739029668
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_474 :
Polynomial.coeff recurrence4Scalar2Exceptional 474 = (8352686958553728343342389171256586309028268361675078991126803128 * 10 ^ 70 + 9045713211187336021313591845919950631878867043706278440678882653422953) * 10 ^ 70 + 600164881665518167820744078185710382744262089219280063220706434718299
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_475 :
Polynomial.coeff recurrence4Scalar2Exceptional 475 = -((20678855757293616866852354390543791035133089625572757985362963 * 10 ^ 70 + 2694387928780178629261375695153016019029603261394431761345281511539704) * 10 ^ 70 + 7794334307692779518425839653097890166170886734297380408545833544993451)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_476 :
Polynomial.coeff recurrence4Scalar2Exceptional 476 = -((8585936751464978812380320992072260611611769023368963143438959 * 10 ^ 70 + 9813776644095482575972050232074529057282160818637927638241677099044096) * 10 ^ 70 + 2282567393300060135556309603251899527694833387771293238248175152925217)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_477 :
Polynomial.coeff recurrence4Scalar2Exceptional 477 = -((128639210343539312072766969737085673796948363831216762779096 * 10 ^ 70 + 6134279271709917202498230347253483620618782710592044572432564069502635) * 10 ^ 70 + 9110389749934442847372783702706390145506229465273522019409520873720939)