Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar2ExceptionalPart2.Coefficients478To508

Recurrence 4 lookup certificate: Scalar2Exceptional 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.recurrence4Scalar2Exceptional_coeff_478 :

Polynomial.coeff recurrence4Scalar2Exceptional 478 = (3700104007976587403162289332514175894414601199828615895649 * 10 ^ 70 + 7664168226947464425104604683024126145448951992886451121442792079772025) * 10 ^ 70 + 7980069573165569996536042781680063399307449247148179148248960622421524

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

Polynomial.coeff recurrence4Scalar2Exceptional 479 = (187795939698423271368133467800132167984175340348209797902 * 10 ^ 70 + 8620208060561975298100660811225124238622971521671744320475539691836181) * 10 ^ 70 + 5250933974722235598473510900110269418390521581264627128001507147811236

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

Polynomial.coeff recurrence4Scalar2Exceptional 480 = (3940952815331820245159083216226140733306885791246516143 * 10 ^ 70 + 3920172913250871242919656934540610547201869283386463910377431983738256) * 10 ^ 70 + 9945013056318272905930159399172943663545144672757476106921908978705947

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

Polynomial.coeff recurrence4Scalar2Exceptional 481 = (52205562230586854348993749165377108583621494053663439 * 10 ^ 70 + 8156881604145512177727156516612444520313618010956273805489645427961470) * 10 ^ 70 + 1038920531479687119255042922201359051560891166776925737254014860179042

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

Polynomial.coeff recurrence4Scalar2Exceptional 482 = (482274361289914300270959672796185300704893084172091 * 10 ^ 70 + 8790288873594275456881593022708492145357734855070159185021090037817704) * 10 ^ 70 + 1010175001583247430480998184148609869941029625212655593934253739997747

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

Polynomial.coeff recurrence4Scalar2Exceptional 483 = (3205502472787648406817642472868867605917416852513 * 10 ^ 70 + 1255952950855199585764971697166836499346762039400909149779918812676117) * 10 ^ 70 + 2999579360534726339004465339246118846240726367701827049914044220303316

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

Polynomial.coeff recurrence4Scalar2Exceptional 484 = (15229717517413733342166038789464879419730321887 * 10 ^ 70 + 2303180700679467332005337112860903491484212730199164236149112465055462) * 10 ^ 70 + 783838847610022727753572176148874284983016523442584458136358515717279

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

Polynomial.coeff recurrence4Scalar2Exceptional 485 = (48717797521415440783411879190641751043170778 * 10 ^ 70 + 9262849393540865772854067258252185716369404775625903617858043722138358) * 10 ^ 70 + 960342220793856481409364708410118452290314400351681843431318306393391

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

Polynomial.coeff recurrence4Scalar2Exceptional 486 = (81015681900430381409152198222791822300668 * 10 ^ 70 + 1391125331924889528158734268832486652449775751937734217399803810819907) * 10 ^ 70 + 7390289218057278706023592673066363776874933414380256387574905153324759

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

Polynomial.coeff recurrence4Scalar2Exceptional 487 = -((83486965873656452391848860488288239837 * 10 ^ 70 + 7937243828257480572498676013340203485543183914091128780008101144994519) * 10 ^ 70 + 2509266986387132742521634759822153308762305941886764952438475103873584)

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

Polynomial.coeff recurrence4Scalar2Exceptional 488 = -((895234397739870999879757038425953777 * 10 ^ 70 + 7909535175289065931360376386760481415837374401660317896520979948641188) * 10 ^ 70 + 5901954198780199959409492139506000743361303289247719272827115040052681)

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

Polynomial.coeff recurrence4Scalar2Exceptional 489 = -((2353375725216896066535339898822551 * 10 ^ 70 + 5751173060130620272044950762126380422876020973394367532150033193468545) * 10 ^ 70 + 5932182292946389625588615068959617067828243444875407916819788683132106)

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

Polynomial.coeff recurrence4Scalar2Exceptional 490 = -((2158204655384406585968350924644 * 10 ^ 70 + 5330166034663474191735012138751761526458091275132687999509221602330906) * 10 ^ 70 + 7797283180350414201687258300385493052561839895138144613305853128701634)

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

Polynomial.coeff recurrence4Scalar2Exceptional 491 = (4155988359667983651302624229 * 10 ^ 70 + 9327801884298354641342784138451854695144295897426127699000315603485105) * 10 ^ 70 + 8457411957122135617760269164201305206041483143210754271058517969458625

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

