Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1FirstPart2.Coefficients277To302

Recurrence 4 lookup certificate: Scalar1First 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.recurrence4Scalar1First_coeff_277 :

Polynomial.coeff recurrence4Scalar1First 277 = (((494895085461110436772500413 * 10 ^ 70 + 6981681160833280586321571978515318318337576712290015460303162715135884) * 10 ^ 70 + 2668741191398412016162865030375266360620459911427975175304612994264522) * 10 ^ 70 + 3237520329943979440755127430900833206707321465413604089456066340067109) * 10 ^ 70 + 9890933335912556445522594594865050065492963918937945190061552661397905

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_278 :

Polynomial.coeff recurrence4Scalar1First 278 = -((((402892609375738616822307784 * 10 ^ 70 + 6584670831949709320228168724588380842222201702403217284716268741690204) * 10 ^ 70 + 7796180487296444065294158546206537395997774353443682547729524240063108) * 10 ^ 70 + 8819796704583720547317167614083389774739899585278903224460804932978145) * 10 ^ 70 + 8368859036085661916010762477077070997969883917166815245083187248736969)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_279 :

Polynomial.coeff recurrence4Scalar1First 279 = (((321577631412161747554452692 * 10 ^ 70 + 6165400475697720569891972886294193174888943068008514545963885314910132) * 10 ^ 70 + 1081631619956240915066061403140360319810841252374968619139379466913534) * 10 ^ 70 + 443276606391641206757893056812899829304860929527880952643629812922721) * 10 ^ 70 + 2639471474207874723205915287995859582990615243367780570507468446284363

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_280 :

Polynomial.coeff recurrence4Scalar1First 280 = -((((251829082274363794362845829 * 10 ^ 70 + 3180916357121323683049692340877789048423794911254929860437138143819948) * 10 ^ 70 + 9647197719966779971993036126491247034260896383502065977897779966041717) * 10 ^ 70 + 4360726907491449909138572189790784382851466643062081175979382812215373) * 10 ^ 70 + 2255369677980507394982652806198184600317644908073330677939025473751259)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_281 :

Polynomial.coeff recurrence4Scalar1First 281 = (((193587157651102352017062433 * 10 ^ 70 + 7810595351762292874610357790641851348609738511228341669064420711225410) * 10 ^ 70 + 2385801069925137164581969928292694518723227576301980562336099506797197) * 10 ^ 70 + 5111295520007198153562032272309860910348870876046326458701030845676449) * 10 ^ 70 + 9626687448471081256161718260049790452838049813233366925510909600085148

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_282 :

Polynomial.coeff recurrence4Scalar1First 282 = -((((146138538944486735259304646 * 10 ^ 70 + 8220241877362468977708191625452472230437636823027031737158289452204250) * 10 ^ 70 + 8417991115281258424150890916334255572011376348103576199885453134810325) * 10 ^ 70 + 3804869760472881081115469465158417786216898425623949556450550195205664) * 10 ^ 70 + 3964639010010031949320502424686240213195749539873371702782232693448537)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_283 :

Polynomial.coeff recurrence4Scalar1First 283 = (((108364800727942824709768024 * 10 ^ 70 + 1241265299595549236457780178437951365009346178245731373094831149348546) * 10 ^ 70 + 3885016625222763024962032029608484358976137651607240338878553743666688) * 10 ^ 70 + 3943632524604715956175022966099007020126893175021346023790097589023045) * 10 ^ 70 + 8620517310633965265210589103970941182556891213647725304414331826642795

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_284 :

Polynomial.coeff recurrence4Scalar1First 284 = -((((78944671044567547080854016 * 10 ^ 70 + 4039914145850422374294014194083914815801435592029549012907105586612146) * 10 ^ 70 + 462603196909674926470101783790053733179050156765591421705494417183460) * 10 ^ 70 + 9136480999704244538562601050708168270556551237319154504564513424670062) * 10 ^ 70 + 8982840347166596594893556121955112308341506976003215472935045796692792)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_285 :

