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_250 :
Polynomial.coeff recurrence4Scalar1Exceptional 250 = (((7012890036652317745723994936 * 10 ^ 70 + 585210592432152320510553259264164936190404310955280635819675800659541) * 10 ^ 70 + 5379208991614919027258339135285285533411994603419397217221111537539873) * 10 ^ 70 + 4825097338210869732316295130418773426561583326620910693789716444480495) * 10 ^ 70 + 8997888719510164534354287195007994957318800359744851964654238068683543
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_251 :
Polynomial.coeff recurrence4Scalar1Exceptional 251 = -((((7726929512691935423187376687 * 10 ^ 70 + 9425944222654309271364703448771244008915128784194300105210296369600332) * 10 ^ 70 + 8169285416370031137722451456372041558553528268335005722058166823426904) * 10 ^ 70 + 4050194347523662958866922451164840044896393564158823941312872168921150) * 10 ^ 70 + 4589358729622065396946564053923095344197014080178745152112843775419290)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_252 :
Polynomial.coeff recurrence4Scalar1Exceptional 252 = (((8403239344604566741777159198 * 10 ^ 70 + 8924996328445706539943824642475778780248462517223997365693649506825316) * 10 ^ 70 + 5718195425692372419306948433139041178419094503633860215119673811888842) * 10 ^ 70 + 5731712992086450273457470815168540962135893774463969304838052364516927) * 10 ^ 70 + 1725528998061128053578512805051113766557470839441276741112970331005416
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_253 :
Polynomial.coeff recurrence4Scalar1Exceptional 253 = -((((9020231246741759949419129660 * 10 ^ 70 + 4206957521312352680183611017871964091144706582931366478057922510741800) * 10 ^ 70 + 9509145292209966055920847504597160809459108004783680287642404422950843) * 10 ^ 70 + 9055519775772253484303283835498146171978944914663520005628846086203798) * 10 ^ 70 + 266861273973932692084886362183548303634501978442259036389559762088771)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_254 :
Polynomial.coeff recurrence4Scalar1Exceptional 254 = (((9556978610277603756472169694 * 10 ^ 70 + 1621528689735998614766004260632977069340768840002135322291295136704579) * 10 ^ 70 + 8422127390585853090815955302910895962516044975675326743613983785334549) * 10 ^ 70 + 6049892418764899739360970871803995917232149527897925296562911009260648) * 10 ^ 70 + 574337000629034620466995022495937379398805241961684429431118132795333
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_255 :
Polynomial.coeff recurrence4Scalar1Exceptional 255 = -((((9994382091225129119404349486 * 10 ^ 70 + 1226786325249395431966640633145443944799605782478023355418578536119213) * 10 ^ 70 + 2590269957808719344484057401042861069185378599912205515326384552902137) * 10 ^ 70 + 4488665992569583776172213810014683008867950179967929455321096430441844) * 10 ^ 70 + 1836199744004211641216167178038265048856641726850234036676132542758369)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_256 :
Polynomial.coeff recurrence4Scalar1Exceptional 256 = (((10316290900234845060975604092 * 10 ^ 70 + 2075650478259523607730080965244548566200240883167056483651452417771961) * 10 ^ 70 + 6425824922943044354288085404717011748494954983470752044513003633944820) * 10 ^ 70 + 7485388511582439379940614796584733451626903743031230985706322583208788) * 10 ^ 70 + 7130941181436944100583173692143816928456235544894662587620818066474169
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_257 :
Polynomial.coeff recurrence4Scalar1Exceptional 257 = -((((10510488537250681076887195757 * 10 ^ 70 + 140214149569360426954915381745305830378483098645139936773719511806214) * 10 ^ 70 + 8741708481931825051430131332545497741223397549702605604857993579544221) * 10 ^ 70 + 9548091256317563712252809253472898394383679939429938747538929545735016) * 10 ^ 70 + 748974929409768563148505658427989695365381245856071199200018037737752)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_258 :
Polynomial.coeff recurrence4Scalar1Exceptional 258 = (((10569459388460101510689572141 * 10 ^ 70 + 1079201100962700198838588211918030568106306541272721328804246360739478) * 10 ^ 70 + 3421378649916965290031025376552207947980396283587036819753062289452683) * 10 ^ 70 + 3245465942459096159084395804467420022839217365799724608994491167464889) * 10 ^ 70 + 6876573805486301128125129117800985913048795856958543254801074796621940
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_259 :
Polynomial.coeff recurrence4Scalar1Exceptional 259 = -((((10490869323737097095538658491 * 10 ^ 70 + 7755179716025035163064797137916812161585789270368734052069537754354871) * 10 ^ 70 + 3841256392585430733515008948173521039157817642910497261854498336500705) * 10 ^ 70 + 5160400171759331208168467771336107306277831270568122668864061312980231) * 10 ^ 70 + 6052594432667419846112808855576050044284585710913549738006870711748473)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_260 :
Polynomial.coeff recurrence4Scalar1Exceptional 260 = (((10277717601643254717104550214 * 10 ^ 70 + 7458766723092257757216392634992388255500632457920267168632228170036980) * 10 ^ 70 + 1646389756422678663583637953362385110267425737395643013274577883299437) * 10 ^ 70 + 341274254756710050326501523383304122770126136873449724406799268969700) * 10 ^ 70 + 938044420338615142905282029791003921133530111915043715179979878124555
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_261 :
Polynomial.coeff recurrence4Scalar1Exceptional 261 = -((((9938146399936075677558289522 * 10 ^ 70 + 2931535898165715801305587878012715787975224677639760006705985392924611) * 10 ^ 70 + 2393885093247395731419299937986140833176009698545114883055705359781335) * 10 ^ 70 + 2429617146682086988602021673182611471927108544881568991162179856559506) * 10 ^ 70 + 9717195290335766545236705548534346306134476957365186242673859652946568)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_262 :
Polynomial.coeff recurrence4Scalar1Exceptional 262 = (((9484924869451202139505674193 * 10 ^ 70 + 9470981137103519523080557296608106952569149819606937099406033635244234) * 10 ^ 70 + 6485780345709185675967283407364913636277039432075288198309816631807791) * 10 ^ 70 + 9753395186884825828246377980262441963049343186293377900994534699791886) * 10 ^ 70 + 8415987710472943495951572375080657990255174557400249536224371220766770
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_263 :
Polynomial.coeff recurrence4Scalar1Exceptional 263 = -((((8934653267098201396538498699 * 10 ^ 70 + 5726595399272374496857985662659972716612512546567781460142341619134033) * 10 ^ 70 + 3226012731927169817284974306543156943788050762283765122507385103409555) * 10 ^ 70 + 1087836729032673246949235988073487848629116769427260502394958541812872) * 10 ^ 70 + 8455377146993082311766759333441883880456653885192676939027029636467528)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_264 :
Polynomial.coeff recurrence4Scalar1Exceptional 264 = (((8306756234739230678386533230 * 10 ^ 70 + 839271547947905373179016407617163341089929749103255524765890590228000) * 10 ^ 70 + 3374723837352642122820936903486427185991596365210999689554525006471180) * 10 ^ 70 + 8412111822356736426014601245841472769837579258580279040237876937147420) * 10 ^ 70 + 3154047811208111405261465049059275740258282374753488260492134043259261
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_265 :
Polynomial.coeff recurrence4Scalar1Exceptional 265 = -((((7622350137340241330972926874 * 10 ^ 70 + 6091611455387140070442348160897339948363577538639923501737601404820386) * 10 ^ 70 + 5857736240059243753129946639632711398550380135841951213020141325923263) * 10 ^ 70 + 6185925036554787564280181203413177554065606847260521207170627784526122) * 10 ^ 70 + 6127954604444681576159449252250712679186841392680473391111715733444340)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_266 :
Polynomial.coeff recurrence4Scalar1Exceptional 266 = (((6903076072337556227442363687 * 10 ^ 70 + 9973341869425515204765001482174660808709811505679657621083079922255445) * 10 ^ 70 + 132400771691725519518113546307099831271066263297660534781974871685855) * 10 ^ 70 + 4274904918711201395083417934782164361500086070714524095656775097163368) * 10 ^ 70 + 2581179628800077242215575839869708194005394495412672505640423241564944
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_267 :
Polynomial.coeff recurrence4Scalar1Exceptional 267 = -((((6169987425635837387353569118 * 10 ^ 70 + 5890503601918731247943269570526589968715023500788038049336758173080297) * 10 ^ 70 + 7648368840158301817887306882263045168309932931023615923273334997344443) * 10 ^ 70 + 433842216297216288866865759794063496862338367377397144738902734985320) * 10 ^ 70 + 6874658812467047446785240538564331124050637137372215362116005287571190)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_268 :
Polynomial.coeff recurrence4Scalar1Exceptional 268 = (((5442569566647864634999277077 * 10 ^ 70 + 5003313699009596596886366700493745808847609168302030422581048975642651) * 10 ^ 70 + 2907009048283083983323260061362098795524482647343513646559606755165526) * 10 ^ 70 + 4033980723941896856074355563642189008846802577698606391966532342476648) * 10 ^ 70 + 2831423417116313803798486143723503859956406018151880327996793833262537
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_269 :
Polynomial.coeff recurrence4Scalar1Exceptional 269 = -((((4737951317235291980200633154 * 10 ^ 70 + 6886651909028446041112586228210054537818105759155492550896666196992629) * 10 ^ 70 + 7124510457731553601724657517667785111540471168335324910421288231250314) * 10 ^ 70 + 3794539246088381054036640635324179645129940480837811100399725079144771) * 10 ^ 70 + 6497598316094194584005005672554555938147038278696568986450065171004154)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_270 :
Polynomial.coeff recurrence4Scalar1Exceptional 270 = (((4070345730012094871011010720 * 10 ^ 70 + 4203279648899498767806627153149930206594356535990254295792156149038534) * 10 ^ 70 + 6575247618608696992969438618216772398921833908025331005829528374505526) * 10 ^ 70 + 3441506429871307009444953430595654783958022236263054253943337498686499) * 10 ^ 70 + 5753684845633863803129976609220220673988607709730810308406061786778979
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_271 :
Polynomial.coeff recurrence4Scalar1Exceptional 271 = -((((3450734271080299749359766926 * 10 ^ 70 + 647063635581381096224037383083317628894125927644493152842582458242867) * 10 ^ 70 + 5335835029105809567916261709065805577020813278130083250008803203942122) * 10 ^ 70 + 658370945974865090086860280058913108511644076343908256649191253273025) * 10 ^ 70 + 2594977238535934444878152313563034426604177830526293026291722442975316)