Polynomial.coeff recurrence4Scalar2Exceptional 492 = (16122313938381690012051114 * 10 ^ 70 + 7799950801803917176293952061406721586666394660627223185821497973433434) * 10 ^ 70 + 3302824501911069784986134074786493083845367389402222303422562721407767

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

Polynomial.coeff recurrence4Scalar2Exceptional 493 = (20679462089242362071853 * 10 ^ 70 + 2237749373569195876203406275226677395447560495796236956925570837183743) * 10 ^ 70 + 658052944348515576683890959253518488619840070605046319167649944059436

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

Polynomial.coeff recurrence4Scalar2Exceptional 494 = (3003192581880532401 * 10 ^ 70 + 4360647949462903116683503286030461690190245707552904434322994611528966) * 10 ^ 70 + 9244577705606871405975678092096749009848719461448885337546534421662012

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

Polynomial.coeff recurrence4Scalar2Exceptional 495 = -((29219318098292994 * 10 ^ 70 + 9179459753321804663727488103467728967089149247883586248553202708675855) * 10 ^ 70 + 7685389136821775341892588196349268481131875646706339841860524557348227)

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

Polynomial.coeff recurrence4Scalar2Exceptional 496 = -((48431306376437 * 10 ^ 70 + 2283769290573312152668479785546733720000127347561927948426983843218091) * 10 ^ 70 + 1092067608987915176577828771211707783839254153332594583940364926006716)

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

Polynomial.coeff recurrence4Scalar2Exceptional 497 = -((41406852700 * 10 ^ 70 + 7241017889814287103774173346528444627671859666299124785780666173538285) * 10 ^ 70 + 3238736330354254586777545749954306947221995301507089641117893088935700)

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

Polynomial.coeff recurrence4Scalar2Exceptional 498 = -((22049789 * 10 ^ 70 + 7134523172812476720251767135305799904998334709268414952991047087384993) * 10 ^ 70 + 4252205652643652074330086297922120741095783282180521970933866498755932)

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

Polynomial.coeff recurrence4Scalar2Exceptional 499 = -((7635 * 10 ^ 70 + 8516995789679819980715514692341580812293876142135128038364709210703216) * 10 ^ 70 + 8625749437456804252331162242010824284765882892518849306421363516407942)

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

Polynomial.coeff recurrence4Scalar2Exceptional 500 = -((1 * 10 ^ 70 + 7311927657638091806818494925863663915155193099909672026660627333181818) * 10 ^ 70 + 1730128324005727888879697912067281746217127654743920334127339565982672)

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

Polynomial.coeff recurrence4Scalar2Exceptional 501 = -(2547575562973483269854063268819670455043806199886436714623584221685 * 10 ^ 70 + 5611960015918314511381012211893756178984962954872819148354700639196198)

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

Polynomial.coeff recurrence4Scalar2Exceptional 502 = -(239039636525752956814950955449619776703455351773247987839363784 * 10 ^ 70 + 6577467902512553560227785583556241546857343224048882520706369841665656)

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

Polynomial.coeff recurrence4Scalar2Exceptional 503 = -(13948249938802240823789802690710724469862692616781879775832 * 10 ^ 70 + 6315981040083865937379362546911224886707650459846415162353144480023696)

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

Polynomial.coeff recurrence4Scalar2Exceptional 504 = -(491205909133784099876717764838648659050237784973283512 * 10 ^ 70 + 951109060622897635564740062507891354582163252664740619823239343254640)

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

Polynomial.coeff recurrence4Scalar2Exceptional 505 = -(10156209983676335293191339120868784072970031295017 * 10 ^ 70 + 1140303748912650417898970852008446531463567884939903995214317013351033)

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

Polynomial.coeff recurrence4Scalar2Exceptional 506 = -(117982370022623698058226463122888927663067836 * 10 ^ 70 + 7810044808561737680640290000986836329418694648091502541776206329062003)

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

Polynomial.coeff recurrence4Scalar2Exceptional 507 = -(719840172583233609660549940119554138033 * 10 ^ 70 + 5984716672167844580940126578627406442033105250780833449292717146451804)

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

Polynomial.coeff recurrence4Scalar2Exceptional 508 = -(2231533975049811042106771452679688 * 10 ^ 70 + 8565927105164372549662364511961454959501078854358331065549703947397611)