Recurrence 4 lookup certificate: Scalar0Exceptional 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.recurrence4Scalar0Exceptional_coeff_161 :
Polynomial.coeff recurrence4Scalar0Exceptional 161 = -(((4576659579864059634418084040224647223288765356366562081240263696962670 * 10 ^ 70 + 3319029951064647928931341367993406025879018810622801649793683121053069) * 10 ^ 70 + 4514578839030622973805748462968482185185176347108875917244650106575856) * 10 ^ 70 + 6678051748822202571643210457642678918336426120502615241305725535477991)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_162 :
Polynomial.coeff recurrence4Scalar0Exceptional 162 = (((1 * 10 ^ 70 + 9755119356675351595992077101960928664213486548533834413364746144280612) * 10 ^ 70 + 4887765414485358541229969647437089969490413443499053805983164796020223) * 10 ^ 70 + 3053728751114012944358526074275212544642338346777858968320594496210981) * 10 ^ 70 + 5777332001673341606423184937042325130448546445327331293529783828758856
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_163 :
Polynomial.coeff recurrence4Scalar0Exceptional 163 = -((((8 * 10 ^ 70 + 3296143803615177598791296912620958871276833376801866478407777033499169) * 10 ^ 70 + 9403763304977043847957565259799600572675050138225246094790861878608630) * 10 ^ 70 + 4474506397299848889725249882653014541594033055299970802131599469692741) * 10 ^ 70 + 6185778670499816710643184406705998870978396371097231056435645092534084)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_164 :
Polynomial.coeff recurrence4Scalar0Exceptional 164 = (((34 * 10 ^ 70 + 3381392349616735266487912978896749243550533659299786035576461135194353) * 10 ^ 70 + 8771108537589435983079894850364737302787060684135867065359275145671329) * 10 ^ 70 + 8513018685971361743474142120600077336299119537513565357854764291619767) * 10 ^ 70 + 6431481385156843311549351153475802869977709933967884077614326533246132
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_165 :
Polynomial.coeff recurrence4Scalar0Exceptional 165 = -((((138 * 10 ^ 70 + 5058646094276538239706260518333599113505837965568122144558447749498004) * 10 ^ 70 + 5983644873303424232260722470115853622279564771863662682688249048053299) * 10 ^ 70 + 5970712992094096522670718980120981391417010090545464974158452151616932) * 10 ^ 70 + 1623438408883423785378173394561925755080270590434287650973385541801040)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_166 :
Polynomial.coeff recurrence4Scalar0Exceptional 166 = (((546 * 10 ^ 70 + 9974518999449069271637046819180184170650798285311034896529466999361953) * 10 ^ 70 + 2363030212003235625918658956605602564051751660700499662802548800372482) * 10 ^ 70 + 8435962507939124096811519155546636619112644835406026739207584813088562) * 10 ^ 70 + 4031132777879367302668290255441379649222830361999075407796901489612998
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_167 :
Polynomial.coeff recurrence4Scalar0Exceptional 167 = -((((2116 * 10 ^ 70 + 2991739499818013059455053959489235443556168891683396215940966467067618) * 10 ^ 70 + 1146540084649549627073476547053422634624090260949488832706638030782597) * 10 ^ 70 + 3008243509624374254537878011624069895655033811740882908528198108008845) * 10 ^ 70 + 2964107736224412696919107245259679702582980221570562753507994518778848)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_168 :
Polynomial.coeff recurrence4Scalar0Exceptional 168 = (((8025 * 10 ^ 70 + 3152200359283994310475582545516871252196883060128566849953430444219980) * 10 ^ 70 + 5889278666529816413934258390253280473088916481314758344267710369149858) * 10 ^ 70 + 6937661182702881605036961328459672300330371198349909838479511275830872) * 10 ^ 70 + 6244989673880295881515304069400688018032974062889920338654674536378713
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_169 :
Polynomial.coeff recurrence4Scalar0Exceptional 169 = -((((29842 * 10 ^ 70 + 4357719517338655238689776295925530228113293361646618102515479005197722) * 10 ^ 70 + 4095454210211132369865158121702429134041181933148462169568050321670278) * 10 ^ 70 + 6173587716060603918675277942249316872888261575272200945458688010665087) * 10 ^ 70 + 2666394826529316206219031793946176741901060530882728167446307245402296)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_170 :
Polynomial.coeff recurrence4Scalar0Exceptional 170 = (((108859 * 10 ^ 70 + 6212695142372249188899909054741474978623929250227238238610110695149526) * 10 ^ 70 + 6287985924721175354850939582042521882452280409427840167644360349895117) * 10 ^ 70 + 5034743223711826167317773214061397046244773018785087173106988536725902) * 10 ^ 70 + 8249257123070551321363588773239770724483122069116882091317354020692436
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_171 :
Polynomial.coeff recurrence4Scalar0Exceptional 171 = -((((389686 * 10 ^ 70 + 8194821209473604359302259926738104484434646146630629673909310675831097) * 10 ^ 70 + 1069503207189379398436385239223541007445583270161850440097148640518313) * 10 ^ 70 + 8177298140066803467056204004756064591340046231200088637682370825970701) * 10 ^ 70 + 6609229559874986370435070025013262682334609542640459983871761473322838)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_172 :
Polynomial.coeff recurrence4Scalar0Exceptional 172 = (((1369374 * 10 ^ 70 + 6216061671634848639778772744928591509122609924792081309157718310474578) * 10 ^ 70 + 4998839349762050334977013364844786240745027786252739529376915987336719) * 10 ^ 70 + 3662965462353518815051379077752018052954686523145923670720886085500043) * 10 ^ 70 + 2042073106789162379249532407853128290116297332264815153946682256326402
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_173 :
Polynomial.coeff recurrence4Scalar0Exceptional 173 = -((((4725146 * 10 ^ 70 + 5818009405092635425901055495958614706776613178366723966061041510992993) * 10 ^ 70 + 5295235151710153327271880333645054640084871030196583658368911377302760) * 10 ^ 70 + 1949845388031684974471069780313641286781046262169075552305802845850879) * 10 ^ 70 + 9346722665001073191979125689232975638238871544268826058506060379768409)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_174 :
Polynomial.coeff recurrence4Scalar0Exceptional 174 = (((16014476 * 10 ^ 70 + 6842222093538707804672566171196477416421145818132687645560222671025539) * 10 ^ 70 + 5631351913784854450977735535516932413356631578116759792066154173112401) * 10 ^ 70 + 5403337099912929531804731572724305294202183583466818171697625580582714) * 10 ^ 70 + 6364017005188328741112490800412944619727713150283273214646831535965136
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_175 :
Polynomial.coeff recurrence4Scalar0Exceptional 175 = -((((53324072 * 10 ^ 70 + 4834795049952122971515661558898675035040970839809690190944738527485652) * 10 ^ 70 + 593546922771836159838102459621528177472212724525215860250515644670068) * 10 ^ 70 + 8175660252622144097223386079420405610041059557178456571533349059345979) * 10 ^ 70 + 811251354238224476071636757613434970075426032478718040213920136870048)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_176 :
Polynomial.coeff recurrence4Scalar0Exceptional 176 = (((174480707 * 10 ^ 70 + 7317671827678793705737529352957450115320910921740917029057579909683634) * 10 ^ 70 + 2347291810656688632501655407493876991104486420174230949375378470977659) * 10 ^ 70 + 293277016236665097208793113518162423391844747835245203458319408471247) * 10 ^ 70 + 5147714078566956467718293653670479440215911950228560755793893043643551
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_177 :
Polynomial.coeff recurrence4Scalar0Exceptional 177 = -((((561149161 * 10 ^ 70 + 7951092211082337257804729598160360547295823658007768733943025956129220) * 10 ^ 70 + 4376022427787733806011178641674092849815553100178530830895700704581272) * 10 ^ 70 + 680816272703938932065004068810538528878474883633604893018048202215959) * 10 ^ 70 + 4945687440407178805209940683923110607352547898647887845025386825488219)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_178 :
Polynomial.coeff recurrence4Scalar0Exceptional 178 = (((1774201370 * 10 ^ 70 + 7341897238979039281292931414166125165448462976355035564388291193147595) * 10 ^ 70 + 865650124398567078325795156965332233437285528043892814390227672835147) * 10 ^ 70 + 7851473207241904994889776372314011403092840458558136907697302212251017) * 10 ^ 70 + 7990466929452316936102116443407084390593059793211330145885524511794979
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_179 :
Polynomial.coeff recurrence4Scalar0Exceptional 179 = -((((5515722563 * 10 ^ 70 + 4428300949643702497652998671498699720090925322742424642385106386072619) * 10 ^ 70 + 9281838796433007312602730927020855213667382586784654288885582579871114) * 10 ^ 70 + 4217995614353783811392995022028078751573981499712151834232836040056341) * 10 ^ 70 + 3480079802893136601293542654723579509381448917970485156452750922023157)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_180 :
Polynomial.coeff recurrence4Scalar0Exceptional 180 = (((16863704646 * 10 ^ 70 + 152662629902056493959834936121085539027249452866808079480710089185850) * 10 ^ 70 + 8849370534934151502958257584156709717202859786398519196447190652140104) * 10 ^ 70 + 3298613989785045340474459843861276265453914786403995252963668433127571) * 10 ^ 70 + 6756520938534818156860808712197149714336927165934732237035551134797950
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_181 :
Polynomial.coeff recurrence4Scalar0Exceptional 181 = -((((50713810492 * 10 ^ 70 + 4772340863300618643697964346989107166751493262854161751055467546701298) * 10 ^ 70 + 6356108580964001631897587677523707431703299112254104858914348435311708) * 10 ^ 70 + 8174925001327616774301729104383832375700883104034556601009911084295899) * 10 ^ 70 + 9529559822765237302985661786767209776550966985509654539522151642574187)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_182 :
Polynomial.coeff recurrence4Scalar0Exceptional 182 = (((150034000181 * 10 ^ 70 + 9884811421028551263973875754637249159071162106408397827218520813186030) * 10 ^ 70 + 6735309442633134183634418011313704879310631106855138176064413140291101) * 10 ^ 70 + 2461103794406614422741283913938825039197506566656248429968791686804346) * 10 ^ 70 + 1990862637358141996389273221175981266278111788595513149271786237174133