Recurrence 4 lookup certificate: Scalar1Left 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.recurrence4Scalar1Left_coeff_106 :
Polynomial.coeff recurrence4Scalar1Left 106 = ((3835079622278795157236889490386 * 10 ^ 70 + 2039860541009361024337538044030593332693471422385709522254614274187096) * 10 ^ 70 + 2224938527404640193263036540468645915025539673002328764089634388813707) * 10 ^ 70 + 4216301650161910008340355761660456717889071599590413322461949888112189
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_107 :
Polynomial.coeff recurrence4Scalar1Left 107 = -(((41470160009675924921391946907331 * 10 ^ 70 + 7448152629047715039569783366327566330927685096365594093628044456922395) * 10 ^ 70 + 4825188341940219665390084322931075045020036083397770675552919247963270) * 10 ^ 70 + 6927838124624072554935301563757078736342494894956094664689925775557857)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_108 :
Polynomial.coeff recurrence4Scalar1Left 108 = ((436154368793780843651788324745273 * 10 ^ 70 + 9792312517821524725084529911041320245614261232667462791705767232405615) * 10 ^ 70 + 3956393687510937429878623458380434626770456738350149409660647652817235) * 10 ^ 70 + 595579902822300032928881903203208533753205551909615890990306700759982
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_109 :
Polynomial.coeff recurrence4Scalar1Left 109 = -(((4464529112687811945148164122015098 * 10 ^ 70 + 5469450660740003829176794268129618763408810383082261032534836860723576) * 10 ^ 70 + 3450278000372993156077026385479711333090728245910051127332921993339752) * 10 ^ 70 + 2608813395443129951972047725485646304760707960106052327112541820590068)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_110 :
Polynomial.coeff recurrence4Scalar1Left 110 = ((44504335236510943139052651158525894 * 10 ^ 70 + 6171011136429891894043326534815724420078203777025898210772239957217362) * 10 ^ 70 + 2375722440889557379716482566330121050182458990339542068271053597612921) * 10 ^ 70 + 2187065545870370014478820394571172021345874272925151100164634616772014
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_111 :
Polynomial.coeff recurrence4Scalar1Left 111 = -(((432272572583619348595243494836119849 * 10 ^ 70 + 3792966885602613315541635368006402646631276152628564405878659419739683) * 10 ^ 70 + 488992807096885739740816709532517667882765026302777688553212773588685) * 10 ^ 70 + 9060807344877176660661920134298025807830902848665339594896407352769951)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_112 :
Polynomial.coeff recurrence4Scalar1Left 112 = ((4093171846637418152453439916231667452 * 10 ^ 70 + 9002166296891593184868609628501341158441495622409183473435020823087489) * 10 ^ 70 + 2626611887480184570375228390296753213859034596966123843084398427345980) * 10 ^ 70 + 3595589343164183885389881279648267889892376105357621907764789841185443
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_113 :
Polynomial.coeff recurrence4Scalar1Left 113 = -(((37801675242139679891599342630928984098 * 10 ^ 70 + 9918940972133855529890038834337736739971463508318444291741388308675896) * 10 ^ 70 + 134280666783206617885004326766469359908201278576289719530813166645035) * 10 ^ 70 + 9302678775378800421583527825225716208408850845726378735342755132328287)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_114 :
Polynomial.coeff recurrence4Scalar1Left 114 = ((340642327744769746243002239381884174384 * 10 ^ 70 + 4808666203508721525096693049183790419265332914593593195005691407525296) * 10 ^ 70 + 5414013499029866446431537868011978160510850863626010127210417932271814) * 10 ^ 70 + 3718047999389553295643459645367929887601673745811170394551187086403984
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_115 :
Polynomial.coeff recurrence4Scalar1Left 115 = -(((2996388669297270437427877512510165140842 * 10 ^ 70 + 2073615064175262391059227885770289313243257795986206521865796426315940) * 10 ^ 70 + 7004738157667288717193858594025216050435194660651384822094967890364840) * 10 ^ 70 + 5805789332798519967219972786409608958886333677222447231830621645481501)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_116 :
Polynomial.coeff recurrence4Scalar1Left 116 = ((25737975929062535169651386915765127923576 * 10 ^ 70 + 7250556940486314041426985764579873844913224002281376584975616907108586) * 10 ^ 70 + 1172334272720994117967468050975654203788961354431370656313494228601737) * 10 ^ 70 + 1549110141633992407091031175898149122658849385916136440897426068422313
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_117 :
Polynomial.coeff recurrence4Scalar1Left 117 = -(((215964621234868545802422839454733376376877 * 10 ^ 70 + 3375889616606709472882293038937503654265258740103697585295852605140711) * 10 ^ 70 + 7786788058470736159493346689654134678903656929995545222848852352151949) * 10 ^ 70 + 3750424305260077556171651464549287772440631279297615616428951443094787)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_118 :
Polynomial.coeff recurrence4Scalar1Left 118 = ((1770800578436909431545005952976755035572529 * 10 ^ 70 + 2302429922134200253286219431197489292067924012733774538274697035305980) * 10 ^ 70 + 9230413909913756202371961659826125751441214797021749338644505634696345) * 10 ^ 70 + 7308389764951727673765759054110703564073587625099271800321497882738398
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_119 :
Polynomial.coeff recurrence4Scalar1Left 119 = -(((14193020294822084098923825276194210656226439 * 10 ^ 70 + 9082108516586368648259880565890892417446683718438877930400706393870047) * 10 ^ 70 + 1186473979925427321258503007942090276568648708854545897894790702907342) * 10 ^ 70 + 6690938063076080411784153521742857674852648987870722627925859340024449)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_120 :
Polynomial.coeff recurrence4Scalar1Left 120 = ((111232226112718984638331090258019654807671963 * 10 ^ 70 + 6759788300219653010292297711626728654170295256035274540243084444282434) * 10 ^ 70 + 9674219525516788365779609959591364531211973581349290020297979141173633) * 10 ^ 70 + 9734106862934489881980795746426671500155279758250579129804335528629466
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_121 :
Polynomial.coeff recurrence4Scalar1Left 121 = -(((852635531253777267845807960412128612433912565 * 10 ^ 70 + 6703212585852615481147827875111792146174304088853285951237126518725550) * 10 ^ 70 + 5942602648746543869307843153192695142755345129887370913385858627118470) * 10 ^ 70 + 6654111895381122847998021625169971209920426117755302798981864046708951)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_122 :
Polynomial.coeff recurrence4Scalar1Left 122 = ((6394314094525898008852880701829322315755494500 * 10 ^ 70 + 3698259904034862633900349712994710663993637487616597535208309257615577) * 10 ^ 70 + 4374918784909123548936849861913115929013531891986660185018553441056100) * 10 ^ 70 + 1222871649152798107940965486939485076275709086585267435970275052915041
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_123 :
Polynomial.coeff recurrence4Scalar1Left 123 = -(((46928628049956608046392858743707474527071749001 * 10 ^ 70 + 6751991768350483394524780771388997338263132327113549539882442711087348) * 10 ^ 70 + 3962278235694753429200763145979784488159512978759740569453330501116626) * 10 ^ 70 + 4382344787020434977987390920196250459598966735213531196353290966195625)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_124 :
Polynomial.coeff recurrence4Scalar1Left 124 = ((337136669369144159151093142946320886314516552744 * 10 ^ 70 + 5523625196171564465121373529742797899521676522283582387779752207499989) * 10 ^ 70 + 3827411904067961650474667563454084072227797717148147666152936357176082) * 10 ^ 70 + 7619980515676396568328534513796276220875036672441491488393888429013476
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_125 :
Polynomial.coeff recurrence4Scalar1Left 125 = -(((2371400400640449810971259650923830759082133899271 * 10 ^ 70 + 9437501497218921091320321920164410606049899064627962511268454647335322) * 10 ^ 70 + 9830102964699212916229319282669706106644377011414494911705873823886524) * 10 ^ 70 + 517983537712433572095692070779933188385591158555662683271206131944783)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_126 :
Polynomial.coeff recurrence4Scalar1Left 126 = ((16335672462590625920652827728009518794261101514590 * 10 ^ 70 + 5355873575817386416037969610498198201769659750653412297194033109324523) * 10 ^ 70 + 6320282911847938087179088769850131376578741778125578817832793359068639) * 10 ^ 70 + 8583600515409842066002243973669035709223527814111071381173750701078242
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_127 :
Polynomial.coeff recurrence4Scalar1Left 127 = -(((110230320369379694139549570961065590106132842387873 * 10 ^ 70 + 4768806468413027688302126404524318629814781852828327788734680132961725) * 10 ^ 70 + 2031896416187248127138281301824474591505263593996146213051698404470490) * 10 ^ 70 + 9021123558292342245826372918954126201646038479791186564212090548229508)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_128 :
Polynomial.coeff recurrence4Scalar1Left 128 = ((728772892342431882562606582843696579496865295030966 * 10 ^ 70 + 3335865644290234649865702105271261127432260119349921227767799434344497) * 10 ^ 70 + 6583469126959067377932835624416123220390603894868949005475807710710416) * 10 ^ 70 + 5747070421955253865631860047279397153026918411667384756534718858471663
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_129 :
Polynomial.coeff recurrence4Scalar1Left 129 = -(((4721742406929675024896201544873164958935073377120832 * 10 ^ 70 + 5936079930676619761868362203280039571534530811966251923101873849097746) * 10 ^ 70 + 6220204709973334011496615323915055618092646056792083976174262643291642) * 10 ^ 70 + 9422578810885891790738186094710944860500988137429044242001597893686700)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_130 :
Polynomial.coeff recurrence4Scalar1Left 130 = ((29986104291563651521575262116348269091482797910919437 * 10 ^ 70 + 2280612338498031545343135827531502196276183438363487872204309482470367) * 10 ^ 70 + 3378345639557355338859458063705970520070125966616231235024725913012949) * 10 ^ 70 + 7394150545113385022486138066219529092263990995985422107859211623831542
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_131 :
Polynomial.coeff recurrence4Scalar1Left 131 = -(((186694392966148835127506720161753078981032408373576455 * 10 ^ 70 + 8417281065470185561530056812310511489325528536180190659966852670342062) * 10 ^ 70 + 6093776533539828022916790424094812974682564870479282721492519946475639) * 10 ^ 70 + 9258918181646412916872838007194831246605581223429074921290056672105396)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_132 :
Polynomial.coeff recurrence4Scalar1Left 132 = ((1139774630094335723941486416793103998446790046159043307 * 10 ^ 70 + 1405253430120350922465083137308328425514659706646205801523487001587899) * 10 ^ 70 + 7522283777973543697994851252407602639958291710337497329205434985732577) * 10 ^ 70 + 432634271172065044813783958263411513203129473734555132835229639120102
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_133 :
Polynomial.coeff recurrence4Scalar1Left 133 = -(((6824385505142687414994077822829962757270650054129607743 * 10 ^ 70 + 5898311422826293630373511546720363390616698808066726893261935810836127) * 10 ^ 70 + 6094726876796347499715607613521966091386168322908409870833660149645479) * 10 ^ 70 + 8955826260832183005959673247585167137867144086015313839765144125545041)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_134 :
Polynomial.coeff recurrence4Scalar1Left 134 = ((40081395466374212191067713293418183642428562015879421104 * 10 ^ 70 + 64794980485725012766961210569484789995225249257686326259830198620497) * 10 ^ 70 + 3721698952547640999369524941313258026213886587828656456514665882807501) * 10 ^ 70 + 9421239729053713445047156968811389060307149309094965334534932314468155