Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupLeadingSquarePart0.Coefficients0To95

Recurrence 2 lookup certificate: LeadingSquare coefficient convolution #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_0 :
Polynomial.coeff recurrence2LeadingSquare 0 = 4096
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_1 :
Polynomial.coeff recurrence2LeadingSquare 1 = -1555968
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_2 :
Polynomial.coeff recurrence2LeadingSquare 2 = 173531730192
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_3 :
Polynomial.coeff recurrence2LeadingSquare 3 = -99284860407600
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_4 :
Polynomial.coeff recurrence2LeadingSquare 4 = 1922392753113905604
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_5 :
Polynomial.coeff recurrence2LeadingSquare 5 = -1438742654696290875232
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_6 :
Polynomial.coeff recurrence2LeadingSquare 6 = 1863311887180376241076440
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_7 :
Polynomial.coeff recurrence2LeadingSquare 7 = -1034916299402820150501916880
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_8 :
Polynomial.coeff recurrence2LeadingSquare 8 = 599843957166365418574143949196
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_9 :
Polynomial.coeff recurrence2LeadingSquare 9 = -231837150853507546031805458369756
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_10 :
Polynomial.coeff recurrence2LeadingSquare 10 = 70748550007318215530341904478201924
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_11 :
Polynomial.coeff recurrence2LeadingSquare 11 = -16377455483128575823415601197313151212
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_12 :
Polynomial.coeff recurrence2LeadingSquare 12 = 3024973294940718459127631084538949238228
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_13 :
Polynomial.coeff recurrence2LeadingSquare 13 = -446439313674927150719615688839969928008852
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_14 :
Polynomial.coeff recurrence2LeadingSquare 14 = 53562293848573888568410189832336706738863545
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_15 :
Polynomial.coeff recurrence2LeadingSquare 15 = -5263628285951024367685081149476342859270224830
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_16 :
Polynomial.coeff recurrence2LeadingSquare 16 = 428418678920886674821768830626837678950757033669
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_17 :
Polynomial.coeff recurrence2LeadingSquare 17 = -29088271130254720787808348406322930881548928914024
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_18 :
Polynomial.coeff recurrence2LeadingSquare 18 = 1656098930124530654497011715217891691405298437260086
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_19 :
Polynomial.coeff recurrence2LeadingSquare 19 = -78618047501288122379065927173442983805033661057132738
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_20 :
Polynomial.coeff recurrence2LeadingSquare 20 = 3000605181584223092537705329306074589411769526567330554
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_21 :
Polynomial.coeff recurrence2LeadingSquare 21 = -78285615043618307479386608467173936895042044729004895848
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_22 :
Polynomial.coeff recurrence2LeadingSquare 22 = -72397998627720587945454512726589116106947046833913277715
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_23 :
Polynomial.coeff recurrence2LeadingSquare 23 = 176108286663937982352109677361722544863605249530646409058664
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_24 :
Polynomial.coeff recurrence2LeadingSquare 24 = -14208040997285836710944735093707236908243364347917983238286010
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_25 :
Polynomial.coeff recurrence2LeadingSquare 25 = 781193829976591951776804191692890301470387188918380576779810194
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_26 :
Polynomial.coeff recurrence2LeadingSquare 26 = -34034748746878105739823147823072336190669282113251729184687964229
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_27 :
Polynomial.coeff recurrence2LeadingSquare 27 = 1202072385797189122518701258725931151583279352612921482604713901230
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_28 :
Polynomial.coeff recurrence2LeadingSquare 28 = -32485380623456132758842202488029802249117307560793426782234383067965
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_29 :
Polynomial.coeff recurrence2LeadingSquare 29 = 470385138190939287162565606258071646786611090584086425085347097474682
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_30 :
Polynomial.coeff recurrence2LeadingSquare 30 = 1 * 10 ^ 70 + 4174417140336370287313557288715394986268578323455892420469825428678697
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_31 :
Polynomial.coeff recurrence2LeadingSquare 31 = -(157 * 10 ^ 70 + 1521662967724245987560395989198441585873520014510887910580876734621824)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_32 :
Polynomial.coeff recurrence2LeadingSquare 32 = 8306 * 10 ^ 70 + 9451137282270090890824420171278551854200274446407526052577645967124855
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_33 :
Polynomial.coeff recurrence2LeadingSquare 33 = -(332253 * 10 ^ 70 + 9554158016061556869642763499406756607254136093338406518581905913056068)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_34 :
Polynomial.coeff recurrence2LeadingSquare 34 = 10998124 * 10 ^ 70 + 9281371399504220421643476805465813176352778206521763522744160738478441
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_35 :
Polynomial.coeff recurrence2LeadingSquare 35 = -(310533145 * 10 ^ 70 + 9509604684241636551827803173825658170604041797034761636467684047037898)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_36 :
Polynomial.coeff recurrence2LeadingSquare 36 = 7552970313 * 10 ^ 70 + 5668872902576711565584354905403331773267132224554792226414494305837591
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_37 :
Polynomial.coeff recurrence2LeadingSquare 37 = -(157838935196 * 10 ^ 70 + 4110416614298779101955688842751412107648011018349341174949971136009008)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_38 :
Polynomial.coeff recurrence2LeadingSquare 38 = 2783867644641 * 10 ^ 70 + 2606688944115780958307951310019451682914898452285520552314602964468579
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_39 :
Polynomial.coeff recurrence2LeadingSquare 39 = -(39355048733997 * 10 ^ 70 + 4089450770643641977579652759776565905534424693521370475270740367031564)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_40 :
Polynomial.coeff recurrence2LeadingSquare 40 = 371488439385395 * 10 ^ 70 + 1797560907500689696481963661390335149459325194418901571297434997584338
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_41 :
Polynomial.coeff recurrence2LeadingSquare 41 = 415525739727202 * 10 ^ 70 + 2144595899215620898747273242761327052287291877986732684770834481639808
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_42 :
Polynomial.coeff recurrence2LeadingSquare 42 = -(119726167015602386 * 10 ^ 70 + 7167402319074167035040937943970632166212613896834812718667040628860743)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_43 :
Polynomial.coeff recurrence2LeadingSquare 43 = 3410558442406656267 * 10 ^ 70 + 1640755740780323600107327021860769621866059705754146812268097147138824
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_44 :
Polynomial.coeff recurrence2LeadingSquare 44 = -(66976207024820589621 * 10 ^ 70 + 7517204376090625438687623062290810287702100420304753709081527976360783)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_45 :
Polynomial.coeff recurrence2LeadingSquare 45 = 1045468359101359221290 * 10 ^ 70 + 6227317008034204717094790249760254580416355865542827550399172984074260
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_46 :
Polynomial.coeff recurrence2LeadingSquare 46 = -(13243063703683876381112 * 10 ^ 70 + 9812857944665116246287393183800426163619311333150894277629375709856202)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_47 :
Polynomial.coeff recurrence2LeadingSquare 47 = 128847130886487213506114 * 10 ^ 70 + 6223743480654962396760165095371573910313747865350881889873928365415420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_48 :
Polynomial.coeff recurrence2LeadingSquare 48 = -(698844604935277074505877 * 10 ^ 70 + 5557942277353285540859351676307529020799928070701726018598877565364633)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_49 :
Polynomial.coeff recurrence2LeadingSquare 49 = -(6178001483692798900195469 * 10 ^ 70 + 3561205526239217686734869547021225337742826553960191046565040324035458)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_50 :
Polynomial.coeff recurrence2LeadingSquare 50 = 267851265930608362766823765 * 10 ^ 70 + 6394578001481986028450203038898422013894242453235203878309199685875604
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_51 :
Polynomial.coeff recurrence2LeadingSquare 51 = -(5293275131030408333245098956 * 10 ^ 70 + 7938295791290922159723572264745581387552068367383832731706793464275358)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_52 :
Polynomial.coeff recurrence2LeadingSquare 52 = 80849762172713013140727974537 * 10 ^ 70 + 2408657650770764971171018310486937620684736365901559736667519328543010
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_53 :
Polynomial.coeff recurrence2LeadingSquare 53 = -(1058163062334017885810489986108 * 10 ^ 70 + 8422631246069707343189010792421303109252873646690103734809259666168658)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_54 :
Polynomial.coeff recurrence2LeadingSquare 54 = 12348480047993925336174065528903 * 10 ^ 70 + 576629658785834264169605042380579515051565171779052947222999944740199
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_55 :
Polynomial.coeff recurrence2LeadingSquare 55 = -(131088629799897886661737934903598 * 10 ^ 70 + 4735547557104605679105458211957155692240202532723629873693111200084158)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_56 :
Polynomial.coeff recurrence2LeadingSquare 56 = 1280895964528849715633439720128879 * 10 ^ 70 + 3842070335167895589021269134626629848765557495871873093561859475547595
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_57 :
Polynomial.coeff recurrence2LeadingSquare 57 = -(11608108126121601700947196155353258 * 10 ^ 70 + 9027267102560515145204603567953630846923225521605246441600182596520496)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_58 :
Polynomial.coeff recurrence2LeadingSquare 58 = 98080788734109460575871904037113393 * 10 ^ 70 + 1935328300102984172560685656965828206628224101546289837916468016095813
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_59 :
Polynomial.coeff recurrence2LeadingSquare 59 = -(775562526399301848020052831739815181 * 10 ^ 70 + 4480056070145193933700798181834131874030693172868273142420574193783524)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_60 :
Polynomial.coeff recurrence2LeadingSquare 60 = 5755208642294814842225106502462709405 * 10 ^ 70 + 7481072002904497817340773231477104095205509519830328031035957958364037
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_61 :
Polynomial.coeff recurrence2LeadingSquare 61 = -(40160560921477053672112120169273364271 * 10 ^ 70 + 4602529667813167330035783660880268422258899800649414838342009479546790)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_62 :
Polynomial.coeff recurrence2LeadingSquare 62 = 263915121917746405481939855001465934418 * 10 ^ 70 + 3031883341364414821796392378439863772744642306193339303348604456572772
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_63 :
Polynomial.coeff recurrence2LeadingSquare 63 = -(1634817173734795263594165501647317205063 * 10 ^ 70 + 2768600591047498267573168398937253501450434505691710306846943635469404)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_64 :
Polynomial.coeff recurrence2LeadingSquare 64 = 9550464496968238704169421669395631292718 * 10 ^ 70 + 8827345141334011721148763810645622681937071663613558398722770668755916
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_65 :
Polynomial.coeff recurrence2LeadingSquare 65 = -(52617169760471667186265357718466252878641 * 10 ^ 70 + 8528078631963464413307046195903810065285998068709299681625230119047960)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_66 :
Polynomial.coeff recurrence2LeadingSquare 66 = 273232480379004278969324189742715364743354 * 10 ^ 70 + 5013056499110798887809750099451143721809639902475992064162185050593402
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_67 :
Polynomial.coeff recurrence2LeadingSquare 67 = -(1335639133948980027770532000948988116596887 * 10 ^ 70 + 5388675293216982800472220246011483064497351373622458171126164055128418)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_68 :
Polynomial.coeff recurrence2LeadingSquare 68 = 6132460389253774123652130615339235729409714 * 10 ^ 70 + 5149048590727623313328962004695950099862341558892047890669969383745405
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_69 :
Polynomial.coeff recurrence2LeadingSquare 69 = -(26351006467404195298452453948858415151938596 * 10 ^ 70 + 8249030539384162825893376622540443472371446873781857386496782918710728)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_70 :
Polynomial.coeff recurrence2LeadingSquare 70 = 105348722951499375653161677573669830484378021 * 10 ^ 70 + 1821039288494139630098420433588270121032715645108196421537094891007055
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_71 :
Polynomial.coeff recurrence2LeadingSquare 71 = -(388028242238821340730553354727577567060511186 * 10 ^ 70 + 2707092909904867338331237487771276753641204764540033520211962492285336)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_72 :
Polynomial.coeff recurrence2LeadingSquare 72 = 1293602944528889884162709775383806669112665908 * 10 ^ 70 + 7646437120224616237950747276546660762296779643912269586766626848773691
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_73 :
Polynomial.coeff recurrence2LeadingSquare 73 = -(3763545968787821543587994856682306872716793432 * 10 ^ 70 + 5027575239949270790827054896199590020819042437338459823274508851123540)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_74 :
Polynomial.coeff recurrence2LeadingSquare 74 = 8680145385371938171972953493265924375080815283 * 10 ^ 70 + 5857867358003885750600497454234662049660523643191287019107424548657741
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_75 :
Polynomial.coeff recurrence2LeadingSquare 75 = -(9871614818651339553615707299423725501919813510 * 10 ^ 70 + 3394140211426548228484229263726621100904064815358999145692622011769644)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_76 :
Polynomial.coeff recurrence2LeadingSquare 76 = -(44347703838688118520229489247843715779380349998 * 10 ^ 70 + 5412628875549692398327822029357448022002989437309526965787755494141073)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_77 :
Polynomial.coeff recurrence2LeadingSquare 77 = 414570574233139036281256807008632706571190345195 * 10 ^ 70 + 341855366747830132604406938232013616050497798705890769374706532669588
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_78 :
Polynomial.coeff recurrence2LeadingSquare 78 = -(2158341869657888603881486360852943837414947809262 * 10 ^ 70 + 9528067030786236831608033432413046704475058723573074174575705619465384)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_79 :
Polynomial.coeff recurrence2LeadingSquare 79 = 8963401137461205672479664806541636092235091337255 * 10 ^ 70 + 4076671006342973751171401450043981375235247290542393092382503642002020
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_80 :
Polynomial.coeff recurrence2LeadingSquare 80 = -(32043166600665066719638788264208854106912935523111 * 10 ^ 70 + 7395486203109865047157114230032822927639068249024762276866432752719053)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_81 :
Polynomial.coeff recurrence2LeadingSquare 81 = 100695416808995487249058299938412708962883902964772 * 10 ^ 70 + 5794488417445331144061952556682749865155363297010050525501992912321150
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_82 :
Polynomial.coeff recurrence2LeadingSquare 82 = -(276692179424274851462595490576101049278328655088164 * 10 ^ 70 + 1354103680010779920919344092407128646384450112747943498031227235375020)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_83 :
Polynomial.coeff recurrence2LeadingSquare 83 = 640615451172545569632303348962096756149776033715726 * 10 ^ 70 + 7548128511013012587572551108297802066124054449931633764579823455606784
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_84 :
Polynomial.coeff recurrence2LeadingSquare 84 = -(1096871126778262059890297574072078631353932614293008 * 10 ^ 70 + 6771735301325154930882552431622484165421539258578449271105581702902500)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_85 :
Polynomial.coeff recurrence2LeadingSquare 85 = 447823119623887092291819753955925941593118083211088 * 10 ^ 70 + 92506850739520626849316946360800645403489043076685809798638662305704
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_86 :
Polynomial.coeff recurrence2LeadingSquare 86 = 6956120909074875926599966405556714023284254511716659 * 10 ^ 70 + 7587373399581388741157141403397718029023418573004214429138651166397446
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_87 :
Polynomial.coeff recurrence2LeadingSquare 87 = -(41733982647600763559981219919986753420194451324352158 * 10 ^ 70 + 4208882280723070258947994951781905089017738852859077927569066402981914)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_88 :
Polynomial.coeff recurrence2LeadingSquare 88 = 169377959112703663306835312213923937133674076204924796 * 10 ^ 70 + 8669955828696656174451381023929606378100445854743271606184156669242396
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_89 :
Polynomial.coeff recurrence2LeadingSquare 89 = -(576382188798410550490011273942201107887120543766037542 * 10 ^ 70 + 1697038421728060281830459005965511767574648844884788458995190312105458)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_90 :
Polynomial.coeff recurrence2LeadingSquare 90 = 1726776630082999755390513889186366453916649304148115484 * 10 ^ 70 + 3784381207204048327992502323492092713700692262487022069259266094715438
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_91 :
Polynomial.coeff recurrence2LeadingSquare 91 = -(4520227572146493299628978335520852711017801208029590965 * 10 ^ 70 + 248444835965439937760819093883945412465095007148862432379767471292748)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_92 :
Polynomial.coeff recurrence2LeadingSquare 92 = 9755994499721447375713123418267750730351600192585823690 * 10 ^ 70 + 1370841004737340201496213923559636990391813701311531225618980869413080
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_93 :
Polynomial.coeff recurrence2LeadingSquare 93 = -(14791499408283347235846431476691305374994269627289950865 * 10 ^ 70 + 6334204677044522208062552197323478487285049151377301106724255854178970)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_94 :
Polynomial.coeff recurrence2LeadingSquare 94 = 7228412933024815289000831270082507801533005704900853426 * 10 ^ 70 + 3975250301781278963066693855519379646322760042884583184057244739077729
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_95 :
Polynomial.coeff recurrence2LeadingSquare 95 = 14480952329981992621887154491045738980743143662431877221 * 10 ^ 70 + 5499130067765030638384359453607555109127628778377152000055068288504864