Polynomial.coeff recurrence4Scalar1First 285 = (((56507661662498909384691820 * 10 ^ 70 + 1113348862706831554648405634470706549142130160636757093621604579524979) * 10 ^ 70 + 952111780238516805422420561174032941800069256303786019038651073537511) * 10 ^ 70 + 759162657889888554420230370230514661891367495656839731135790779157822) * 10 ^ 70 + 7300899997862684537729536595448900564434740504429289828854448758793157

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_286 :

Polynomial.coeff recurrence4Scalar1First 286 = -((((39741698373589595411004315 * 10 ^ 70 + 6773292399012771264624655216908283013646912514789424342449703908947024) * 10 ^ 70 + 4651377233520670170509079951673727728258175673299294501410377284846367) * 10 ^ 70 + 4740574616455707328074021833345028846663444634346073199019527717153720) * 10 ^ 70 + 6103954311411598013264361113983753941657711227350920586435016269678753)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_287 :

Polynomial.coeff recurrence4Scalar1First 287 = (((27460704564745356942929200 * 10 ^ 70 + 3782025934735008140382031009857887020253714274845815826960413950377452) * 10 ^ 70 + 2877712014789091375716532082271454525243569091623667573956200716042969) * 10 ^ 70 + 1888505758807129847126650041937206057422883506494152824535882153812425) * 10 ^ 70 + 7931840547311423879891487758171653231987804929061648727371364819265908

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_288 :

Polynomial.coeff recurrence4Scalar1First 288 = -((((18639800349729924913472983 * 10 ^ 70 + 1488019585633064714863755252222884298910809271898008931111395046018810) * 10 ^ 70 + 8444616731163645891151136024848999042378727450202026812373925516202678) * 10 ^ 70 + 8900903056509611233082901911868419830776307608991502248795591349952304) * 10 ^ 70 + 4339954648808277214445206416490671727250850422030873740777197506156014)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_289 :

Polynomial.coeff recurrence4Scalar1First 289 = (((12426188010183527642590478 * 10 ^ 70 + 39903990764093521935736732510397532757968920581370921790432011474485) * 10 ^ 70 + 9372326903466517973771386119231251360765510633565194854214381288509802) * 10 ^ 70 + 7638925752843869749390508470349522874019776042500530161382795813443114) * 10 ^ 70 + 8380490978964987483122530781056861508564378199915673654630164671631817

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_290 :

Polynomial.coeff recurrence4Scalar1First 290 = -((((8133271692311188444688827 * 10 ^ 70 + 2729833751813076299161265472179885046078144522995155103079317906813492) * 10 ^ 70 + 9626494643232917480472375137617180498885588925435086409415281208456954) * 10 ^ 70 + 5913581393832190011413259280242913995222206055151764775383269816814387) * 10 ^ 70 + 3697543648922756449707166511748418506471560253446720912942010973509801)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_291 :

Polynomial.coeff recurrence4Scalar1First 291 = (((5224466017160060352961439 * 10 ^ 70 + 2319271775727791504888334267941875898320751867369180609729952210317328) * 10 ^ 70 + 3848817417047728614488889815918495696071813230975437204892192098260976) * 10 ^ 70 + 7614902200150632526568360229573214738081422060685737151410018695793652) * 10 ^ 70 + 6327265587049759593144520218804900378924780758323405086046567672983423

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_292 :

Polynomial.coeff recurrence4Scalar1First 292 = -((((3291793765441587661290302 * 10 ^ 70 + 8313066624932919707981069483950074236699068084410875748868575066675203) * 10 ^ 70 + 5628491665110680769552023472946134947545305387090996769577465886503030) * 10 ^ 70 + 4535777727457016365522863778117992274110677237143857063532331323276761) * 10 ^ 70 + 7648757164984744902435060080688568745360049257445566443425378766910291)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_293 :

Polynomial.coeff recurrence4Scalar1First 293 = (((2032992805351442166858686 * 10 ^ 70 + 1868084893697887630026537016609071551201071426256133020623587793324782) * 10 ^ 70 + 8517275079251543914928058618677143565654041723294762773035044487711137) * 10 ^ 70 + 3510350414734121988358322136077278674982562878597534662485202649150498) * 10 ^ 70 + 5048158490847532403739682540821547134278370438946207183172308610464176

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_294 :

