Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1ExceptionalPart0.Coefficients0To39

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.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_0 :
Polynomial.coeff recurrence4Scalar1Exceptional 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_1 :
Polynomial.coeff recurrence4Scalar1Exceptional 1 = 7863807291149679993597577870117009352646656
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_2 :
Polynomial.coeff recurrence4Scalar1Exceptional 2 = -65585369952137973030776642519053722462814502912
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_3 :
Polynomial.coeff recurrence4Scalar1Exceptional 3 = 213602094035798907069872632148706090165475271664512
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_4 :
Polynomial.coeff recurrence4Scalar1Exceptional 4 = -256151286573907978714623159179340362693804423166735072
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_5 :
Polynomial.coeff recurrence4Scalar1Exceptional 5 = -303555327441912774450756825390853734758323020746029086688
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_6 :
Polynomial.coeff recurrence4Scalar1Exceptional 6 = 1378264803633140828532305316462818952003048343155292463730376
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_7 :
Polynomial.coeff recurrence4Scalar1Exceptional 7 = -1575905859927531543220076487586939332447886986718618638727858392
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_8 :
Polynomial.coeff recurrence4Scalar1Exceptional 8 = -26139555887831090764656872400976619984019805101441023071622170952
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_9 :
Polynomial.coeff recurrence4Scalar1Exceptional 9 = 1978977344706207232369306006416468317370727638608381741488084704973280
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_10 :
Polynomial.coeff recurrence4Scalar1Exceptional 10 = -(233 * 10 ^ 70 + 1075246628308340418451622858589291699073123341198240320689315475539566)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_11 :
Polynomial.coeff recurrence4Scalar1Exceptional 11 = 124837 * 10 ^ 70 + 4356957940182118916634972187170271130317807997925367316709388957035318
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_12 :
Polynomial.coeff recurrence4Scalar1Exceptional 12 = -(17594161 * 10 ^ 70 + 7833599236914993163371293564110919470093178202947381855999071567803266)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_13 :
Polynomial.coeff recurrence4Scalar1Exceptional 13 = -(20962174070 * 10 ^ 70 + 5126716174518197508737156731395451406747301665122054554191077477576056)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_14 :
Polynomial.coeff recurrence4Scalar1Exceptional 14 = 17081055767507 * 10 ^ 70 + 1612717017700678145021420565016134295339501346198481801644765215427616
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_15 :
Polynomial.coeff recurrence4Scalar1Exceptional 15 = -(6810343231232760 * 10 ^ 70 + 4871704089947933006248303479387852355424606786069464410826210068200649)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_16 :
Polynomial.coeff recurrence4Scalar1Exceptional 16 = 1701847712569801238 * 10 ^ 70 + 9832348406565502158000744883386647948175515919411295581806096008993133
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_17 :
Polynomial.coeff recurrence4Scalar1Exceptional 17 = -(274374260437772883497 * 10 ^ 70 + 9898965211923329604771281255821489825245386412665049816233113987192014)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_18 :
Polynomial.coeff recurrence4Scalar1Exceptional 18 = 32870854569160369076566 * 10 ^ 70 + 1298510137545937208406095291512276291865996621953682964453276815568636
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_19 :
Polynomial.coeff recurrence4Scalar1Exceptional 19 = -(8908654785596230946301143 * 10 ^ 70 + 9778371287913298509238266615580635846180851590847232902993158440572000)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_20 :
Polynomial.coeff recurrence4Scalar1Exceptional 20 = 4800951679070295036277750725 * 10 ^ 70 + 6690176673189811299666575179213611981102202816730849660583377496748960
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_21 :
Polynomial.coeff recurrence4Scalar1Exceptional 21 = -(1989241067819580173265318028742 * 10 ^ 70 + 4804642198455257505709923852933464777368141685181855045385656840726215)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_22 :
Polynomial.coeff recurrence4Scalar1Exceptional 22 = 616449352562833567046707378832874 * 10 ^ 70 + 3291440784151618602043024258581566985391248565820001228881270455829677
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_23 :
Polynomial.coeff recurrence4Scalar1Exceptional 23 = -(154001295385416132317482297609589440 * 10 ^ 70 + 1742041679183364931097376073477264348555835576176507661197482742627827)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_24 :
Polynomial.coeff recurrence4Scalar1Exceptional 24 = 32983059285868508708905072363615612974 * 10 ^ 70 + 893922724387833512248483992447538707629187298664034991184804205835289
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_25 :
Polynomial.coeff recurrence4Scalar1Exceptional 25 = -(6488868849789877748964233978832103233484 * 10 ^ 70 + 7110894102659122180981788236523060847318517429180942689191717842183981)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_26 :
Polynomial.coeff recurrence4Scalar1Exceptional 26 = 1292426268308749843054185548531900352803760 * 10 ^ 70 + 1204205835358125692753795899911942971026177127138643927146870934746054
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_27 :
Polynomial.coeff recurrence4Scalar1Exceptional 27 = -(285873960136211531002426301884838870988012122 * 10 ^ 70 + 3771114510142434305414938326822543241151657826332412004618058756705222)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_28 :
Polynomial.coeff recurrence4Scalar1Exceptional 28 = 70386572134203829754294546380670392434318026573 * 10 ^ 70 + 2776587248909554081951449213224643718625551754308585801624792791137131
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_29 :
Polynomial.coeff recurrence4Scalar1Exceptional 29 = -(17822907461918602551435218102674656569555286172712 * 10 ^ 70 + 2200563209446191517575124689138528436851944336273460119204300275003724)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_30 :
Polynomial.coeff recurrence4Scalar1Exceptional 30 = 4319791061385120746193295905246352956009376811309355 * 10 ^ 70 + 8189190226529499578893947018229622595948374584112656511462566465251215
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_31 :
Polynomial.coeff recurrence4Scalar1Exceptional 31 = -(968781106815575974883934766570233146248277897905745849 * 10 ^ 70 + 6356069000344210583794560707234395351648847368274212303534902894838149)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_32 :
Polynomial.coeff recurrence4Scalar1Exceptional 32 = 199082504618260879576988298563807033939604454765118554424 * 10 ^ 70 + 2916391753515782914497142819394876895933287671335326019677791669015398
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_33 :
Polynomial.coeff recurrence4Scalar1Exceptional 33 = -(37497228718455318160455356795505336866799084004903561082970 * 10 ^ 70 + 2977806339127571460717384186074858645942981275512912219954979436577318)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_34 :
Polynomial.coeff recurrence4Scalar1Exceptional 34 = 6495682768542936505778210173262730857167848198803933954000304 * 10 ^ 70 + 142842581847583142120057912482783609667783767884776037086782730212256
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_35 :
Polynomial.coeff recurrence4Scalar1Exceptional 35 = -(1039114900641161191081543485019313300918061394027819801400208169 * 10 ^ 70 + 1147551470713519166024779503590421926694995320107809601425850543984497)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_36 :
Polynomial.coeff recurrence4Scalar1Exceptional 36 = 154082107180924690663319281581684249372838719872292737544659547525 * 10 ^ 70 + 8892396814715015043895085859336283360946307903906526968573042672033704
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_37 :
Polynomial.coeff recurrence4Scalar1Exceptional 37 = -(21248344628030394278381239279568132519367621506581149331729604570842 * 10 ^ 70 + 6521116074524073787395822185706459846509440102737940893500336658085384)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_38 :
Polynomial.coeff recurrence4Scalar1Exceptional 38 = 2732896445904859320498357016775374729239234554756363304899142436102485 * 10 ^ 70 + 1311179944396891228395392344293055128440815669340612113663763428781710
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_39 :
Polynomial.coeff recurrence4Scalar1Exceptional 39 = -((32 * 10 ^ 70 + 8644988984690878438945199251642656782786259446135390547693542597711000) * 10 ^ 70 + 9011391457562091824469172578361138277113400085923435966513851156301789)