Recurrence 4 lookup certificate: Scalar1Exceptional 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.recurrence4Scalar1Exceptional_coeff_272 :
Polynomial.coeff recurrence4Scalar1Exceptional 272 = (((2886786394452517511269673636 * 10 ^ 70 + 6101779730743934553211880964864347717165377678059591537580586461868332) * 10 ^ 70 + 5025686815356174866119059470908994551146313823051553755518590424800449) * 10 ^ 70 + 5089586821214009318989902026402176849532156557350142580804846383080320) * 10 ^ 70 + 6085575626965306501663937642813847445501692095668818312071984904417297
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_273 :
Polynomial.coeff recurrence4Scalar1Exceptional 273 = -((((2382987929810189974973572612 * 10 ^ 70 + 6862564322332312888653581838359436799312169271249285944903741430424062) * 10 ^ 70 + 7848692327383338023611707619758994880317133989718486203674739131777649) * 10 ^ 70 + 8790069455447257919522882176482366679538393020232547723336362536213625) * 10 ^ 70 + 2634065680971924452467393004185613713471102860154916234788263488523481)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_274 :
Polynomial.coeff recurrence4Scalar1Exceptional 274 = (((1940938195184930130235869961 * 10 ^ 70 + 1217404231527164639084569588518062309466594785668067105945237410874366) * 10 ^ 70 + 6069098791820482182993582423136732016894142939497042068992749025568455) * 10 ^ 70 + 4365223735617051036422266035374670636272586384872509135298762606089638) * 10 ^ 70 + 405411617133510889321734326794001313004972669370990125666097542554930
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_275 :
Polynomial.coeff recurrence4Scalar1Exceptional 275 = -((((1559768003755490772797985087 * 10 ^ 70 + 4716370298888193943572767542633906392178824290587343196965344714730427) * 10 ^ 70 + 3739242218583233478913321426727660357024480340960160525642806804655046) * 10 ^ 70 + 199495842546629475744058889244386639919457123033892557659398248688123) * 10 ^ 70 + 9829042167949378151019436758349945788081711459549739955731531825842033)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_276 :
Polynomial.coeff recurrence4Scalar1Exceptional 276 = (((1236628692016876795504727740 * 10 ^ 70 + 753411803555617241525845960329256750019563726611519581529162119244567) * 10 ^ 70 + 3142855319335701211828024152178417194065521856857053032239269557154578) * 10 ^ 70 + 9950666628246730058843880689892986152434793067311270304518988399176879) * 10 ^ 70 + 5743709378469364757275795188408751470594144996216805253931442703524055
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_277 :
Polynomial.coeff recurrence4Scalar1Exceptional 277 = -((((967205236007632606069762082 * 10 ^ 70 + 6006606937927781917564211157146984412122186142091725304728488025106328) * 10 ^ 70 + 2566458366211668151220098051429092656700865116318109196295489105025093) * 10 ^ 70 + 827742509578706930423876684587846402105082813555770289737114583021737) * 10 ^ 70 + 2912392421007867551621487837530362952474978799448871206971091541125184)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_278 :
Polynomial.coeff recurrence4Scalar1Exceptional 278 = (((746213269880396009228623704 * 10 ^ 70 + 2370967895679497446999273464576924295028063222480921885066077522463065) * 10 ^ 70 + 237954001625103104463997230910465776194769631115831934614534779724928) * 10 ^ 70 + 9805629022224784958765952725032821165172183842150557994710361632021336) * 10 ^ 70 + 9688199345658081033816000093447579470641589468444349166486313813270937
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_279 :
Polynomial.coeff recurrence4Scalar1Exceptional 279 = -((((567848976678702289811016716 * 10 ^ 70 + 3707556165705034674743341487723242018532495258889247057112457813042664) * 10 ^ 70 + 4722128470727362388618010738208720853903207514288661904073634045649555) * 10 ^ 70 + 1811013345366263216559833917990173886932520393230359277984703869377278) * 10 ^ 70 + 4825262443335962554612683145803936850992367967697819332429961883775195)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_280 :
Polynomial.coeff recurrence4Scalar1Exceptional 280 = (((426170975167561055775561184 * 10 ^ 70 + 8900605440553241551632648718434022189376103401894177171381786000340689) * 10 ^ 70 + 8652585302787524723347415019170524226781710578270100390883441545326907) * 10 ^ 70 + 7185716568020602400530172150134679592996107617469157884350424083632822) * 10 ^ 70 + 7054515223978273719770522897438607115771422697964383463515905682722066
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_281 :
Polynomial.coeff recurrence4Scalar1Exceptional 281 = -((((315403237737375234234310351 * 10 ^ 70 + 4157848481237866673361776347716810895750163360745937725080770034738075) * 10 ^ 70 + 3485836882728784909797841250546430499505076485163558376290684012775104) * 10 ^ 70 + 3996890888706191042954077698150994234628149677256848304531841591807254) * 10 ^ 70 + 5941682936534170348373431018323038702161702617860731431877803081285157)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_282 :
Polynomial.coeff recurrence4Scalar1Exceptional 282 = (((230156789407359884171792158 * 10 ^ 70 + 3831094857256645480845442761565901294207123474334192878265109188300019) * 10 ^ 70 + 507705865338907230797278514837139573386304922373027314197512299544974) * 10 ^ 70 + 6125541816989855793807598754412839569389767627623610988517150222025035) * 10 ^ 70 + 8626223536955063826652538434546000402724229950210195344833020159263206
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_283 :
Polynomial.coeff recurrence4Scalar1Exceptional 283 = -((((165574847059039672624271723 * 10 ^ 70 + 1172405195093565129119058816560041405139471131095578201277909898333986) * 10 ^ 70 + 8644957395592516042737602753426033177387451202528387741745545646790907) * 10 ^ 70 + 3239828236827810351498753150495718440060203273888429526801418719513475) * 10 ^ 70 + 1596562719596022203712372390828428071856608127944808812336040155352367)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_284 :
Polynomial.coeff recurrence4Scalar1Exceptional 284 = (((117410892677976932103802303 * 10 ^ 70 + 5849671967004169375272000741639168160073321156686788239060188348235208) * 10 ^ 70 + 2328653064591585575855492772627538989112383766196407499410786719770414) * 10 ^ 70 + 3469334159291377075724630020187671037265890711669589632713889346542370) * 10 ^ 70 + 4585067065544773874666243919833070928455336659516165353085115638588465
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_285 :
Polynomial.coeff recurrence4Scalar1Exceptional 285 = -((((82051959973399954653520105 * 10 ^ 70 + 9610664094632798850977740827384584520274888647077147740579453316575592) * 10 ^ 70 + 5255889208456260803689760409580031700623144359978174396926062003103419) * 10 ^ 70 + 8449193890143174791650271038331070171552851259707864430759492158401308) * 10 ^ 70 + 2776765369485178289813349764972500871788390162243859909829542860292652)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_286 :
Polynomial.coeff recurrence4Scalar1Exceptional 286 = (((56500394858633526335557916 * 10 ^ 70 + 1289212333834263718267691318130954932169063010455016109447527219837919) * 10 ^ 70 + 1260247869520619809423691996643574280419600754666357227596321397385132) * 10 ^ 70 + 881254112235692593684427977282064009177708403702192845362598991530316) * 10 ^ 70 + 6270450556542945723557500923059323001792739237977504712069031443065316
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_287 :
Polynomial.coeff recurrence4Scalar1Exceptional 287 = -((((38326905688224403272316512 * 10 ^ 70 + 9571452207088992899894382156379840699774698870255334809056195387128058) * 10 ^ 70 + 2634312888781321227871092294507467632805990174191836532657438325865868) * 10 ^ 70 + 1865809261398052056021505458971918926870705559368183277816496951852972) * 10 ^ 70 + 4296942421780720105342032269964987864729767800635434336163065637345613)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_288 :
Polynomial.coeff recurrence4Scalar1Exceptional 288 = (((25606281265794995906576127 * 10 ^ 70 + 7484671850128436548124652776392974247173782325814870394004845365408303) * 10 ^ 70 + 7988197601117923789720249200130010303791694604787358293796848387776361) * 10 ^ 70 + 3866078855406933747986176476901026659089220178746885527882573120912232) * 10 ^ 70 + 4814065477836037458100817383902715475421585663677324184546011211808086
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_289 :
Polynomial.coeff recurrence4Scalar1Exceptional 289 = -((((16845143496264682846585136 * 10 ^ 70 + 1313041301848823006081876228394865339884420917905247088867418688319562) * 10 ^ 70 + 4229043526074643112944801459902242122932303513663640839853005782996807) * 10 ^ 70 + 3114884921122859271284992977200127388186355747178045973101233167807900) * 10 ^ 70 + 3591451670447629875320501741754910925488023237153918538603318298113507)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_290 :
Polynomial.coeff recurrence4Scalar1Exceptional 290 = (((10908878666099753629683235 * 10 ^ 70 + 6370543130463232542519536173664251716612963150661718112668842952828329) * 10 ^ 70 + 8427806994015595006857091619160596452845152078155048852941276987004090) * 10 ^ 70 + 1065251122282346625551016735505071580960647941138303160308512382061069) * 10 ^ 70 + 8866415199053918361017557701384494117849293202085338138064835093412427
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_291 :
Polynomial.coeff recurrence4Scalar1Exceptional 291 = -((((6952734196277086843873731 * 10 ^ 70 + 9339020255860401851595309429414268177840080378833976845346606056108042) * 10 ^ 70 + 7702111960267394122350546849362907622829512707286548094506442803129220) * 10 ^ 70 + 4732242162127946341906974617517757427395748263178235807291580106460114) * 10 ^ 70 + 7533115527483898051682789711678239961510994131175460336829426129218996)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_292 :
Polynomial.coeff recurrence4Scalar1Exceptional 292 = (((4360162537191147566894993 * 10 ^ 70 + 2788511421968802394339985588980415246029825033797141769698635758613601) * 10 ^ 70 + 8874619510638065500239628237006604915629955536345771005199471570341104) * 10 ^ 70 + 9830892673620386447702936342647430432391547094862491617886577787078747) * 10 ^ 70 + 3920670459910449032648945849234352033082978028194976538591084466777107
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_293 :
Polynomial.coeff recurrence4Scalar1Exceptional 293 = -((((2689942070645429578062251 * 10 ^ 70 + 1604235319697502118123111188192650141414333045787186550165618474927683) * 10 ^ 70 + 3693904851390380079786701170362981609851127867441069143000636714554142) * 10 ^ 70 + 5869573254216804976980324050598476791887170675979130916386338027589917) * 10 ^ 70 + 8108643719654892655306347787977068656143473444811493030463700323278581)