Polynomial.coeff recurrence4Scalar1First 294 = -((((1229604291363470668698055 * 10 ^ 70 + 9552805197682235682741853993266528622623950493183618579558126168464368) * 10 ^ 70 + 8723104000643993847935681283291668195055854355897541960853564200494310) * 10 ^ 70 + 4817500882423378742001749826660807379598501128890593794352519134775318) * 10 ^ 70 + 876803551644322553271379247178898464456042002140572344591160607564885)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_295 :

Polynomial.coeff recurrence4Scalar1First 295 = (((727484248721387282641918 * 10 ^ 70 + 1670183343607696748838326048104669449430487366166391464813416175628014) * 10 ^ 70 + 8218180256946265570068085386942988626821401429633929971209913977643286) * 10 ^ 70 + 4231940573331485555771873996312796720292451771677213343185857203557533) * 10 ^ 70 + 5686119656162041227291387133235022754596163623132961150775228081903518

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_296 :

Polynomial.coeff recurrence4Scalar1First 296 = -((((420398732061647471668414 * 10 ^ 70 + 4349326778161946057150911248933505889721833774641485380039400390905199) * 10 ^ 70 + 9391843232517610994627297642915437945513176781035475376803366255977139) * 10 ^ 70 + 8883920303439646915540953431492919415940556434229576999721438091679015) * 10 ^ 70 + 5571525838493471011614463616106290045671898707615925779513712110531401)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_297 :

Polynomial.coeff recurrence4Scalar1First 297 = (((236818781874342583739950 * 10 ^ 70 + 3873949814107541913204771040420568976602820734723476219122567837458765) * 10 ^ 70 + 4128143480637004499152151619730532020008217269815743592020809278568944) * 10 ^ 70 + 8813253874686036274938550076585283779086703943804850310396577856415102) * 10 ^ 70 + 6892177820698014902602764722026742603858052564598916053899374921176675

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_298 :

Polynomial.coeff recurrence4Scalar1First 298 = -((((129691606445164724574510 * 10 ^ 70 + 4733324259104657827195262091521354064631944575902867372911104364966235) * 10 ^ 70 + 5944396454830366484424660790928656213298132034907876988501499898123695) * 10 ^ 70 + 1152748170452099280134229054102926658062746427635442341429974518351104) * 10 ^ 70 + 702790378554098503024831472968770469854016852202769116573549079890133)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_299 :

Polynomial.coeff recurrence4Scalar1First 299 = (((68784452382539713840562 * 10 ^ 70 + 4855062449233500509449394045857396017031480120678745688232061331376024) * 10 ^ 70 + 9723585932293729095194818332011957446781855278117991087872778913207550) * 10 ^ 70 + 8823705036047839314208039184221856927725560585672231742825679226604400) * 10 ^ 70 + 8753015675753772462584510757941639896572393153710757178953053304955078

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_300 :

Polynomial.coeff recurrence4Scalar1First 300 = -((((35132208926544517734297 * 10 ^ 70 + 2604801951329116138067157300532858178035678738105621223542782672382733) * 10 ^ 70 + 2544147439658607354339116475867784186685573494976685214270578255609884) * 10 ^ 70 + 3921084710466837261224640886125229750672667574683108665552502419045846) * 10 ^ 70 + 5260961602694617180446443543687799223078729047328637771085021764021596)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_301 :

Polynomial.coeff recurrence4Scalar1First 301 = (((17128682204192677849599 * 10 ^ 70 + 1717146935087341646379322643399297476371603267075616449139456319789567) * 10 ^ 70 + 2572770846683266053880937106172185989392902879987894712138646980161937) * 10 ^ 70 + 9885289449466457665638508770071896865560403777563156707154273088127268) * 10 ^ 70 + 6788063735720891502725641740519660860560464986216072539398106707937933

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_302 :

Polynomial.coeff recurrence4Scalar1First 302 = -((((7852433903617639693260 * 10 ^ 70 + 2531306555571487512083079523417873359652782140068891749963799373791199) * 10 ^ 70 + 6087791775255957289746106678754983119917141340587543300331826818703859) * 10 ^ 70 + 6508260448549362892890791044728807693275152574942661545420882030852035) * 10 ^ 70 + 8295762199663625210059385971147470598092347296300982010810825682304989)