Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupB2A4Part1.Coefficients216To245

Recurrence 4 lookup certificate: B2A4 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.recurrence4B2A4_coeff_216 :

Polynomial.coeff recurrence4B2A4 216 = -((63762994325171324934031074669622217433832829585118447881 * 10 ^ 70 + 1198825374972891139972808578273562253776471072438123000896862451525340) * 10 ^ 70 + 2098955694890801747927878536393824525663089908290179057437363324536159)

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

Polynomial.coeff recurrence4B2A4 217 = (41502983888800793785550937926167715717379405223032860458 * 10 ^ 70 + 8467241192931725889510030297106515620055008177526646455338243552762411) * 10 ^ 70 + 867241935540039163327899575438770833055558736794510513633354871690618

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

Polynomial.coeff recurrence4B2A4 218 = -((25244755845665170679788638357588337786960783102689842832 * 10 ^ 70 + 5911207050510025927839034129482920201069197897233236799153200149838344) * 10 ^ 70 + 3677123890118641656015394765896434325355823030350658614877934872506738)

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

Polynomial.coeff recurrence4B2A4 219 = (14604048688918919862442960216978605667154659403179996377 * 10 ^ 70 + 9592366365161223798262914048488385373568659324905680807578359826316189) * 10 ^ 70 + 5071547162571778749820421510600136418696365344692455740723360503508960

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

Polynomial.coeff recurrence4B2A4 220 = -((8114332685945279051295836488413571033723562475324235413 * 10 ^ 70 + 4516897138284916469903134752344636426689742089603370073175777051041117) * 10 ^ 70 + 9109270809896767230660392409540033578453486845937743297639760857351881)

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

Polynomial.coeff recurrence4B2A4 221 = (4356238388947067762607737343286114040207570121712298280 * 10 ^ 70 + 1108453324433974244222238463369514958325560978684741401528798805390553) * 10 ^ 70 + 1101497502130142801203380320620556539307004722419455856297717637739382

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

Polynomial.coeff recurrence4B2A4 222 = -((2268436445978979565702508866530724519919819535981893456 * 10 ^ 70 + 2899051578997106424432564456075135576723085834678255739352866470923875) * 10 ^ 70 + 8620099083539917191273098644727683305060892138029485468599788959275866)

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

Polynomial.coeff recurrence4B2A4 223 = (1148725437671083307182298041486054707894679999503534237 * 10 ^ 70 + 1100191967825872200171306306791837645999324508789595695544462173402920) * 10 ^ 70 + 425251903105670447634334647353405419759322078649021292070642986900359

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

Polynomial.coeff recurrence4B2A4 224 = -((566682660770767732908032150644126605262178776317762135 * 10 ^ 70 + 2996285590277200240952446096869566815934428249478202236087005467309807) * 10 ^ 70 + 5405697947318428226744469965222535566854234279757948109175537609143524)

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

Polynomial.coeff recurrence4B2A4 225 = (272655583389565998237908376288739273846979690041888911 * 10 ^ 70 + 9489054227748486214535340859561449491875172924896584687676908429177744) * 10 ^ 70 + 9496052800209450450336843753526172784552275171488993865087017636912787

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

Polynomial.coeff recurrence4B2A4 226 = -((128051724423123565304599882346885955973503139442340444 * 10 ^ 70 + 6065467395405393909717268548315346783206178821198127145303130668354174) * 10 ^ 70 + 515138044564526535587721097305035048315925834140654495943804448070636)

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

Polynomial.coeff recurrence4B2A4 227 = (58731860779261278546196149926183256201799810734694468 * 10 ^ 70 + 2867462022502225333513621608411229446899513681133119129987188032136452) * 10 ^ 70 + 3133941186277582841600933760772786471410920971422310826021053597210218

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

Polynomial.coeff recurrence4B2A4 228 = -((26315080401405971966268443191972019878024094633583842 * 10 ^ 70 + 5654584820129625061582678299024290743847913790741464185882199466064471) * 10 ^ 70 + 4163757348803949726846237285181352010995459236583591834099913328357087)

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

Polynomial.coeff recurrence4B2A4 229 = (11519310247239823018855771862297490421817210116786883 * 10 ^ 70 + 1331837122137828217797209701582953660322834805619590463682867378566118) * 10 ^ 70 + 6975303444412324627564564387909511748610933161147044024459384052082377

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

Polynomial.coeff recurrence4B2A4 230 = -((4926283233120750599811424750910743310516314690545951 * 10 ^ 70 + 8369185581899224047066805209874816968262288481512816070467085873777288) * 10 ^ 70 + 8092161080309035187360010844845427758931820393058005752603839463533269)

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

