Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupA0Low

Recurrence 4 lookup certificate: A0 source coefficients, low half #

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.recurrence4A0_coeff_0 :
Polynomial.coeff remainder4Coefficient0 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_1 :
Polynomial.coeff remainder4Coefficient0 1 = -480
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_2 :
Polynomial.coeff remainder4Coefficient0 2 = -1155556
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_3 :
Polynomial.coeff remainder4Coefficient0 3 = 9736172392
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_4 :
Polynomial.coeff remainder4Coefficient0 4 = -16423440806733
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_5 :
Polynomial.coeff remainder4Coefficient0 5 = 4962878559054749
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_6 :
Polynomial.coeff remainder4Coefficient0 6 = 102164852818091143
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_7 :
Polynomial.coeff remainder4Coefficient0 7 = -174570283367325557914
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_8 :
Polynomial.coeff remainder4Coefficient0 8 = 16971635485316593160253
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_9 :
Polynomial.coeff remainder4Coefficient0 9 = -1987372853128920730284497
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_10 :
Polynomial.coeff remainder4Coefficient0 10 = 1037153502365342951467098014
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_11 :
Polynomial.coeff remainder4Coefficient0 11 = -349526738997984038153494449661
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_12 :
Polynomial.coeff remainder4Coefficient0 12 = 84901689992003848492177873655587
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_13 :
Polynomial.coeff remainder4Coefficient0 13 = -16352667734463880226360448854219828
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_14 :
Polynomial.coeff remainder4Coefficient0 14 = 2565177297628097530010580556359543693
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_15 :
Polynomial.coeff remainder4Coefficient0 15 = -333800508239121059175948637360295552192
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_16 :
Polynomial.coeff remainder4Coefficient0 16 = 36587384198255758979280741147876340582674
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_17 :
Polynomial.coeff remainder4Coefficient0 17 = -3419412929303129369590936763792570525919843
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_18 :
Polynomial.coeff remainder4Coefficient0 18 = 275266221231594527722590210037775210341936415
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_19 :
Polynomial.coeff remainder4Coefficient0 19 = -19254132146361394764594199340404152527817392416
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_20 :
Polynomial.coeff remainder4Coefficient0 20 = 1179191434858326803678139570533696562234113231007
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_21 :
Polynomial.coeff remainder4Coefficient0 21 = -63662698240520829270727927863644116342844301394297
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_22 :
Polynomial.coeff remainder4Coefficient0 22 = 3048456799788126981426530242874006721063169129975568
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_23 :
Polynomial.coeff remainder4Coefficient0 23 = -130190017247630784430273724525535800743183253852586767
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_24 :
Polynomial.coeff remainder4Coefficient0 24 = 4984012111357720919132972081171726882070498470418930825
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_25 :
Polynomial.coeff remainder4Coefficient0 25 = -171833374329887690929979143920362797722934521553807165394
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_26 :
Polynomial.coeff remainder4Coefficient0 26 = 5358353641923289810316231454695640774731160930358869641301
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_27 :
Polynomial.coeff remainder4Coefficient0 27 = -151733892613902320668731059276185396977874583181787529963366
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_28 :
Polynomial.coeff remainder4Coefficient0 28 = 3916261660788291569420069376764028379928785109835567828887690
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_29 :
Polynomial.coeff remainder4Coefficient0 29 = -92448566200735918254424866746257832196092338994497115278176440
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_30 :
Polynomial.coeff remainder4Coefficient0 30 = 2002493030313663849759458446818828012981658913199308038612727636
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_31 :
Polynomial.coeff remainder4Coefficient0 31 = -39920648526267385629952858400090707042200265355834615164512062208
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_32 :
Polynomial.coeff remainder4Coefficient0 32 = 734533177819509477287413271955281502005821078427064188360344442371
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_33 :
Polynomial.coeff remainder4Coefficient0 33 = -12507452692977962651544595122820773459955498832237098200234945555742
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_34 :
Polynomial.coeff remainder4Coefficient0 34 = 197586420462991385248909542772129415135930036618213305292649025647133
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_35 :
Polynomial.coeff remainder4Coefficient0 35 = -2902680805118970352871139647271194747604401551075543746504464144683328
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_36 :
Polynomial.coeff remainder4Coefficient0 36 = 3 * 10 ^ 70 + 9742882462546483249549056718894116011316711210031170589579524649197846
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_37 :
Polynomial.coeff remainder4Coefficient0 37 = -(50 * 10 ^ 70 + 8213543483660942809957690511042854497063475878832254864470856856441634)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_38 :
Polynomial.coeff remainder4Coefficient0 38 = 608 * 10 ^ 70 + 1596189531773994598656774218130238755639278940312271766174398508850511
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_39 :
Polynomial.coeff remainder4Coefficient0 39 = -(6823 * 10 ^ 70 + 1251170549194221430846048959370653224910873577491003681983242674804801)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_40 :
Polynomial.coeff remainder4Coefficient0 40 = 71896 * 10 ^ 70 + 6819966711527633191319997714427672769795222442919773561069858031147343
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_41 :
Polynomial.coeff remainder4Coefficient0 41 = -(712718 * 10 ^ 70 + 734788483776173122298590248485379690068318915160677312771485795258676)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_42 :
Polynomial.coeff remainder4Coefficient0 42 = 6657247 * 10 ^ 70 + 6318226452339400055634241503321154514772743610266037296127378929400351
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_43 :
Polynomial.coeff remainder4Coefficient0 43 = -(58679670 * 10 ^ 70 + 1504962688268005975387631723641132508787499309238881208765493889823571)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_44 :
Polynomial.coeff remainder4Coefficient0 44 = 488776435 * 10 ^ 70 + 6956172415846479131359694355903840319106372781967595853558554161723593
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_45 :
Polynomial.coeff remainder4Coefficient0 45 = -(3852510585 * 10 ^ 70 + 8048473692569738347169218738352833697880681990998305810053119145127830)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_46 :
Polynomial.coeff remainder4Coefficient0 46 = 28769967559 * 10 ^ 70 + 9817819811918013130383649950126923852107816831092272538441039427590772
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_47 :
Polynomial.coeff remainder4Coefficient0 47 = -(203807058938 * 10 ^ 70 + 9069762039019664301648459371411587297439357768324093667918080645561781)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_48 :
Polynomial.coeff remainder4Coefficient0 48 = 1371130542823 * 10 ^ 70 + 1842150721098517967175393927491905839555583700223202166366631931175344
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_49 :
Polynomial.coeff remainder4Coefficient0 49 = -(8769768194628 * 10 ^ 70 + 9105807251357786741769827395230528932397345372402484534391047643844940)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_50 :
Polynomial.coeff remainder4Coefficient0 50 = 53381790827567 * 10 ^ 70 + 4244154274601007747366021648075638082852107911194677131652075737508590
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_51 :
Polynomial.coeff remainder4Coefficient0 51 = -(309540294753858 * 10 ^ 70 + 5033099372090542674237766588514053969279928818230534685864177133740893)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_52 :
Polynomial.coeff remainder4Coefficient0 52 = 1711441805490243 * 10 ^ 70 + 8397519695720582822022519525971149838281963279609161536387956405258181
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_53 :
Polynomial.coeff remainder4Coefficient0 53 = -(9030453049377010 * 10 ^ 70 + 3620101117270949708545493980196735893640531383917728158851069683150107)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_54 :
Polynomial.coeff remainder4Coefficient0 54 = 45511561886060662 * 10 ^ 70 + 8553333617391812603464342608246166234748804523050039435189284774870618
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_55 :
Polynomial.coeff remainder4Coefficient0 55 = -(219251642291040787 * 10 ^ 70 + 2546647733459784922820530093342100581728221553390189056035548213512656)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_56 :
Polynomial.coeff remainder4Coefficient0 56 = 1010414829029634936 * 10 ^ 70 + 2283908739166724087704574373383161256071197687769597165541031327709355
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_57 :
Polynomial.coeff remainder4Coefficient0 57 = -(4457616723382702318 * 10 ^ 70 + 8518894610137196556102341442606011929362970079119588195173611977297505)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_58 :
Polynomial.coeff remainder4Coefficient0 58 = 18838517245440986277 * 10 ^ 70 + 5320928688992881194800991872511702208729285651243929385941262443449604
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_59 :
Polynomial.coeff remainder4Coefficient0 59 = -(76315313516479787827 * 10 ^ 70 + 487081249516218809357606793885905185697080587464127738372814506070245)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_60 :
Polynomial.coeff remainder4Coefficient0 60 = 296526529348733163435 * 10 ^ 70 + 6514481098165307147414227312137481883543218630922227684358011914044149
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_61 :
Polynomial.coeff remainder4Coefficient0 61 = -(1105744495845591294834 * 10 ^ 70 + 3451132212385177366427028184281029405798960565992519866788614800313472)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_62 :
Polynomial.coeff remainder4Coefficient0 62 = 3959360916770984161287 * 10 ^ 70 + 5668367333964400645450168642981072450884470728478364009850981211642567
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_63 :
Polynomial.coeff remainder4Coefficient0 63 = -(13620780618649545980279 * 10 ^ 70 + 8469776891798179807115206150951316824482253717518633592867227313520635)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_64 :
Polynomial.coeff remainder4Coefficient0 64 = 45040315567274952965738 * 10 ^ 70 + 8294970071399877035643832432403887454354070337430932295112130830313719
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_65 :
Polynomial.coeff remainder4Coefficient0 65 = -(143228097551643054824078 * 10 ^ 70 + 7360685991333606995870890418040370088772968605232965571361190818481826)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_66 :
Polynomial.coeff remainder4Coefficient0 66 = 438204356006963667507926 * 10 ^ 70 + 1864273863292663309525678202294020243495815297457351575563856528955031
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_67 :
Polynomial.coeff remainder4Coefficient0 67 = -(1290419905869442014791300 * 10 ^ 70 + 2055337689149965597070498041553523859646916044207133608455447943182640)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_68 :
Polynomial.coeff remainder4Coefficient0 68 = 3659029743257642554173431 * 10 ^ 70 + 3703542967885994882804159830157614429159295750921710533045770572200706
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_69 :
Polynomial.coeff remainder4Coefficient0 69 = -(9994172003593366337249813 * 10 ^ 70 + 393434495052939879097110689110456733259243015996342669675310581726471)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_70 :
Polynomial.coeff remainder4Coefficient0 70 = 26304523612370033332620224 * 10 ^ 70 + 1222276478139228171605858045872634574646230975847957516258788819253348
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_71 :
Polynomial.coeff remainder4Coefficient0 71 = -(66736779679105242612865764 * 10 ^ 70 + 7397358923161793929807087608621757958188620872711622496208474733738499)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_72 :
Polynomial.coeff remainder4Coefficient0 72 = 163264507017518134829938958 * 10 ^ 70 + 6100282371851994185173758914013947766367631473503207541146652703706981
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_73 :
Polynomial.coeff remainder4Coefficient0 73 = -(385250397682266060202427579 * 10 ^ 70 + 7396905920202973374952255110301229417905034462509235067536187545336222)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_74 :
Polynomial.coeff remainder4Coefficient0 74 = 877091984276516223227301912 * 10 ^ 70 + 4387112897031501232801110196746143832608541889317368905923470646429335
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_75 :
Polynomial.coeff remainder4Coefficient0 75 = -(1927157339764645003404952377 * 10 ^ 70 + 4069805214443417921045820575471479795673355117669686817980778705336467)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_76 :
Polynomial.coeff remainder4Coefficient0 76 = 4087635345459265407174635325 * 10 ^ 70 + 2011761206551094466884283436548995692673741422330711364913473563022175
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_77 :
Polynomial.coeff remainder4Coefficient0 77 = -(8371766913620828787959910483 * 10 ^ 70 + 5979783516743203546100704133730428311642677841407368228542824643915721)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_78 :
Polynomial.coeff remainder4Coefficient0 78 = 16559748070657190043871716709 * 10 ^ 70 + 2873868588425133217945142839705385257873302472610580920491864676236682
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_79 :
Polynomial.coeff remainder4Coefficient0 79 = -(31643063151446146386796436921 * 10 ^ 70 + 1734007882908553377210873176861967450746453660487280130324779305991769)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_80 :
Polynomial.coeff remainder4Coefficient0 80 = 58422955704673838967458698942 * 10 ^ 70 + 5286503992202649592295700271467845383405589067730884314802796419221016
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_81 :
Polynomial.coeff remainder4Coefficient0 81 = -(104245350404801167085685149183 * 10 ^ 70 + 6046783238729668669918728026912986730319386108799459887279014661430814)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_82 :
Polynomial.coeff remainder4Coefficient0 82 = 179796993080558260279221420551 * 10 ^ 70 + 9726183815259852306846432403121341581982543255244029577645818851102548
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_83 :
Polynomial.coeff remainder4Coefficient0 83 = -(299807251954072261914729804788 * 10 ^ 70 + 2938088605495066869607672772121056283087993811986285799753660362653895)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_84 :
Polynomial.coeff remainder4Coefficient0 84 = 483409145599314153751582281516 * 10 ^ 70 + 8559116475769210647365984170274552135866004812089852982002266574616115
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_85 :
Polynomial.coeff remainder4Coefficient0 85 = -(753837843977681520130181780029 * 10 ^ 70 + 5257363152098877430929499147574127452158415629080105222878627891864087)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_86 :
Polynomial.coeff remainder4Coefficient0 86 = 1137123612057692598698166959408 * 10 ^ 70 + 5091881950338239364148960747191751043145516771316495505414257686275768
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_87 :
Polynomial.coeff remainder4Coefficient0 87 = -(1659511180917703076843649613660 * 10 ^ 70 + 1354035617988662097854306777358389486319929179861922897531904994712005)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_88 :
Polynomial.coeff remainder4Coefficient0 88 = 2343538817729134368586086315801 * 10 ^ 70 + 4217509406710843707448067969711269422730069772867397172527579584838613
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_89 :
Polynomial.coeff remainder4Coefficient0 89 = -(3203035692233677543034133103024 * 10 ^ 70 + 1874977438200640368750943377662360960292298586530160463215722583094871)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_90 :
Polynomial.coeff remainder4Coefficient0 90 = 4237694964683749202580834028176 * 10 ^ 70 + 4096857003286494351749937598679970524384770531354898743124571380337277
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_91 :
Polynomial.coeff remainder4Coefficient0 91 = -(5428251177393272613659067103500 * 10 ^ 70 + 2367731630701682637915427707867611227462934180490392126657667907456342)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_92 :
Polynomial.coeff remainder4Coefficient0 92 = 6733501330921963449621335284059 * 10 ^ 70 + 831169268238333365854208720695242677616955345460937655564127570790800
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_93 :
Polynomial.coeff remainder4Coefficient0 93 = -(8090335925998022791172332624737 * 10 ^ 70 + 5723645827954556020065494930868880071322246256098357069024863089937147)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_94 :
Polynomial.coeff remainder4Coefficient0 94 = 9417526337652128650606095425680 * 10 ^ 70 + 5252053637563917256893966150918698930726744782687970421882795126710194
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_95 :
Polynomial.coeff remainder4Coefficient0 95 = -(10623288182008538018950764289458 * 10 ^ 70 + 2680511849680788815987080183305030182321984418912169171700587559320275)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_96 :
Polynomial.coeff remainder4Coefficient0 96 = 11615761123617550949379524258951 * 10 ^ 70 + 7880995149843237303543704997412073003272616028623079441523364974052631
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A0_coeff_97 :
Polynomial.coeff remainder4Coefficient0 97 = -(12314749793561964620939811485050 * 10 ^ 70 + 2545943268794009388989703572599402961954287641389455918284558198443425)