Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupExceptionalProductPart0

Recurrence 2 lookup certificate: ExceptionalProduct 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.recurrence2ExceptionalProduct_coeff_0 :
Polynomial.coeff recurrence2ExceptionalProduct 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_1 :
Polynomial.coeff recurrence2ExceptionalProduct 1 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_2 :
Polynomial.coeff recurrence2ExceptionalProduct 2 = -367236
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_3 :
Polynomial.coeff recurrence2ExceptionalProduct 3 = -320066172
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_4 :
Polynomial.coeff recurrence2ExceptionalProduct 4 = 726546325632
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_5 :
Polynomial.coeff recurrence2ExceptionalProduct 5 = 293748497931840
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_6 :
Polynomial.coeff recurrence2ExceptionalProduct 6 = -464414710975843852
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_7 :
Polynomial.coeff recurrence2ExceptionalProduct 7 = 53864452136449766196
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_8 :
Polynomial.coeff recurrence2ExceptionalProduct 8 = 8580322044044475318048
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_9 :
Polynomial.coeff recurrence2ExceptionalProduct 9 = -1001453366418884843606568
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_10 :
Polynomial.coeff recurrence2ExceptionalProduct 10 = -64252976984225032604588313
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_11 :
Polynomial.coeff recurrence2ExceptionalProduct 11 = 5452970601589238298142705045
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_12 :
Polynomial.coeff recurrence2ExceptionalProduct 12 = 234364405905702466757098034684
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_13 :
Polynomial.coeff recurrence2ExceptionalProduct 13 = -10831583456008651287292133283792
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_14 :
Polynomial.coeff recurrence2ExceptionalProduct 14 = -532714846177645343055757957864660
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_15 :
Polynomial.coeff recurrence2ExceptionalProduct 15 = 8187876999495614449250817161580580
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_16 :
Polynomial.coeff recurrence2ExceptionalProduct 16 = 655462633793904002454813954733517428
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_17 :
Polynomial.coeff recurrence2ExceptionalProduct 17 = 1254943686434167520935030100967300032
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_18 :
Polynomial.coeff recurrence2ExceptionalProduct 18 = -431604430997692370886068060436844971276
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_19 :
Polynomial.coeff recurrence2ExceptionalProduct 19 = -5759130543607096172110135860926818550508
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_20 :
Polynomial.coeff recurrence2ExceptionalProduct 20 = 139455335874789394051382244505329667376498
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_21 :
Polynomial.coeff recurrence2ExceptionalProduct 21 = 3832676783471946320679822029723045573855560
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_22 :
Polynomial.coeff recurrence2ExceptionalProduct 22 = -10361801064580706182287348275790192104357274
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_23 :
Polynomial.coeff recurrence2ExceptionalProduct 23 = -1241133528661695456966297010467235357473406188
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_24 :
Polynomial.coeff recurrence2ExceptionalProduct 24 = -8336013200853651481157214035047331126217786224
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_25 :
Polynomial.coeff recurrence2ExceptionalProduct 25 = 219766367495676034433559725442115466829645150974
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_26 :
Polynomial.coeff recurrence2ExceptionalProduct 26 = 3350547321296009101461884977055609408352809866324
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_27 :
Polynomial.coeff recurrence2ExceptionalProduct 27 = -15671492776784366117862057166505053487802614760230
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_28 :
Polynomial.coeff recurrence2ExceptionalProduct 28 = -653853008246548467203894962436503424735444345739462
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_29 :
Polynomial.coeff recurrence2ExceptionalProduct 29 = -1669107412922621511183069451092319398596471171290566
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_30 :
Polynomial.coeff recurrence2ExceptionalProduct 30 = 76769740752737525756169103484344860861448719813644719
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_31 :
Polynomial.coeff recurrence2ExceptionalProduct 31 = 611460189620752895913540969883175876842161412110398055
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_32 :
Polynomial.coeff recurrence2ExceptionalProduct 32 = -5517963228067169191289274706169170522476232483488244689
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_33 :
Polynomial.coeff recurrence2ExceptionalProduct 33 = -86325214978043221947437868116250845948823825918570161983
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_34 :
Polynomial.coeff recurrence2ExceptionalProduct 34 = 151143706355058743306980491546291952167591967094064241618
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_35 :
Polynomial.coeff recurrence2ExceptionalProduct 35 = 7998617371108576359967507365059461863986472312980998358368
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_36 :
Polynomial.coeff recurrence2ExceptionalProduct 36 = 16074338672650160990198592499503640428494909878081203046756
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_37 :
Polynomial.coeff recurrence2ExceptionalProduct 37 = -536566015595370252368194826012537429588602445028342825188526
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_38 :
Polynomial.coeff recurrence2ExceptionalProduct 38 = -2695168151331901135135417541265380450499938991112532667180766
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_39 :
Polynomial.coeff recurrence2ExceptionalProduct 39 = 27053083693333196854760042837152451500730060821000440806073410
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_40 :
Polynomial.coeff recurrence2ExceptionalProduct 40 = 227709230781144031353179555547601143071269686408217307801312501
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_41 :
Polynomial.coeff recurrence2ExceptionalProduct 41 = -1006880818712974624959799323030566991273474193270998827493683331
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_42 :
Polynomial.coeff recurrence2ExceptionalProduct 42 = -14017139639256106867352550309066383600060086814430277992385815633
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_43 :
Polynomial.coeff recurrence2ExceptionalProduct 43 = 24423140247470161044550549161331275664112238919786188312934930987
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_44 :
Polynomial.coeff recurrence2ExceptionalProduct 44 = 693269486216798461042119947394830875480048225958416689677407198556
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_45 :
Polynomial.coeff recurrence2ExceptionalProduct 45 = -78607444671217781145927345181450305385976261764762533653667880804
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_46 :
Polynomial.coeff recurrence2ExceptionalProduct 46 = -28942120752221119530208836225732924349667112231940773036924630743853
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_47 :
Polynomial.coeff recurrence2ExceptionalProduct 47 = -28670640541775414514497327493362329549653840313889590302088579814633
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_48 :
Polynomial.coeff recurrence2ExceptionalProduct 48 = 1053189151656227946905877737195340657120845365791854701988202090459744
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_49 :
Polynomial.coeff recurrence2ExceptionalProduct 49 = 1848672307114596625622773663470838921741823118673852382128625451972936
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_50 :
Polynomial.coeff recurrence2ExceptionalProduct 50 = -(3 * 10 ^ 70 + 4238504622762320631545766898075064358161833380722524169134905083307382)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_51 :
Polynomial.coeff recurrence2ExceptionalProduct 51 = -(7 * 10 ^ 70 + 6737701699620924854239376231166016443445272835624928053131374791938532)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_52 :
Polynomial.coeff recurrence2ExceptionalProduct 52 = 101 * 10 ^ 70 + 3804516520198809766426517839361923322890771393422285007446553548135950
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_53 :
Polynomial.coeff recurrence2ExceptionalProduct 53 = 249 * 10 ^ 70 + 2568898441810445993097849386336078543546325161264972178007859325751454
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_54 :
Polynomial.coeff recurrence2ExceptionalProduct 54 = -(2772 * 10 ^ 70 + 7937563601633934802066951637527271535668279367939559965003700168726169)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_55 :
Polynomial.coeff recurrence2ExceptionalProduct 55 = -(6675 * 10 ^ 70 + 1304309640768173553864473582897949977506641461264696234781264777062801)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_56 :
Polynomial.coeff recurrence2ExceptionalProduct 56 = 70588 * 10 ^ 70 + 7349919748570618429594007726709067918101628468315596866490912694278575
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_57 :
Polynomial.coeff recurrence2ExceptionalProduct 57 = 148521 * 10 ^ 70 + 3536335445904406197975000411239827629840919665359469205089508004112205
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_58 :
Polynomial.coeff recurrence2ExceptionalProduct 58 = -(1673780 * 10 ^ 70 + 9622629112029994783671948485944220322856317131546633742576069581734384)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_59 :
Polynomial.coeff recurrence2ExceptionalProduct 59 = -(2661734 * 10 ^ 70 + 1269737702488570588164724183096262034415794347097890790864423118540682)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_60 :
Polynomial.coeff recurrence2ExceptionalProduct 60 = 36747872 * 10 ^ 70 + 89758904007966451163450240273591178212239510854208029126379766946903
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_61 :
Polynomial.coeff recurrence2ExceptionalProduct 61 = 33845104 * 10 ^ 70 + 545517841041143494956880855647896149185408669081758599286560926387325
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_62 :
Polynomial.coeff recurrence2ExceptionalProduct 62 = -(738502534 * 10 ^ 70 + 3399259809637285496100184205048660088590843009876757360402316490357902)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_63 :
Polynomial.coeff recurrence2ExceptionalProduct 63 = -(105061558 * 10 ^ 70 + 5201104378695760487275170670034061190954112058173239552280028445688814)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_64 :
Polynomial.coeff recurrence2ExceptionalProduct 64 = 13362160826 * 10 ^ 70 + 4139518628531256106591985764703543033371151522876684515551956011081868
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_65 :
Polynomial.coeff recurrence2ExceptionalProduct 65 = -(9768872450 * 10 ^ 70 + 7040722305791370676066450029182165982489750239513989448941836339938980)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_66 :
Polynomial.coeff recurrence2ExceptionalProduct 66 = -(212655203318 * 10 ^ 70 + 9881063386516234362404857046076157850904205596225588045068957867132627)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_67 :
Polynomial.coeff recurrence2ExceptionalProduct 67 = 369915202308 * 10 ^ 70 + 6636879278024935520559721130387744102341673436026026134625213406997629
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_68 :
Polynomial.coeff recurrence2ExceptionalProduct 68 = 2867656201935 * 10 ^ 70 + 4711253799452211321061851142625370492088352593652383029770385937380424
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_69 :
Polynomial.coeff recurrence2ExceptionalProduct 69 = -(8718389395549 * 10 ^ 70 + 1633196620911875573827157284347192956461348858594534521058488703460406)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_70 :
Polynomial.coeff recurrence2ExceptionalProduct 70 = -(30327408320013 * 10 ^ 70 + 7669559041567317947571617736571440044513900587346739568970162132023240)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_71 :
Polynomial.coeff recurrence2ExceptionalProduct 71 = 157323172588982 * 10 ^ 70 + 9252969992147064188139553527258744016368397234806206416470511745765934
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_72 :
Polynomial.coeff recurrence2ExceptionalProduct 72 = 193270080263200 * 10 ^ 70 + 6198202700379323559328187728387940966906585045184006454663813955502333
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_73 :
Polynomial.coeff recurrence2ExceptionalProduct 73 = -(2259668692723739 * 10 ^ 70 + 4718444193948315736335364659549687561931924518127717836297849039379927)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_74 :
Polynomial.coeff recurrence2ExceptionalProduct 74 = 840392942215601 * 10 ^ 70 + 6577423161743830346410726598659221741654912391223079096460304565973257
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_75 :
Polynomial.coeff recurrence2ExceptionalProduct 75 = 25370064399230947 * 10 ^ 70 + 3330275833313560349711513105629239624254062493027080174283338884223569
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_76 :
Polynomial.coeff recurrence2ExceptionalProduct 76 = -(47980011996121583 * 10 ^ 70 + 298260564945560519673997055024133664248167609800205479327328160459844)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_77 :
Polynomial.coeff recurrence2ExceptionalProduct 77 = -(202395746359578875 * 10 ^ 70 + 9179196914435098876171061488034811618123216677731420926706155981218686)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_78 :
Polynomial.coeff recurrence2ExceptionalProduct 78 = 830590001658700255 * 10 ^ 70 + 9100472427276531092159565119588187518274719224427218308220057121901259
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_79 :
Polynomial.coeff recurrence2ExceptionalProduct 79 = 685193413067536854 * 10 ^ 70 + 6139651925789359388306964282802996960405462355593986890466154219830731
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_80 :
Polynomial.coeff recurrence2ExceptionalProduct 80 = -(9286368465706528068 * 10 ^ 70 + 4026451852587392742206894080705646306336905794833742392229552794549670)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_81 :
Polynomial.coeff recurrence2ExceptionalProduct 81 = 9601158995046983099 * 10 ^ 70 + 4697264770994548492776951611151888705503395545662336064967216839421634
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_82 :
Polynomial.coeff recurrence2ExceptionalProduct 82 = 67444811749567923764 * 10 ^ 70 + 587248638851226861750562784197992848404736029312906214765946176213822
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_83 :
Polynomial.coeff recurrence2ExceptionalProduct 83 = -(205783325162616836314 * 10 ^ 70 + 1454950803020439658915590999315500295665990340450590667206334292385330)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_84 :
Polynomial.coeff recurrence2ExceptionalProduct 84 = -(191017000854084115244 * 10 ^ 70 + 586378344708196969262620439116297479372467804499339254779396370441013)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_85 :
Polynomial.coeff recurrence2ExceptionalProduct 85 = 2031542412801216466541 * 10 ^ 70 + 7091257381707392331725173363284761996853554531127623746608145845335653
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_86 :
Polynomial.coeff recurrence2ExceptionalProduct 86 = -(2370279134212870509754 * 10 ^ 70 + 304673144216675916109305840796385955298040894575876421375493758655581)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_87 :
Polynomial.coeff recurrence2ExceptionalProduct 87 = -(10752005359082615412732 * 10 ^ 70 + 5090480051555007719287570067341887042751297882568511371441428429732787)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_88 :
Polynomial.coeff recurrence2ExceptionalProduct 88 = 38331734290069542152326 * 10 ^ 70 + 5554162916705593370336100691040411567647556973567592561929435150487564
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_89 :
Polynomial.coeff recurrence2ExceptionalProduct 89 = -(1015373578082761696328 * 10 ^ 70 + 6563718456561001821040655229898475580299872587895293384841321226786772)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_90 :
Polynomial.coeff recurrence2ExceptionalProduct 90 = -(256172754146187871883378 * 10 ^ 70 + 6487517789630557453223351358491621654749255857890192257392361872444865)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_91 :
Polynomial.coeff recurrence2ExceptionalProduct 91 = 529072904335011878690799 * 10 ^ 70 + 4635872815018766244658466631102818236253538683631489463970032653650459
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_92 :
Polynomial.coeff recurrence2ExceptionalProduct 92 = 505845707685901658810681 * 10 ^ 70 + 3045113526479076919156563465549600295555849772694985231177631367324890
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_93 :
Polynomial.coeff recurrence2ExceptionalProduct 93 = -(4224655657647773841060621 * 10 ^ 70 + 809299923708681836991204786224980765477757413272897589827230673861124)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_94 :
Polynomial.coeff recurrence2ExceptionalProduct 94 = 5971380087942685996584306 * 10 ^ 70 + 3721741822983045174763494208449717874918970899853976863448419827424618
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_95 :
Polynomial.coeff recurrence2ExceptionalProduct 95 = 10699552024298593034696463 * 10 ^ 70 + 5772674179134294371079745427978714895522111391423144808527699686743416
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_96 :
Polynomial.coeff recurrence2ExceptionalProduct 96 = -(54563494076316265710090235 * 10 ^ 70 + 191452118127308193091519331667208492964902443918739500943029193089270)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_97 :
Polynomial.coeff recurrence2ExceptionalProduct 97 = 62934707710346302696536417 * 10 ^ 70 + 962673406580592719412113216846675704753637467137929006912034435228642
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_98 :
Polynomial.coeff recurrence2ExceptionalProduct 98 = 130003993977936857315318005 * 10 ^ 70 + 1890603328715731319343831537237734356652459750186418072304655513105159
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_99 :
Polynomial.coeff recurrence2ExceptionalProduct 99 = -(576836305665920391158486525 * 10 ^ 70 + 3692375653578530366691349215998718413787059641577368546022450050287309)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_100 :
Polynomial.coeff recurrence2ExceptionalProduct 100 = 678824976613071408739256364 * 10 ^ 70 + 1113339717494683596301628124971545410968103596051363846061258228112452
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_101 :
Polynomial.coeff recurrence2ExceptionalProduct 101 = 976621856991058723891023768 * 10 ^ 70 + 5056022363494995685047899728686971425732405000916258875180308856099600
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_102 :
Polynomial.coeff recurrence2ExceptionalProduct 102 = -(4911368581971145354372931284 * 10 ^ 70 + 6672317983804157894906802557687388180619337689413441895212994040357900)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_103 :
Polynomial.coeff recurrence2ExceptionalProduct 103 = 6995775178806802541280548621 * 10 ^ 70 + 5731527026779996204198718377396410074997023823438595182116490402223402
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_104 :
Polynomial.coeff recurrence2ExceptionalProduct 104 = 2800493956758801408864669895 * 10 ^ 70 + 6757566121754033735693966513685012201598683680819803338901988111176604
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_105 :
Polynomial.coeff recurrence2ExceptionalProduct 105 = -(30728232510030144703126315930 * 10 ^ 70 + 4964362524293432101911441225304393789143694897031182657656336107427128)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_106 :
Polynomial.coeff recurrence2ExceptionalProduct 106 = 57833735550200740399953999153 * 10 ^ 70 + 9366487342853499885006525804231283705720907757183381939882506995029648
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_107 :
Polynomial.coeff recurrence2ExceptionalProduct 107 = -(28876576746669442390492599349 * 10 ^ 70 + 9834174608936150498668756518252717197847030929331255608618146007659942)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_108 :
Polynomial.coeff recurrence2ExceptionalProduct 108 = -(109863641123629577694172109882 * 10 ^ 70 + 7428392756239192327643488205851663630360165798316865930708023169723234)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_109 :
Polynomial.coeff recurrence2ExceptionalProduct 109 = 316379558478709605664608966191 * 10 ^ 70 + 4519217254503896318730003358438400017531935318193432480849237861440294
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_110 :
Polynomial.coeff recurrence2ExceptionalProduct 110 = -(380989173469896572241602134875 * 10 ^ 70 + 317566986624439326663893736074254755692707258283112379320619260267367)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_111 :
Polynomial.coeff recurrence2ExceptionalProduct 111 = 16174048964653152765229984619 * 10 ^ 70 + 7180470719715866263610123463747209635965744383118594512568449463948113
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_112 :
Polynomial.coeff recurrence2ExceptionalProduct 112 = 843286013707195127927314936818 * 10 ^ 70 + 1161369207297596133666305846676135154785975174546785226194463712593599
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_113 :
Polynomial.coeff recurrence2ExceptionalProduct 113 = -(1733626915126433598913680866805 * 10 ^ 70 + 6297691464917825559400215327510834268447014153795041728417094308600745)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_114 :
Polynomial.coeff recurrence2ExceptionalProduct 114 = 1738077292844312424215549933002 * 10 ^ 70 + 1249024919399049004910929939304527731741261147697868997013552604483266
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_115 :
Polynomial.coeff recurrence2ExceptionalProduct 115 = -(142270709871359333779847079306 * 10 ^ 70 + 5209264122483438709131537003925634465692136837884345983345229257121586)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_116 :
Polynomial.coeff recurrence2ExceptionalProduct 116 = -(2706576561497382842179733906781 * 10 ^ 70 + 2102696494643881658966410431585869140943144960671766499664402056109585)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_117 :
Polynomial.coeff recurrence2ExceptionalProduct 117 = 5160756731961429513190740741130 * 10 ^ 70 + 7836348405953177439538457410684174891984310948907917915493707846424055
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_118 :
Polynomial.coeff recurrence2ExceptionalProduct 118 = -(5189579961905659078062793099510 * 10 ^ 70 + 6935878702700252826680022575963969606283791137813180815099912851728505)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_119 :
Polynomial.coeff recurrence2ExceptionalProduct 119 = 1984113608307749325751447456120 * 10 ^ 70 + 729485844887578818513871795374336764587003564419999975375762957168083
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_120 :
Polynomial.coeff recurrence2ExceptionalProduct 120 = 3064290815209133222297287139120 * 10 ^ 70 + 5961557085290623384412172303246879039895199586810078051240994550347555
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_121 :
Polynomial.coeff recurrence2ExceptionalProduct 121 = -(7041779910121006310676981999328 * 10 ^ 70 + 7590680728008037759354033523158006388365603661869223039053388898170111)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_122 :
Polynomial.coeff recurrence2ExceptionalProduct 122 = 7511850123853507181287843322720 * 10 ^ 70 + 1667623857396524438232116327212357518709595487292084581779553310204032
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_123 :
Polynomial.coeff recurrence2ExceptionalProduct 123 = -(4272571389507279641894866745593 * 10 ^ 70 + 1692870475774335400943078186266068193381714508152530485823678751033424)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_124 :
Polynomial.coeff recurrence2ExceptionalProduct 124 = -(564085837046512090947264919251 * 10 ^ 70 + 3647618535886373832612157825213400174789937671353356992272389230518270)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_125 :
Polynomial.coeff recurrence2ExceptionalProduct 125 = 4180581222883930284849420077216 * 10 ^ 70 + 50169343081451109294431483702344556895840476477048201014040682636034
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_126 :
Polynomial.coeff recurrence2ExceptionalProduct 126 = -(4974580684167422340906539685046 * 10 ^ 70 + 8354404133421838858571351523225747512495558760245211059984875368764815)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_127 :
Polynomial.coeff recurrence2ExceptionalProduct 127 = 3321855414342779454141175150753 * 10 ^ 70 + 9107468857344727057069020320500064077854540554511144140529221667706983
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_128 :
Polynomial.coeff recurrence2ExceptionalProduct 128 = -(848421989474998023722845592076 * 10 ^ 70 + 3897430198231368287905824906118449834476435105886659379787825020036245)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_129 :
Polynomial.coeff recurrence2ExceptionalProduct 129 = -(920505798690292723688115506921 * 10 ^ 70 + 2113392297194427036983168593391025750061198553623402357432522780398593)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_130 :
Polynomial.coeff recurrence2ExceptionalProduct 130 = 1424483285631968080630226880997 * 10 ^ 70 + 3688177000666685709196615540890243400502011657329807819069011873978368
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_131 :
Polynomial.coeff recurrence2ExceptionalProduct 131 = -(1016866871202270057456261109336 * 10 ^ 70 + 6583602100618306396878096604620075833966850455377467006777042671307932)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_132 :
Polynomial.coeff recurrence2ExceptionalProduct 132 = 367527133241869987766502073523 * 10 ^ 70 + 8884515078841182609680771016653071223365048102844477637985044370776871
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_133 :
Polynomial.coeff recurrence2ExceptionalProduct 133 = 67518477735773249768283405253 * 10 ^ 70 + 5535029850990308996305103117429292925995453447833274535682368840781909
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_134 :
Polynomial.coeff recurrence2ExceptionalProduct 134 = -(195541599314439733220540685812 * 10 ^ 70 + 206234314903756274920971802835403799526567110405744218514609504619822)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_135 :
Polynomial.coeff recurrence2ExceptionalProduct 135 = 141826360593659238037463673557 * 10 ^ 70 + 1648232289969695523490775203850257651077764476762693921797664961068350
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_136 :
Polynomial.coeff recurrence2ExceptionalProduct 136 = -(52772341585217920332752800380 * 10 ^ 70 + 7556787971747202580724355418202209517287677863510325427237075991516017)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_137 :
Polynomial.coeff recurrence2ExceptionalProduct 137 = -(266037343648290871540772622 * 10 ^ 70 + 109147315842759559677837779272051331667866088405040639168334231149267)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_138 :
Polynomial.coeff recurrence2ExceptionalProduct 138 = 13919270524834260068864156592 * 10 ^ 70 + 3326329015344139034407724953399048083124134865251490039317542185214096
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_139 :
Polynomial.coeff recurrence2ExceptionalProduct 139 = -(9395292200057097978763697070 * 10 ^ 70 + 7318765435852128828082629302948036738130663731478707865265834767874186)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_140 :
Polynomial.coeff recurrence2ExceptionalProduct 140 = 2995940005411745323109310667 * 10 ^ 70 + 4464390914671289957055852508631847672540361824310366294422212100320564
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_141 :
Polynomial.coeff recurrence2ExceptionalProduct 141 = 61980516299132994629724586 * 10 ^ 70 + 7963153423677586927863447998884966891239123701657834601884554402251064
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_142 :
Polynomial.coeff recurrence2ExceptionalProduct 142 = -(584238613196211428049621441 * 10 ^ 70 + 9529856581268831271794842673663127745653803689286808840223580942887708)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_143 :
Polynomial.coeff recurrence2ExceptionalProduct 143 = 304512697019243196962359228 * 10 ^ 70 + 5675525738636569013135506412304597521149732006591654889771420143587296
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_144 :
Polynomial.coeff recurrence2ExceptionalProduct 144 = -(64875093933639441736606651 * 10 ^ 70 + 4750755018667949861417405761345184178385558367656201663553698040417379)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_145 :
Polynomial.coeff recurrence2ExceptionalProduct 145 = -(11663832816515126202338580 * 10 ^ 70 + 8099805400655236061947232803801712833012659962103709454833376216717709)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_146 :
Polynomial.coeff recurrence2ExceptionalProduct 146 = 13409901212491001941358821 * 10 ^ 70 + 9770263277878583597154469535741790151439676963850949738145939701871948
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_147 :
Polynomial.coeff recurrence2ExceptionalProduct 147 = -(4193856341800954797106067 * 10 ^ 70 + 3338879655595881357492738069061077695542810542923845045339272446264126)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_148 :
Polynomial.coeff recurrence2ExceptionalProduct 148 = 200445778642751701401934 * 10 ^ 70 + 4891562173741188102189459033400658668724361305809345853471079001846868
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_149 :
Polynomial.coeff recurrence2ExceptionalProduct 149 = 329865733774190079810623 * 10 ^ 70 + 9716064942154727540451697881574976309309774707093960632985685203048308
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_150 :
Polynomial.coeff recurrence2ExceptionalProduct 150 = -(125983674825029627246793 * 10 ^ 70 + 746041725928433953264810189767665137163822230723556434124107730178599)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_151 :
Polynomial.coeff recurrence2ExceptionalProduct 151 = 12176851322104210864051 * 10 ^ 70 + 5405850395179194994460969482709210620868577243874929294273795343577343
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_152 :
Polynomial.coeff recurrence2ExceptionalProduct 152 = 5594623382471179079893 * 10 ^ 70 + 4049622635296666282208954002527797384174666340399638758379909902743465
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_153 :
Polynomial.coeff recurrence2ExceptionalProduct 153 = -(2191237259796771418525 * 10 ^ 70 + 5233562731340876301406574156330860143159914705726126166671232665526789)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_154 :
Polynomial.coeff recurrence2ExceptionalProduct 154 = 174091541242205865791 * 10 ^ 70 + 8979283769642141318031601835887575774993845349924646383691843988718249
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_155 :
Polynomial.coeff recurrence2ExceptionalProduct 155 = 78827814340838560950 * 10 ^ 70 + 5733906839126339896857863289017856265048401595620788524676757728593859
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_156 :
Polynomial.coeff recurrence2ExceptionalProduct 156 = -(22413176238144911426 * 10 ^ 70 + 2458691995150997220199808183873312789732385775982564635331140118964405)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_157 :
Polynomial.coeff recurrence2ExceptionalProduct 157 = 244303237049703813 * 10 ^ 70 + 9245863362786512758211268475342128829193355362218291387781965073178689
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_158 :
Polynomial.coeff recurrence2ExceptionalProduct 158 = 807423507372207915 * 10 ^ 70 + 2907479335757457641735578725513709221894655927027863547681573724517979
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_159 :
Polynomial.coeff recurrence2ExceptionalProduct 159 = -(101550076557735071 * 10 ^ 70 + 9152395487390308825178512930352380951907572693348839444886798235844935)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_160 :
Polynomial.coeff recurrence2ExceptionalProduct 160 = -(14346076337618034 * 10 ^ 70 + 6674098732072327859864518659762823013284910552965697252937107711341099)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_161 :
Polynomial.coeff recurrence2ExceptionalProduct 161 = 3752324455656202 * 10 ^ 70 + 5175798594695044768598150587341907176978182192784982228342718779128899
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_162 :
Polynomial.coeff recurrence2ExceptionalProduct 162 = 124992453700994 * 10 ^ 70 + 6657773579030250564280879448934379679060797919098106674769060153828386
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_163 :
Polynomial.coeff recurrence2ExceptionalProduct 163 = -(81379664555039 * 10 ^ 70 + 1610659506352394603439719381635003253060270772036881756842733129218458)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_164 :
Polynomial.coeff recurrence2ExceptionalProduct 164 = -(758517740107 * 10 ^ 70 + 6765362504141612171735583427793198626106245897089305997853617511254904)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_165 :
Polynomial.coeff recurrence2ExceptionalProduct 165 = 1273456795690 * 10 ^ 70 + 1737377524756637192476230842930937292795059254395054559133348587128504
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_166 :
Polynomial.coeff recurrence2ExceptionalProduct 166 = 32242915903 * 10 ^ 70 + 3773408856464037003192480328756593916740602000635413577348720061084669
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_167 :
Polynomial.coeff recurrence2ExceptionalProduct 167 = -(13833753107 * 10 ^ 70 + 5904323640383786699767225069062916236928974388226747587610721046793019)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_168 :
Polynomial.coeff recurrence2ExceptionalProduct 168 = -(1028259689 * 10 ^ 70 + 5851510642794679897085384085863605054563090242254344903407322670942396)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_169 :
Polynomial.coeff recurrence2ExceptionalProduct 169 = 49938169 * 10 ^ 70 + 329533994375999445818228543781678848472909042592571002744037783640814
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_170 :
Polynomial.coeff recurrence2ExceptionalProduct 170 = 11614895 * 10 ^ 70 + 2729709647106052947168486237021077547041238692312405372213670710400919
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_171 :
Polynomial.coeff recurrence2ExceptionalProduct 171 = 834052 * 10 ^ 70 + 9858705572159031767672384036154792061054113700847169877636327829596313
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_172 :
Polynomial.coeff recurrence2ExceptionalProduct 172 = 35138 * 10 ^ 70 + 573958967164954559703550661427196371515804502939580702580099887406751
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_173 :
Polynomial.coeff recurrence2ExceptionalProduct 173 = 982 * 10 ^ 70 + 476536544450933187859581662630978130593051007236900846592254064577823
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_174 :
Polynomial.coeff recurrence2ExceptionalProduct 174 = 19 * 10 ^ 70 + 201738507549245857740417831814927945194603816871153360522986840951576
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_175 :
Polynomial.coeff recurrence2ExceptionalProduct 175 = 2590334884478045949618454757618757374449021359078660735983310493896292
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_176 :
Polynomial.coeff recurrence2ExceptionalProduct 176 = 24726789264893570127529264904553469105636610184203191232381603508441
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_177 :
Polynomial.coeff recurrence2ExceptionalProduct 177 = 161802614570873968609746227325830059579355070554895720291438423699
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_178 :
Polynomial.coeff recurrence2ExceptionalProduct 178 = 684481757264596808744193918080996431643661293377763617859746328
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_179 :
Polynomial.coeff recurrence2ExceptionalProduct 179 = 1559114659305173638564267988435542366590388297023471845358766
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_180 :
Polynomial.coeff recurrence2ExceptionalProduct 180 = 18706287284264735025185938886800570797719454105688711427
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_181 :
Polynomial.coeff recurrence2ExceptionalProduct 181 = -10279976870582267855639879074409970767282377203252952703
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_182 :
Polynomial.coeff recurrence2ExceptionalProduct 182 = -24816490176589969372083057336547509125912462193664260
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_183 :
Polynomial.coeff recurrence2ExceptionalProduct 183 = -12064146606251989635038940038993896494134240839726
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_184 :
Polynomial.coeff recurrence2ExceptionalProduct 184 = 40246446432363529434470043240204824813598601911
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_185 :
Polynomial.coeff recurrence2ExceptionalProduct 185 = 72138992442074386338722923695269656113364109
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_186 :
Polynomial.coeff recurrence2ExceptionalProduct 186 = 46018701789594108135664733430096178815735
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_187 :
Polynomial.coeff recurrence2ExceptionalProduct 187 = 12452683985295238859848991041189999177
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_188 :
Polynomial.coeff recurrence2ExceptionalProduct 188 = 1242648732597308443281398765999555
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_189 :
Polynomial.coeff recurrence2ExceptionalProduct 189 = 43661757379497123762590298513
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_190 :
Polynomial.coeff recurrence2ExceptionalProduct 190 = 251108966979503023409725
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_191 :
Polynomial.coeff recurrence2ExceptionalProduct 191 = 396784196304291633
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_192 :
Polynomial.coeff recurrence2ExceptionalProduct 192 = 1259182849
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2ExceptionalProduct_coeff_193 :
Polynomial.coeff recurrence2ExceptionalProduct 193 = 1