Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0MainPart0.Coefficients112To141

Recurrence 4 lookup certificate: Scalar0Main coefficient convolution #

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_112 :
Polynomial.coeff recurrence4Scalar0Main 112 = ((657869401583866899453173797485002321 * 10 ^ 70 + 7210948258668213119494403888635019463153835512704205644195589568297289) * 10 ^ 70 + 6806525141871504645203837216231431275383464584048834530928978337188558) * 10 ^ 70 + 9885940264958393387741752822557376216534137808530373925938255341237907
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_113 :
Polynomial.coeff recurrence4Scalar0Main 113 = -(((6189968587639320393932323827006751223 * 10 ^ 70 + 2511994312759236790584247557606832258263578040173091205068252495668321) * 10 ^ 70 + 5082436047999858916204530436809571921320647134131530396242854110674877) * 10 ^ 70 + 5837834197491576335997007686014726977769445202835567705532780961174579)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_114 :
Polynomial.coeff recurrence4Scalar0Main 114 = ((56815901726409006963290099914943220485 * 10 ^ 70 + 9647137522588220932732872111802143980560547820623770960863656613003600) * 10 ^ 70 + 5979409037598285470299016364527270131543635629482211694699094133316298) * 10 ^ 70 + 8641439964569015309514317023635251562163261179026391653489796510826765
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_115 :
Polynomial.coeff recurrence4Scalar0Main 115 = -(((508941704059742493745770824122505908043 * 10 ^ 70 + 311738904811409506863291756782949648203998523977495550869143280436355) * 10 ^ 70 + 669131958362470936316485250735045811654788031674618240472916705498166) * 10 ^ 70 + 6610164970739325889844667405483825432097336686468495650591473182331419)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_116 :
Polynomial.coeff recurrence4Scalar0Main 116 = ((4450973407753940663868948768362312815464 * 10 ^ 70 + 7542146663089180725943249645962377720969221443682268114816278545603250) * 10 ^ 70 + 2581599592168395180623093037978517550298416092436796557808412351084534) * 10 ^ 70 + 8527037302103201238038863695696505698270438093532607006810971055220943
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_117 :
Polynomial.coeff recurrence4Scalar0Main 117 = -(((38018287747449534422394290520103321314226 * 10 ^ 70 + 515493030005598748072770282631790532845887545800619703487447845183305) * 10 ^ 70 + 8031738282614078803353611849322782288238326466054995528145566437673761) * 10 ^ 70 + 7071718840233657921622900942971357650954393085548454097805731148952330)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_118 :
Polynomial.coeff recurrence4Scalar0Main 118 = ((317273132083460058385472343968138793883005 * 10 ^ 70 + 7637287210542911087003434630993152316192434402999520860495317944702798) * 10 ^ 70 + 6856269581385413180976714572047983461899455413462233085019312389550175) * 10 ^ 70 + 4056873077349418375453955799622887015632384746395598804573250197883610
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_119 :
Polynomial.coeff recurrence4Scalar0Main 119 = -(((2587746038252377126672703695194495198649411 * 10 ^ 70 + 1364283457632932226888596295684920185850939202244492643488432315969259) * 10 ^ 70 + 860995114603581704434185455943183272075852870204579876715979304638583) * 10 ^ 70 + 5248382940910567750432075179485817024850660869280900536421752658265994)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_120 :
Polynomial.coeff recurrence4Scalar0Main 120 = ((20634536780271312817705738437997014773560255 * 10 ^ 70 + 2821840941740987285183862454098110049269603118245565832987317932801390) * 10 ^ 70 + 8338947341511413127156986475599019962611185506625531664705931040894299) * 10 ^ 70 + 7079949631257518690365835679819669255150775556221164943377666376839432
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_121 :
Polynomial.coeff recurrence4Scalar0Main 121 = -(((160909989021293386562695498058648056598143221 * 10 ^ 70 + 2735503493692315059121615025746629652638806011364617785216536666052878) * 10 ^ 70 + 2961746233582196486572406129816982832605105828152725430843715941179399) * 10 ^ 70 + 5350157472971612611831732350875695404028441568583445653538175325380989)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_122 :
Polynomial.coeff recurrence4Scalar0Main 122 = ((1227470310279126843416676510267184398788849278 * 10 ^ 70 + 6565609389457781267166083843865066781799710564398764891283659400631954) * 10 ^ 70 + 7360142404545188073062302042350926461339684594757839697822861371112283) * 10 ^ 70 + 9671954197338166507560817194582938717995576857454713102861445069531690
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_123 :
Polynomial.coeff recurrence4Scalar0Main 123 = -(((9162156995312255327445665935112370091058166618 * 10 ^ 70 + 1121592568125789042546860380988724063282379027522066742725517384216589) * 10 ^ 70 + 8250459795383160262319890505940354363310551848376997220627693382790280) * 10 ^ 70 + 113391240352303571592868849497037371554366628602687712892996517105506)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_124 :
Polynomial.coeff recurrence4Scalar0Main 124 = ((66935609485437236116710585005211001115518401743 * 10 ^ 70 + 1116628956039630024281206319769897340338709217728662123547040047562204) * 10 ^ 70 + 1416142250676221861120263429399976776232157210791197236924231891145498) * 10 ^ 70 + 7047404505856309851565533476977313655854935676681302391140807705584328
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_125 :
Polynomial.coeff recurrence4Scalar0Main 125 = -(((478739073854523519363741810492664993016746558430 * 10 ^ 70 + 6922217164008445388942537319782496469342552055834536298335980153857463) * 10 ^ 70 + 2321100505580686580460601602257550338963804516315836193883701917120617) * 10 ^ 70 + 1519570451875009733115540631143923670414708288596097337361034223493123)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_126 :
Polynomial.coeff recurrence4Scalar0Main 126 = ((3352955698660662172910000865881729705691059840088 * 10 ^ 70 + 6405586656396223573973095605859744159015763662202759307312761920301581) * 10 ^ 70 + 9287563340172519267156439492738710820258773736464443769893192469792002) * 10 ^ 70 + 8683166349629871016152600974724211505437972257811467852821931325909561
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_127 :
Polynomial.coeff recurrence4Scalar0Main 127 = -(((23000919573433758841812864837629367905288444770368 * 10 ^ 70 + 6888867660015634507735514727596103174233502601472268113245228969990024) * 10 ^ 70 + 4952340335020384341060086319476985925621937535159287433346423425262704) * 10 ^ 70 + 6540600413495330757241499323853392926928733759471753426659698311068952)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_128 :
Polynomial.coeff recurrence4Scalar0Main 128 = ((154578284303360972052489793869737892988287531894135 * 10 ^ 70 + 4723537621317307339219640321240143044038003372944127977704103603161850) * 10 ^ 70 + 5109172544518896255431396875694600351029728090331723071438814546170589) * 10 ^ 70 + 3486497004626623979355064201432072143431941104076865478686229813334577
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_129 :
Polynomial.coeff recurrence4Scalar0Main 129 = -(((1017962208889608527549540522764657383520173124892507 * 10 ^ 70 + 9957234857836477424687415949953975910603439233112047865695666400148977) * 10 ^ 70 + 8589953609535945528562870692510448773605355542866116062786392983459300) * 10 ^ 70 + 9421795465010280482730045337274394746018383074517812516872301215832158)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_130 :
Polynomial.coeff recurrence4Scalar0Main 130 = ((6570303853474652163986843701081779478846691092113147 * 10 ^ 70 + 774088311303279549846208870295714880522053377394381430851298164712238) * 10 ^ 70 + 1823583353217784544108236022269708390384864067580401200063153476298497) * 10 ^ 70 + 1349680997693613894042595602619816177088442984222942944312223560713298
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_131 :
Polynomial.coeff recurrence4Scalar0Main 131 = -(((41571677808660979972905431835836798567801478598587579 * 10 ^ 70 + 231349860753617394973534580095576046255617447227849265341426345324059) * 10 ^ 70 + 6614276302689417890139258872670229277317981145619903611180016281887975) * 10 ^ 70 + 5240059432461264855698338172398925115505164164904502989567166026690268)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_132 :
Polynomial.coeff recurrence4Scalar0Main 132 = ((257900822724604245006333622742879541431429835078386371 * 10 ^ 70 + 886917085494918621142028403722256888360777571723483545193196334700749) * 10 ^ 70 + 6075883491871489840896649810387309838962294158399954313311674629612834) * 10 ^ 70 + 6433757253710972466933343633575010076728839457089195391663243004453642
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_133 :
Polynomial.coeff recurrence4Scalar0Main 133 = -(((1569036386805732574944103217166790713390745248482788373 * 10 ^ 70 + 680656250485785290451615118389264716366405608572109607845813603938641) * 10 ^ 70 + 2679656244073062526256380146883869342962221133021770692237293486929220) * 10 ^ 70 + 2330902888922877102075608704842062504569800030679540350731236760039433)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_134 :
Polynomial.coeff recurrence4Scalar0Main 134 = ((9363060906658648295056749219533432174290566987995282537 * 10 ^ 70 + 8180467851811615269200363767412310675703562665008012520577003139289359) * 10 ^ 70 + 5999120827646605417579797124146634483174334036312724190298378512670923) * 10 ^ 70 + 6830385551793108417270533191228624458817173081454552455005213257119346
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_135 :
Polynomial.coeff recurrence4Scalar0Main 135 = -(((54813077013396195942008797225147712579288391551848291152 * 10 ^ 70 + 8556055382774017223256010969612024569120383553475115057199594680908304) * 10 ^ 70 + 6764553541640800933228787788989358407785119236288149225638911435244736) * 10 ^ 70 + 7655544278664390401835006993824047163019658783371824058950305874057802)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_136 :
Polynomial.coeff recurrence4Scalar0Main 136 = ((314852111050451851041288382043211104414820764013870259418 * 10 ^ 70 + 3172080865927869206192157548592808753614608310204222727419255926817276) * 10 ^ 70 + 7253863430969536221356515508522430317185560711084328626643084912975466) * 10 ^ 70 + 1792978705668442998468753728662207507483459593714881853663104129232363
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_137 :
Polynomial.coeff recurrence4Scalar0Main 137 = -(((1774832870898751178215504000821005850180789178885493076929 * 10 ^ 70 + 4613077117187437493693215697876926817672503884381507257744037518613750) * 10 ^ 70 + 5847195296779594160856578805556818556398762203186208697005045646243829) * 10 ^ 70 + 1651456148581021903099297943919528384529100083572251610483353100971599)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_138 :
Polynomial.coeff recurrence4Scalar0Main 138 = ((9819896630583578637069129508800370062764332173824960080480 * 10 ^ 70 + 1179694725703392604078751556334235270474015411820885805837420084074867) * 10 ^ 70 + 3861972829329402909358476208517070872993330681653947255480614969602177) * 10 ^ 70 + 2829050897188215048797749217411527471284875789365732012454898010158155
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_139 :
Polynomial.coeff recurrence4Scalar0Main 139 = -(((53336322223547533106794403850746906602449651259348235146029 * 10 ^ 70 + 1529745124831636433095703132629431098904858554389576118338827669244258) * 10 ^ 70 + 7959142610756461207804956980270442858426270234976412340231777157841324) * 10 ^ 70 + 3877897725395094799713774292952692557909458203887686589490918006443334)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_140 :
Polynomial.coeff recurrence4Scalar0Main 140 = ((284427784681169867494926874120980745165724799597265241881388 * 10 ^ 70 + 1685863996690571574915966852522169054562035340600462229305618158283126) * 10 ^ 70 + 1864748489271356252598326130214316482313479505709972507303019583279520) * 10 ^ 70 + 4778695468658272578644853611232258505862232920651178885161298605543850
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_141 :
Polynomial.coeff recurrence4Scalar0Main 141 = -(((1489422687195997424009409474090383381013815706250306444891325 * 10 ^ 70 + 8340062848859028899575495806784001839495312304319767408958126466673938) * 10 ^ 70 + 9338223746758706058476622642843651775901624162479174005160926684421539) * 10 ^ 70 + 5022197647143685318046644803743581986348843932532062210550315068855796)