Recurrence 2 lookup certificate: Scalar1Exceptional 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.recurrence2Scalar1Exceptional_coeff_258 :
Polynomial.coeff recurrence2Scalar1Exceptional 258 = (2184504747302033324609489690037910445968791251494253031 * 10 ^ 70 + 8565184718945359895369245920553849685734027485612823929751403890005181) * 10 ^ 70 + 3769704277420895987258408779091034289077513005783103317078566877167788
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_259 :
Polynomial.coeff recurrence2Scalar1Exceptional 259 = -((1041323194739635889152635728146647646142197149590036152 * 10 ^ 70 + 9686131573889654408382644591584142823718657765580226728103671256940674) * 10 ^ 70 + 5623303912801487187190498773413235952484304094101006904849815910731325)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_260 :
Polynomial.coeff recurrence2Scalar1Exceptional 260 = (437485109783086109324328819578783940844124188355283752 * 10 ^ 70 + 211549899714733960178859587918410030841059292063669036010916709475185) * 10 ^ 70 + 5328036573742044835069347922686042052852856165127070691550948197090890
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_261 :
Polynomial.coeff recurrence2Scalar1Exceptional 261 = -((163528573869556786987501643177639995215158899188376891 * 10 ^ 70 + 7080782411018406459000983267156617725706761144832932711266933527438477) * 10 ^ 70 + 5747615479992819946122494914531105758032335227052031749518220731850624)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_262 :
Polynomial.coeff recurrence2Scalar1Exceptional 262 = (53840021776045105093614988561267078939944661601380319 * 10 ^ 70 + 6076559244940886787501094057448233539888418019840326392488433639364562) * 10 ^ 70 + 7911467316689193089384972757077834810848307287170601665051463330510473
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_263 :
Polynomial.coeff recurrence2Scalar1Exceptional 263 = -((14802253981067972504934982362924926887124053429634696 * 10 ^ 70 + 5757214249684831360133696255638898715893700560921934978684088427845644) * 10 ^ 70 + 874904397009835605671741979120255607065940949300570958164367680048198)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_264 :
Polynomial.coeff recurrence2Scalar1Exceptional 264 = (2609835216285974475213494431694238885732375411890731 * 10 ^ 70 + 471200142676432321745508364048189354647756327849444522502887147328961) * 10 ^ 70 + 7033790217289110102391964754094376422693513488310959152267199517509135
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_265 :
Polynomial.coeff recurrence2Scalar1Exceptional 265 = (506074841025927124709545345942944922280599429649027 * 10 ^ 70 + 2690938939159366845314330719277905794751202530575606286125805854218406) * 10 ^ 70 + 2895486023269091306616231849675119632967027706501291818999550128651815
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_266 :
Polynomial.coeff recurrence2Scalar1Exceptional 266 = -((925876573057010616747879539194460290971502228091411 * 10 ^ 70 + 4970470449422209861649798382042268302398169888735133200474582913550634) * 10 ^ 70 + 1436414899841050831984530376721261737254680854819921033593811342199841)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_267 :
Polynomial.coeff recurrence2Scalar1Exceptional 267 = (701493559685272532679419546164001717512905995648673 * 10 ^ 70 + 3330874571606305914664170072575465668206346474768004852881627471404613) * 10 ^ 70 + 1653523209480982345076402888794967427411805291224738092248980421926118
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_268 :
Polynomial.coeff recurrence2Scalar1Exceptional 268 = -((420392789695734837937121543084914106025034377243729 * 10 ^ 70 + 3373591932901044291550420819124519351677247563643322191984177011905895) * 10 ^ 70 + 5462703869373757097036461461585922177694735007717898046056617646878616)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_269 :
Polynomial.coeff recurrence2Scalar1Exceptional 269 = (217489051166540956434200245542125306565386301234374 * 10 ^ 70 + 1564954825214605477877783069374355492765986810588100620129575396327911) * 10 ^ 70 + 5307195499831414237635308906790127746360156004887265866045650811281518
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_270 :
Polynomial.coeff recurrence2Scalar1Exceptional 270 = -((98340238504012480889138072060446228606955474883089 * 10 ^ 70 + 1207059576356421402180198127500696158593518324563076335255993881943448) * 10 ^ 70 + 9383685454063235023759918048009678037433551252352612317104513870848547)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_271 :
Polynomial.coeff recurrence2Scalar1Exceptional 271 = (38120919228884517381483887267413530239741400782368 * 10 ^ 70 + 7902288491408393706843070512945203622738767058402416643853647688665191) * 10 ^ 70 + 751195123110763813368175838129258432357050802013631436274960910709793
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_272 :
Polynomial.coeff recurrence2Scalar1Exceptional 272 = -((11853476396326974167368984742918566015512152940519 * 10 ^ 70 + 6633587589776093458109627919079218056000365628492707035537196881677914) * 10 ^ 70 + 1553444472298813426075970097626769071721940778101932161760230548922902)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_273 :
Polynomial.coeff recurrence2Scalar1Exceptional 273 = (2246123717209421677595866672675350867046007613228 * 10 ^ 70 + 1030938953383516638387029245729719478720133814162502850452830070618341) * 10 ^ 70 + 5939461245471744773296316662123744172986726057865048516030284647068849
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_274 :
Polynomial.coeff recurrence2Scalar1Exceptional 274 = (422437618448613377321595837314087306773346995939 * 10 ^ 70 + 682160608346267723106785032818241761415237483587308506393902459011011) * 10 ^ 70 + 8968880043987852480905239798987646126872209895773240145845482100566934
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_275 :
Polynomial.coeff recurrence2Scalar1Exceptional 275 = -((736661539716578859351969249080114006081840022098 * 10 ^ 70 + 8197525183376184462598772831620296519845275530461329350219152708751262) * 10 ^ 70 + 2867223244460142042029593633242111786075536308945414036363026093157541)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_276 :
Polynomial.coeff recurrence2Scalar1Exceptional 276 = (495312937619988782188096108823294971304005762111 * 10 ^ 70 + 5472928583961738523125261233279865899583659349304722318982382340536825) * 10 ^ 70 + 7790302119551478281905074512111323839903346046244874711973278601855578
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_277 :
Polynomial.coeff recurrence2Scalar1Exceptional 277 = -((251484773881498340751675969719506462481496782784 * 10 ^ 70 + 2194046633330013723800306063249257152217137920490442919933759645035438) * 10 ^ 70 + 9025642328127356603616379718705341539905448285760499059514044609373616)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_278 :
Polynomial.coeff recurrence2Scalar1Exceptional 278 = (105529917226001600547138826612528151578669662722 * 10 ^ 70 + 6390554926976845993869576000072507893260012084502400596946027572727978) * 10 ^ 70 + 1651754204576217878038096258430353660522425068429292041074781605573017
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_279 :
Polynomial.coeff recurrence2Scalar1Exceptional 279 = -((35910999641676217974502284904659567333541544011 * 10 ^ 70 + 69105401002549266702096317055200999427290151687319666245875379543475) * 10 ^ 70 + 6377280774951695859848117229823807655194028779581765654096590017205408)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_280 :
Polynomial.coeff recurrence2Scalar1Exceptional 280 = (8245083674630212128765448772456800407214586203 * 10 ^ 70 + 6354566928045829293115254330124750822659966720357585513900625048884804) * 10 ^ 70 + 5880667301610533102133943514023403869198885163045339148063662892269320
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_281 :
Polynomial.coeff recurrence2Scalar1Exceptional 281 = (411237471608906739216584211368111277811425248 * 10 ^ 70 + 5490688562709363789719798109385394646075337992156678202392829878461877) * 10 ^ 70 + 6995165646499885373428711554194698095466994388038430143880768495950203
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_282 :
Polynomial.coeff recurrence2Scalar1Exceptional 282 = -((1906868444398349072812764040985052552133159958 * 10 ^ 70 + 7533350731704272088390323892502069898668001958835782328711693553398869) * 10 ^ 70 + 1467904947234030707098788627346584387508043443449854461502952616716747)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_283 :
Polynomial.coeff recurrence2Scalar1Exceptional 283 = (1391629501884391733677362727907458227440171188 * 10 ^ 70 + 1981705782641999906225827179237132531786263472384761375897361638305419) * 10 ^ 70 + 9298880794650851540284265550220087532305615279265899973135255981899870
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_284 :
Polynomial.coeff recurrence2Scalar1Exceptional 284 = -((697686086963904293807721636832923336195412453 * 10 ^ 70 + 9667174981559504999009609620047534227760040254592347212257109260619468) * 10 ^ 70 + 5989375074185782134455559792478906361416509873241889176830425089261275)