Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupScalar1LeftPart1.Coefficients306To329

Recurrence 5 lookup certificate: Scalar1Left coefficient convolution #

This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_306 :
Polynomial.coeff recurrence5Scalar1Left 306 = -((((1378207091754196579590459637035754282713798098399469912320557 * 10 ^ 70 + 248005650189340187569706441523647457313430890626748397236561422748020) * 10 ^ 70 + 7199763468603672429414371139261174806067971749393632674970189206293427) * 10 ^ 70 + 1924595967222232157929350839778788347746032656065513947851525158128358) * 10 ^ 70 + 6383330185491807641095418515078057660092457330195149567128133894505852)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_307 :
Polynomial.coeff recurrence5Scalar1Left 307 = (((1974454214555040627532777705097489669620088288613134128329937 * 10 ^ 70 + 5666113777545568472416255910940415028323013111862960786702119354455383) * 10 ^ 70 + 4137791923623993478269352275377491935881349492944617108212307715700092) * 10 ^ 70 + 2447806826640068165787347224261601643234070607082853406894249462796602) * 10 ^ 70 + 2524468541373975275777728877190975376010604686853815338417056609031777
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_308 :
Polynomial.coeff recurrence5Scalar1Left 308 = -((((1450729725418397169804220675238564145255613499416066090185855 * 10 ^ 70 + 3472512019702186786584789986695108040400963720605154322023582206749490) * 10 ^ 70 + 6200043592489712811975651599102033996723054264799407070612166988956130) * 10 ^ 70 + 7537471955195951479780794828519841225832324207199015824679697430182507) * 10 ^ 70 + 5482154609999840367294215492394470127062683568873070476639301529069733)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_309 :
Polynomial.coeff recurrence5Scalar1Left 309 = (((855703301204149643729306669880631034970003684531521573146381 * 10 ^ 70 + 4932795568157412660954503204959628815793408325088585485940835427037168) * 10 ^ 70 + 5477305203586153481897118141700881820518721498873295036640322598746835) * 10 ^ 70 + 2013002295810843846247706217406782234935628625722271376740718987162770) * 10 ^ 70 + 2467780922808392441213160303620110441717020207004510903620661433906841
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_310 :
Polynomial.coeff recurrence5Scalar1Left 310 = -((((443790074535435720084494197361584890965118755610827655029022 * 10 ^ 70 + 2438543927763735058887405436917087385085384718249875628886472095153363) * 10 ^ 70 + 9724510570873830141537308154620327639512031476478811508111162640188714) * 10 ^ 70 + 8913429934740656207198056029136182761361931038808578026534745613879135) * 10 ^ 70 + 7437522901996624912167812656486102557541071671483393564627012425951018)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_311 :
Polynomial.coeff recurrence5Scalar1Left 311 = (((208973385784183754209655078506653062547934970594841308766777 * 10 ^ 70 + 8820131847678744224580871027239746599983325236230210222691778224913928) * 10 ^ 70 + 8250853302945970497703356259204183135483381346012087552918488946791666) * 10 ^ 70 + 9481741792508248000428035136685456092418239901462128459327941230345245) * 10 ^ 70 + 1813811097665923491370162318740616986458385588271369661723301972339805
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_312 :
Polynomial.coeff recurrence5Scalar1Left 312 = -((((90415767478513818269526424687891084452957592835608767858215 * 10 ^ 70 + 988903067611121579795889827324075891308284512071241127573453683103097) * 10 ^ 70 + 8922692660323482053397137180229262635943803371825478514824640629174158) * 10 ^ 70 + 6646029252549318610919589033301359245567885696390706559063007469036126) * 10 ^ 70 + 2057791909447573089655471327982906316097737079927852302696663458914545)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_313 :
Polynomial.coeff recurrence5Scalar1Left 313 = (((35984903955221497912636495488244696715561693768501512446797 * 10 ^ 70 + 1442234191910124215598207783228788469923716610011558265274390595360689) * 10 ^ 70 + 6425970084731621110757402225543497167169065962121446802518095197654394) * 10 ^ 70 + 9558509467636814640054170762788367676520941856147552897047196969499002) * 10 ^ 70 + 9800122272394233558806045740020356195370105387659261796534855935194640
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_314 :
Polynomial.coeff recurrence5Scalar1Left 314 = -((((13065012022536162726406840019914786665285444249719207758126 * 10 ^ 70 + 2261232586564237399493601161921787870001517009834985590794790914531691) * 10 ^ 70 + 3949701622852855881115945763438643643931698554184017941869426964451722) * 10 ^ 70 + 2736099025120354565925422372324680078033091801338537864815907997793582) * 10 ^ 70 + 3497467140739233062719192072654377428303982506740073699108448777623787)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_315 :
Polynomial.coeff recurrence5Scalar1Left 315 = (((4234347959630293650296446610374373433681618191223015916301 * 10 ^ 70 + 4606033783604242529160993489934300373465887012101465419888921069723178) * 10 ^ 70 + 4197986735251927383444878159708931003621125195790399999289843211584865) * 10 ^ 70 + 8146269245330863090301023849724955742153688814910679781315199912943820) * 10 ^ 70 + 5722356027250113681438676197996370867280089624750477894916587271274092
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_316 :
Polynomial.coeff recurrence5Scalar1Left 316 = -((((1165161055961261708565838717406081149734318315185066608087 * 10 ^ 70 + 7352469939590328183777132962104125921582525110449031923670352045628590) * 10 ^ 70 + 9620097763614075715031663908594846088815362264039742496599921511559453) * 10 ^ 70 + 237956414834122922795276349087943670161222397728453155133147280884404) * 10 ^ 70 + 5821132711147603519044965774151057621055939539228911167695871849664293)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_317 :
Polynomial.coeff recurrence5Scalar1Left 317 = (((236228280230848152387132890983409632425312629009280831842 * 10 ^ 70 + 5483473330304049909812975338376500335617752766637565691654438935584284) * 10 ^ 70 + 1820117119000185272751444754183694452678891389086063433117658541101478) * 10 ^ 70 + 8747446431771425723291252826445155530279718250002949185949111547686656) * 10 ^ 70 + 7419506163859017000067132493921832347884575254504702693607902654895906
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_318 :
Polynomial.coeff recurrence5Scalar1Left 318 = -((((13314716498157949721292114574078620239805541018190597779 * 10 ^ 70 + 7436374943216673476130584920132701219980375137900590031299930007553766) * 10 ^ 70 + 1326589164527734606847982487858860612280550716583318190266061813879605) * 10 ^ 70 + 5979840838770407427488370654650605744919287132923427982218818127159359) * 10 ^ 70 + 8176610690735698784048887867583570791040204561380305718988176153807155)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_319 :
Polynomial.coeff recurrence5Scalar1Left 319 = -((((14554534841556585898491018177400443681176494789233817960 * 10 ^ 70 + 6851709996634407448240474054153052556543005707595077635278852501737117) * 10 ^ 70 + 3479560767490580501651377547156781698431352980944641230094082964038496) * 10 ^ 70 + 7659806391506173513493150494034322156558948353876144153652371935411317) * 10 ^ 70 + 9738452333125507934142242413764991944398786222977249490543847735411641)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_320 :
Polynomial.coeff recurrence5Scalar1Left 320 = (((5383361366846296414431795926069713142729503601041413389 * 10 ^ 70 + 5988080559637849635805750608724929240260434745734652685954032027127558) * 10 ^ 70 + 6156761838044088967502889130750535474904145961135762598127143030779559) * 10 ^ 70 + 6115749824911506906268856720487135926391115411170944190905626092536366) * 10 ^ 70 + 4427956068113611609451141240976462251958641880060328165316529015289920
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_321 :
Polynomial.coeff recurrence5Scalar1Left 321 = (((2565257491298982346136656388595391760323138053373846649 * 10 ^ 70 + 7073484022124578702876642674518348479593739208524861751799877535488094) * 10 ^ 70 + 4701025059775966106926114903689561476911964604001812595560544790321607) * 10 ^ 70 + 7250773160903364531250379475716473050941409190651419590245151313503592) * 10 ^ 70 + 7583947633812200410806028172911579558894460348162357697741978306530059
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_322 :
Polynomial.coeff recurrence5Scalar1Left 322 = -((((5075100537862379209502160947482610629272943182990117257 * 10 ^ 70 + 7562629444935154480375550839378271196710259062720800897483803621105076) * 10 ^ 70 + 7650511773428090791399546189032811953861231147499944706434246822564581) * 10 ^ 70 + 1703663307324846546640154131327572199982959901231084621842173553033789) * 10 ^ 70 + 6046636342689486381729256705380941730788614787553471629319469356926588)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_323 :
Polynomial.coeff recurrence5Scalar1Left 323 = (((4575596334944438932507132947879805085283008454056506730 * 10 ^ 70 + 9539067289379851237480003890530652762094856143673619106358792545392744) * 10 ^ 70 + 989189545471408344452690297432736319405041923693780089110650567925786) * 10 ^ 70 + 3972723557757430095464545203283599329331271075284437681133898364969225) * 10 ^ 70 + 1583423235488198771924913507158432718881511138183295409258368194813225
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_324 :
Polynomial.coeff recurrence5Scalar1Left 324 = -((((3205808800077067169396435231937583851986579361292641064 * 10 ^ 70 + 7782198449465477456999297484392022584709112811257587559665555449265166) * 10 ^ 70 + 688257864293164072750160933544219391428332136542106916742559421598940) * 10 ^ 70 + 7394131012260721367618701647454314573594607145195997522258541519838226) * 10 ^ 70 + 9461963678180048897455176082712666913512102735753621020785412548498823)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_325 :
Polynomial.coeff recurrence5Scalar1Left 325 = (((1953972900084399973797998182103844734849785500854804920 * 10 ^ 70 + 8872492909447023301126937591493203274248017009341105337763059852337002) * 10 ^ 70 + 6437925779746759694726955976557133181518687692786947238471712607816704) * 10 ^ 70 + 8930078089518556566410229684791717861002307936769418332602585976203031) * 10 ^ 70 + 8975785030089856303301866450329530928358038822627595932320847898787267
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_326 :
Polynomial.coeff recurrence5Scalar1Left 326 = -((((1083926748606048133783584879366020621454949621616129355 * 10 ^ 70 + 3432957452044197626381268215343906609158715623604795334140684569841251) * 10 ^ 70 + 972544531292556374127057141919630972169193342140121148770620031863473) * 10 ^ 70 + 9341986242492892910904934502031132130746378867175736202837007602937431) * 10 ^ 70 + 5211806439570861489147455233564738001737495304778805472762495670476141)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_327 :
Polynomial.coeff recurrence5Scalar1Left 327 = (((559922127412954271406548777427564198509569936389663116 * 10 ^ 70 + 4680423172824734884836716417906825624554120435195389852351715503156338) * 10 ^ 70 + 169185470634047024062616584424028467412201521259584503533394288622049) * 10 ^ 70 + 1169366574797821828002497215967356332081556380896273699587403770129651) * 10 ^ 70 + 2934705683180675046669305281700992927890317846470137671655307211195682
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_328 :
Polynomial.coeff recurrence5Scalar1Left 328 = -((((272898739331745300992940940271687717344716531534780692 * 10 ^ 70 + 5095977656064333054821979352219937799020120081167861697381151105162287) * 10 ^ 70 + 6060928351647134602412374506228701209756529682800612362158583745985704) * 10 ^ 70 + 3001163639713365180028207738742003812617853430459499878780807936782085) * 10 ^ 70 + 318924586325856367128332547154347375465022006889843863390431589351057)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_329 :
Polynomial.coeff recurrence5Scalar1Left 329 = (((126503213888170250538553284129385953131405346582055303 * 10 ^ 70 + 4261800603540364278850862028618285485349316829712075133364088564899615) * 10 ^ 70 + 9610326224588985118291118772922418522591582444483794090179674449579895) * 10 ^ 70 + 9583140730431717228681709035302633893319033961971929138490978325727746) * 10 ^ 70 + 4545950440970170458741819715586910764936158351311132023766033833484493