Polynomial.coeff recurrence4B2A4 231 = (2057765943308283759127424238380402311042130005241214 * 10 ^ 70 + 7182536535576680352437808057795664870795532906534708173726888673561420) * 10 ^ 70 + 7000069736290190009283660943457742499585397153264207379958254233835954

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

Polynomial.coeff recurrence4B2A4 232 = -((839248380293127983492071442472265304738383403122184 * 10 ^ 70 + 3721151773763770175118892702963029277120101721480569424960402104192960) * 10 ^ 70 + 7559709914256974690638847330083355747090089151825220686274362419573397)

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

Polynomial.coeff recurrence4B2A4 233 = (333989651859483297313378539891321782390546932616894 * 10 ^ 70 + 3749235821834786154187970760826651518661927690501516498322906933747721) * 10 ^ 70 + 6135366756725766880222280470063274911057940383251612503608901626670030

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

Polynomial.coeff recurrence4B2A4 234 = -((129568414711151860000558692580389034405862927624410 * 10 ^ 70 + 3473726134307399381428943034819860364395271710786297216662078724935146) * 10 ^ 70 + 338307956456897318806039839036792069589610743500205050332047107368109)

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

Polynomial.coeff recurrence4B2A4 235 = (48923638852370445834367613592320821073534566234763 * 10 ^ 70 + 4440081947954070042984744207063471774894756091204029762227893553802376) * 10 ^ 70 + 5469773945847757798690265550867441716751016773333294466461270928835075

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

Polynomial.coeff recurrence4B2A4 236 = -((17935324950747581978607408956199163300464698855783 * 10 ^ 70 + 1498914524525570977631221981064583124720275827791631768529667975136018) * 10 ^ 70 + 923398416024730515749338488398532441754339757258072538219169590751207)

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

Polynomial.coeff recurrence4B2A4 237 = (6357156376068822616035225927468202505892584925590 * 10 ^ 70 + 5380265572536089303343053895200898866126761954466468957649532794944074) * 10 ^ 70 + 2452096188468980655391832222438235343142939829295025462235631771162871

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

Polynomial.coeff recurrence4B2A4 238 = -((2162831334483442405197190139220742659866581531971 * 10 ^ 70 + 7711284217100458581689661956243548459605873846385341330959495548923203) * 10 ^ 70 + 5749183858626830922909400285639008477543444661885025283712026736106132)

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

Polynomial.coeff recurrence4B2A4 239 = (696795581315735572272285990082205345184861018722 * 10 ^ 70 + 269873432781579962976359842936625205726480836200917756956896114852330) * 10 ^ 70 + 5397201058134585012028916743731872333284975383368875793930433705134277

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

Polynomial.coeff recurrence4B2A4 240 = -((206699569848651844214125769068088128845801699407 * 10 ^ 70 + 9477964266710408903215582779374846990714199578335837387965793690547193) * 10 ^ 70 + 1652700452874567984646285205102057945414693959563415639176696364016113)

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

Polynomial.coeff recurrence4B2A4 241 = (52629823648634770259093320626600465661492215157 * 10 ^ 70 + 695688573508184089614289463941682670115593208511690551416660458667439) * 10 ^ 70 + 3759585111427525809826302820501372767307438543258850478432226389910105

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

Polynomial.coeff recurrence4B2A4 242 = -((8740036669557649246143787883754867830340329987 * 10 ^ 70 + 6723307409795232348544457832679663908637686951238138358321094725073780) * 10 ^ 70 + 3967917430165057055063691531357120917236886639735916381616197177960936)

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

Polynomial.coeff recurrence4B2A4 243 = -((1477421557232034532221114076237048019636826293 * 10 ^ 70 + 6902440679959315185393823792946050760535300020088779666969650521192319) * 10 ^ 70 + 3624310336646687269422423008484920612276194670169684307336024866329427)

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

Polynomial.coeff recurrence4B2A4 244 = (2573954026781070862627660590849037759351125260 * 10 ^ 70 + 9073948170606756648049974924578320582063744068337401355798981951330668) * 10 ^ 70 + 7514854605656771737652942775665639450385989942009186840931447984523805

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

Polynomial.coeff recurrence4B2A4 245 = -((1808234428681322094624850059881093883117494770 * 10 ^ 70 + 6977233791209834095070691085838637651246817766084834871998621606235046) * 10 ^ 70 + 1246000128257656938635477742871657654613199437484146662420787636681977)