Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupB1Low

Recurrence 2 lookup certificate: B1 source coefficients, low half #

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.recurrence2B1_coeff_0 :
Polynomial.coeff remainder3Coefficient1 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_1 :
Polynomial.coeff remainder3Coefficient1 1 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_2 :
Polynomial.coeff remainder3Coefficient1 2 = 790
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_3 :
Polynomial.coeff remainder3Coefficient1 3 = 13593174
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_4 :
Polynomial.coeff remainder3Coefficient1 4 = -3143765912
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_5 :
Polynomial.coeff remainder3Coefficient1 5 = 22224431529139
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_6 :
Polynomial.coeff remainder3Coefficient1 6 = -9581546513540763
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_7 :
Polynomial.coeff remainder3Coefficient1 7 = 3625768004123046781
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_8 :
Polynomial.coeff remainder3Coefficient1 8 = -736427900725824578076
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_9 :
Polynomial.coeff remainder3Coefficient1 9 = 103602730525610362262883
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_10 :
Polynomial.coeff remainder3Coefficient1 10 = -9720000525951758301319245
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_11 :
Polynomial.coeff remainder3Coefficient1 11 = 641384061688276159506992347
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_12 :
Polynomial.coeff remainder3Coefficient1 12 = -29807610346047288542981828167
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_13 :
Polynomial.coeff remainder3Coefficient1 13 = 1011993514928827874626255085507
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_14 :
Polynomial.coeff remainder3Coefficient1 14 = -27588785382850700761419492527289
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_15 :
Polynomial.coeff remainder3Coefficient1 15 = 778856192928799753253598015152603
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_16 :
Polynomial.coeff remainder3Coefficient1 16 = -26284968749545126326416226531774290
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_17 :
Polynomial.coeff remainder3Coefficient1 17 = 838677187750941599932471485344008670
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_18 :
Polynomial.coeff remainder3Coefficient1 18 = -19840159097813206912112856692962029068
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_19 :
Polynomial.coeff remainder3Coefficient1 19 = 283995824988650272088359232893564919176
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_20 :
Polynomial.coeff remainder3Coefficient1 20 = -200658286951553508779688024152928626651
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_21 :
Polynomial.coeff remainder3Coefficient1 21 = -120919132753601655772668751345790687120650
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_22 :
Polynomial.coeff remainder3Coefficient1 22 = 4455966837412600171978384930666283132335687
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_23 :
Polynomial.coeff remainder3Coefficient1 23 = -120077005830542256214571792357570834586972659
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_24 :
Polynomial.coeff remainder3Coefficient1 24 = 2902315697149986652200100169000154423713480755
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_25 :
Polynomial.coeff remainder3Coefficient1 25 = -64526473845662151335844662172009059089429794440
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_26 :
Polynomial.coeff remainder3Coefficient1 26 = 1290617704867752262141072773114910620724348839175
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_27 :
Polynomial.coeff remainder3Coefficient1 27 = -22794729084532014995478647727817834396948459520021
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_28 :
Polynomial.coeff remainder3Coefficient1 28 = 353315556448081185199307400698484199360270721194167
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_29 :
Polynomial.coeff remainder3Coefficient1 29 = -4812880786691912788110047237084103655447978586593530
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_30 :
Polynomial.coeff remainder3Coefficient1 30 = 57878291146815460358092129376595562590210734151862692
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_31 :
Polynomial.coeff remainder3Coefficient1 31 = -617737352359349426905107435023724165392922381504137923
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_32 :
Polynomial.coeff remainder3Coefficient1 32 = 5882473491592880845864414439966373119811884720514047408
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_33 :
Polynomial.coeff remainder3Coefficient1 33 = -50225332563756226781419166424600265060827872658557808475
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_34 :
Polynomial.coeff remainder3Coefficient1 34 = 386197339368419763052534094787306808064088847892188612625
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_35 :
Polynomial.coeff remainder3Coefficient1 35 = -2684385573847498095843446412228192123945573443457869640978
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_36 :
Polynomial.coeff remainder3Coefficient1 36 = 16915745887002034351475883518944567198214998221214373419499
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_37 :
Polynomial.coeff remainder3Coefficient1 37 = -96824403862890422932058276712182234587757995442593103229009
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_38 :
Polynomial.coeff remainder3Coefficient1 38 = 503844983252797470837528502548084963562855064376136786810227
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_39 :
Polynomial.coeff remainder3Coefficient1 39 = -2382798511493624516680177675176011018883559732018875565761936
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_40 :
Polynomial.coeff remainder3Coefficient1 40 = 10223013125965829245523948751685394125642246592829054736465168
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_41 :
Polynomial.coeff remainder3Coefficient1 41 = -39627501507429808811790196833806911471089677385973947886850912
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_42 :
Polynomial.coeff remainder3Coefficient1 42 = 137616328417704194525298358145366065885753892096244508687775525
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_43 :
Polynomial.coeff remainder3Coefficient1 43 = -420617832937282719549932530428156073690217654863162183515867533
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_44 :
Polynomial.coeff remainder3Coefficient1 44 = 1086688077016891640040404719916952250758001709002929849819100269
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_45 :
Polynomial.coeff remainder3Coefficient1 45 = -2117045900378094450302394180197976052020697874866389261529290053
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_46 :
Polynomial.coeff remainder3Coefficient1 46 = 1573873370402300220999391826761829897204425586926558504077729681
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_47 :
Polynomial.coeff remainder3Coefficient1 47 = 10644311786833732656582735778162373125475408995102187543542544923
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_48 :
Polynomial.coeff remainder3Coefficient1 48 = -71136715030969184183854200060725777190148445001450823149086923021
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_49 :
Polynomial.coeff remainder3Coefficient1 49 = 292069722490930185310853946295842046672642764572343504310414030087
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_50 :
Polynomial.coeff remainder3Coefficient1 50 = -993393455921345980841725671678556174931105337591928892889947841542
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_51 :
Polynomial.coeff remainder3Coefficient1 51 = 3023085324759856524499293283672137920340087897186076737631493632750
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_52 :
Polynomial.coeff remainder3Coefficient1 52 = -8104447679923438559902964456472011977417072409659123493088766295176
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_53 :
Polynomial.coeff remainder3Coefficient1 53 = 17068731288293475113119521168870069874789814003682746242005916945360
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_54 :
Polynomial.coeff remainder3Coefficient1 54 = -19928043604410636555449239072426940875229149351481373517789242548598
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_55 :
Polynomial.coeff remainder3Coefficient1 55 = -13406571249791003147339517709710462822381192608530851772516857429164
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_56 :
Polynomial.coeff remainder3Coefficient1 56 = 16337173046674659333592019656472193136943084993896137745116502038120
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_57 :
Polynomial.coeff remainder3Coefficient1 57 = 788244571679145887294001151407222542857474774728122808576916171988427
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_58 :
Polynomial.coeff remainder3Coefficient1 58 = -4720544453607848933345905252674414508285957488103489946389986149675376
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_59 :
Polynomial.coeff remainder3Coefficient1 59 = 1 * 10 ^ 70 + 541615416793286959116889447018063695759759247843859465082481202079933
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_60 :
Polynomial.coeff remainder3Coefficient1 60 = 1 * 10 ^ 70 + 9057956045469880482016929997469405733565450970846524356670318413745663
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_61 :
Polynomial.coeff remainder3Coefficient1 61 = -(22 * 10 ^ 70 + 9234680572595593158202990957944906398901149263780505360321775093890590)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_62 :
Polynomial.coeff remainder3Coefficient1 62 = 78 * 10 ^ 70 + 833008966444051047835542198098936282536197180909773443671782123198606
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_63 :
Polynomial.coeff remainder3Coefficient1 63 = -(63 * 10 ^ 70 + 4880177846232697069663772185982670415648143436134681720696102204307272)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_64 :
Polynomial.coeff remainder3Coefficient1 64 = -(652 * 10 ^ 70 + 7460295408561257167332988789855457353847879369243876202961901336308128)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_65 :
Polynomial.coeff remainder3Coefficient1 65 = 3660 * 10 ^ 70 + 3393159720128532642111962270836208076149013765143528862926056211777128
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_66 :
Polynomial.coeff remainder3Coefficient1 66 = -(9202 * 10 ^ 70 + 9916592950937771569915357495182546134341107195158563384457280187594141)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_67 :
Polynomial.coeff remainder3Coefficient1 67 = 2391 * 10 ^ 70 + 6344032483543070847613672697816675629296352215354705655717478907851007
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_68 :
Polynomial.coeff remainder3Coefficient1 68 = 83439 * 10 ^ 70 + 7404747305773033159661648892678823750538762615391283413824994843324864
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_69 :
Polynomial.coeff remainder3Coefficient1 69 = -(399630 * 10 ^ 70 + 3655923177312452137471167100825147480661468764582415270062702396828521)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_70 :
Polynomial.coeff remainder3Coefficient1 70 = 1014452 * 10 ^ 70 + 6130743151480975052942590838687807536124908615956530007344433566950721
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_71 :
Polynomial.coeff remainder3Coefficient1 71 = -(951000 * 10 ^ 70 + 9682626456726579735199708352255118508295802156374570801873286903511519)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_72 :
Polynomial.coeff remainder3Coefficient1 72 = -(4562026 * 10 ^ 70 + 3581110809638804385783434895481376722178741641478022374645621764749733)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_73 :
Polynomial.coeff remainder3Coefficient1 73 = 28645249 * 10 ^ 70 + 2630542240220701359832941097694136397329407855152621898353506403112908
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_74 :
Polynomial.coeff remainder3Coefficient1 74 = -(93011432 * 10 ^ 70 + 3269042709597186787827597165949689489156861307830371574582153217620640)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B1_coeff_75 :
Polynomial.coeff remainder3Coefficient1 75 = 199686410 * 10 ^ 70 + 6811636042452265558222841452121479111209476815590003680762080409656459