Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar2MainPart0.Coefficients0To91

Recurrence 2 lookup certificate: Scalar2Main 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.recurrence2Scalar2Main_coeff_0 :
Polynomial.coeff recurrence2Scalar2Main 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_1 :
Polynomial.coeff recurrence2Scalar2Main 1 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_2 :
Polynomial.coeff recurrence2Scalar2Main 2 = -10529792
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_3 :
Polynomial.coeff recurrence2Scalar2Main 3 = -249451191520
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_4 :
Polynomial.coeff recurrence2Scalar2Main 4 = 745610070910752
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_5 :
Polynomial.coeff recurrence2Scalar2Main 5 = 18895545486795579744
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_6 :
Polynomial.coeff recurrence2Scalar2Main 6 = -16247831568543708403912
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_7 :
Polynomial.coeff recurrence2Scalar2Main 7 = 45147908737249219912255528
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_8 :
Polynomial.coeff recurrence2Scalar2Main 8 = -29881411614576144932874912544
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_9 :
Polynomial.coeff recurrence2Scalar2Main 9 = 21036587864633413436809175746236
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_10 :
Polynomial.coeff recurrence2Scalar2Main 10 = -6002817724092867864637372919007692
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_11 :
Polynomial.coeff recurrence2Scalar2Main 11 = -4316427893016067443990366817624917370
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_12 :
Polynomial.coeff recurrence2Scalar2Main 12 = 4782439040182593299811115397371955369794
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_13 :
Polynomial.coeff recurrence2Scalar2Main 13 = -2634240198427590708026373961562366667290616
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_14 :
Polynomial.coeff recurrence2Scalar2Main 14 = 963488150141891600719593185234919082422477549
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_15 :
Polynomial.coeff recurrence2Scalar2Main 15 = -261585862998558353121181385247173898276512307196
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_16 :
Polynomial.coeff recurrence2Scalar2Main 16 = 54438546624135816636624793729937392916954216556316
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_17 :
Polynomial.coeff recurrence2Scalar2Main 17 = -8833153023304696005193727029010782602235134241325529
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_18 :
Polynomial.coeff recurrence2Scalar2Main 18 = 1127075097054613870561944644319646704737900636008910474
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_19 :
Polynomial.coeff recurrence2Scalar2Main 19 = -112885466578084577363966093354627702159691595773685105427
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_20 :
Polynomial.coeff recurrence2Scalar2Main 20 = 8731392712770797236723341668506883340613868779290813839428
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_21 :
Polynomial.coeff recurrence2Scalar2Main 21 = -495128167052774291706026717762963908054546515359309518555021
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_22 :
Polynomial.coeff recurrence2Scalar2Main 22 = 16996371698066759565926509302512668102378744164343071152366464
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_23 :
Polynomial.coeff recurrence2Scalar2Main 23 = 109270296715914058061385254480150249356908911629060523907131688
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_24 :
Polynomial.coeff recurrence2Scalar2Main 24 = -63413912007431996174765286589417293195350626275367711071047071256
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_25 :
Polynomial.coeff recurrence2Scalar2Main 25 = 5083118210859125669707853236180718162473890368157220742806365938108
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_26 :
Polynomial.coeff recurrence2Scalar2Main 26 = -245233203302910639028440558533268675801251289976564788004498730220079
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_27 :
Polynomial.coeff recurrence2Scalar2Main 27 = 6343495224909179541938764095592845677067182896021559360316294128803366
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_28 :
Polynomial.coeff recurrence2Scalar2Main 28 = 13 * 10 ^ 70 + 4068275893168603208737233333403224867640002980955806703317201020213606
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_29 :
Polynomial.coeff recurrence2Scalar2Main 29 = -(2719 * 10 ^ 70 + 8667256190890545443741881899134369867632940868449333820635423180704879)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_30 :
Polynomial.coeff recurrence2Scalar2Main 30 = 184137 * 10 ^ 70 + 9751910405027851850498751860171534823959024003151357816772278718596587
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_31 :
Polynomial.coeff recurrence2Scalar2Main 31 = -(8336343 * 10 ^ 70 + 453408801553223278525769443367244573566929621250794409599799948924478)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_32 :
Polynomial.coeff recurrence2Scalar2Main 32 = 280728318 * 10 ^ 70 + 8387134589452884913236825768212806000496283809377266511148575584116282
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_33 :
Polynomial.coeff recurrence2Scalar2Main 33 = -(7975284362 * 10 ^ 70 + 1440949358006030346380198047678621048431123942741621490987197646930776)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_34 :
Polynomial.coeff recurrence2Scalar2Main 34 = 277170502011 * 10 ^ 70 + 8889877757841620788874087372829740032924378727179948434475579091469612
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_35 :
Polynomial.coeff recurrence2Scalar2Main 35 = -(14648385752413 * 10 ^ 70 + 3171144706645943355692431329821803580862733598008653458906907196728948)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_36 :
Polynomial.coeff recurrence2Scalar2Main 36 = 804802344381640 * 10 ^ 70 + 2626619381308034924172865713892488675936909852887107508246898408855705
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_37 :
Polynomial.coeff recurrence2Scalar2Main 37 = -(36188863824673420 * 10 ^ 70 + 5511878677225010211219681242825584975137333126992304438179799194174266)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_38 :
Polynomial.coeff recurrence2Scalar2Main 38 = 1278341751679400674 * 10 ^ 70 + 8953439766896298503628875496940581272853264001706804810269702453007698
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_39 :
Polynomial.coeff recurrence2Scalar2Main 39 = -(35252214770680601062 * 10 ^ 70 + 9276989989382682979145153004396569967294191145921157197508103712334399)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_40 :
Polynomial.coeff recurrence2Scalar2Main 40 = 736649520534053202030 * 10 ^ 70 + 3568757422172062576148809235836828643579761529688734635530676854489928
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_41 :
Polynomial.coeff recurrence2Scalar2Main 41 = -(10318257044567886904209 * 10 ^ 70 + 9116825605648942440892850269709561259142195338418923404258431137494566)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_42 :
Polynomial.coeff recurrence2Scalar2Main 42 = 36443043350551329698719 * 10 ^ 70 + 1754208465588934041143545789138362135860627625364168189912303350113599
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_43 :
Polynomial.coeff recurrence2Scalar2Main 43 = 2689340703725529490272333 * 10 ^ 70 + 1964494283454713474801395473024528935386640449731870651093158458542301
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_44 :
Polynomial.coeff recurrence2Scalar2Main 44 = -(83120614213464567397639261 * 10 ^ 70 + 4400626757602995650773846463810783783591508195301203009483648962644708)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_45 :
Polynomial.coeff recurrence2Scalar2Main 45 = 1114471632697188121917364593 * 10 ^ 70 + 6822438141399277770716702505378060986744828805669299767320610881209195
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_46 :
Polynomial.coeff recurrence2Scalar2Main 46 = 1811936574286448532172806588 * 10 ^ 70 + 5836103131209408360041211596627926477439572385007107528999005775478765
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_47 :
Polynomial.coeff recurrence2Scalar2Main 47 = -(322115911106498108882028940110 * 10 ^ 70 + 1581684073395032195482134932858094693444640248319997171820638758445660)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_48 :
Polynomial.coeff recurrence2Scalar2Main 48 = -(520940962334617201591297645520 * 10 ^ 70 + 8623945024767158866936411470172328887607448408195091806546384594980439)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_49 :
Polynomial.coeff recurrence2Scalar2Main 49 = 440458655640833418610882732439122 * 10 ^ 70 + 815780273781241026986723871684923318948911799872011776996803489994819
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_50 :
Polynomial.coeff recurrence2Scalar2Main 50 = -(20340323167221691460460784442615880 * 10 ^ 70 + 1057428207513990628001118639895742412715793094540321027667098585200669)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_51 :
Polynomial.coeff recurrence2Scalar2Main 51 = 598102977884323476561992231828859336 * 10 ^ 70 + 7733446515937484623243994039504174881451845542583984106952711489047116
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_52 :
Polynomial.coeff recurrence2Scalar2Main 52 = -(13393260606313757996084271416606041468 * 10 ^ 70 + 758564187247159548238127295509137506352126127077594153034372565146909)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_53 :
Polynomial.coeff recurrence2Scalar2Main 53 = 239802840703225678054107165332935663943 * 10 ^ 70 + 7623161115903474642170095556305623832424088559538211721641607030482904
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_54 :
Polynomial.coeff recurrence2Scalar2Main 54 = -(3394113169659754985269419700053150007662 * 10 ^ 70 + 7357772952298395842067825111590163348205639410467306783087642114803539)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_55 :
Polynomial.coeff recurrence2Scalar2Main 55 = 33353143116362703083781676951954179991017 * 10 ^ 70 + 3496619824252303510271817710287297592474684895475919497747010266180580
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_56 :
Polynomial.coeff recurrence2Scalar2Main 56 = -(33370174793629617068540671681826416209141 * 10 ^ 70 + 1746261198886546019303539284380499033802058768382022955426298609800839)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_57 :
Polynomial.coeff recurrence2Scalar2Main 57 = -(8669420916550283735337571112390435530610746 * 10 ^ 70 + 5925866224085386844900656567312212826972618172363611761908015678321888)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_58 :
Polynomial.coeff recurrence2Scalar2Main 58 = 280367441501543725649867005150851850874480614 * 10 ^ 70 + 1297337377169159043904103369126710724085005048867397615310374921857266
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_59 :
Polynomial.coeff recurrence2Scalar2Main 59 = -(6305600641385068433139850130826659248242417427 * 10 ^ 70 + 4088199747477545904758718466788909193424994696296646277924665910656853)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_60 :
Polynomial.coeff recurrence2Scalar2Main 60 = 118499207073787859860146438625239385318198633205 * 10 ^ 70 + 5908082442802460759046440694977966762065945113792730366456667900270699
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_61 :
Polynomial.coeff recurrence2Scalar2Main 61 = -(1958140663183750269703620007886073771582107645698 * 10 ^ 70 + 5738089754676262352279871906636847362937634986560842637400896496451958)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_62 :
Polynomial.coeff recurrence2Scalar2Main 62 = 28947990843536646800716405344249293348255323190908 * 10 ^ 70 + 6823319631899911493194946032774589081170621016460391250597973021102361
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_63 :
Polynomial.coeff recurrence2Scalar2Main 63 = -(384102030884694962406929268407786691003419177610857 * 10 ^ 70 + 7502004751042309998783736331993965953439186451631975935113438415149874)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_64 :
Polynomial.coeff recurrence2Scalar2Main 64 = 4542426431794067351085848256733479588060132903034026 * 10 ^ 70 + 2975916411347843032534411372006100695795907692039740228725911423150066
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_65 :
Polynomial.coeff recurrence2Scalar2Main 65 = -(46821868941673083796735184219420463227179235124170134 * 10 ^ 70 + 8875309011657045235541517744401823861967946931453691390516766709503504)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_66 :
Polynomial.coeff recurrence2Scalar2Main 66 = 395414611703218390243217217676187161099918132549664435 * 10 ^ 70 + 3481839139161752482848598876929132102331819646626244851497489323860750
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_67 :
Polynomial.coeff recurrence2Scalar2Main 67 = -(2150426602031640085802544761814026037391828159490271028 * 10 ^ 70 + 8460724558156443894044338385545254361319830723380362601209346788231683)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_68 :
Polynomial.coeff recurrence2Scalar2Main 68 = -(7638531835744286558529135984736341793853507412082271185 * 10 ^ 70 + 9649430815071452858076069204457631283436974553820652231124987010704211)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_69 :
Polynomial.coeff recurrence2Scalar2Main 69 = 461195084211357391517293531493439486661550955730976026728 * 10 ^ 70 + 9534216896502901931895094629667693575842628404968626017004495500569191
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_70 :
Polynomial.coeff recurrence2Scalar2Main 70 = -(9015851482647682413281120725815565998117990390944899736616 * 10 ^ 70 + 1412756376525035484101188277833488455571491883352117482380785901703363)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_71 :
Polynomial.coeff recurrence2Scalar2Main 71 = 134565519448727490850096292894658668421334135270257128978463 * 10 ^ 70 + 4054274606160662415777650521039007204143328678030020674523014094189439
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_72 :
Polynomial.coeff recurrence2Scalar2Main 72 = -(1737291088481775946628494158426805734964335873322337304912508 * 10 ^ 70 + 80533233632806505368280451760939085689212155028671423758864922456883)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_73 :
Polynomial.coeff recurrence2Scalar2Main 73 = 20275765405165084933658293530243421227634092345159864037109618 * 10 ^ 70 + 3977585362725092128498465316864139081753996488998646902787073920790728
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_74 :
Polynomial.coeff recurrence2Scalar2Main 74 = -(218464809488103099574875571512065337259470418412222079082559965 * 10 ^ 70 + 3960210497550242223371845848566972783107813767053005393141184645076062)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_75 :
Polynomial.coeff recurrence2Scalar2Main 75 = 2199170491537072738547234777557586161238756027204067899209643619 * 10 ^ 70 + 1892330447074262304192754939815659993144725835054834564380013026193371
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_76 :
Polynomial.coeff recurrence2Scalar2Main 76 = -(20840475597712613438596252688298588186594085510077526914062213340 * 10 ^ 70 + 1713097054276486885276109977162772355565474136621438654104751982730619)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_77 :
Polynomial.coeff recurrence2Scalar2Main 77 = 186901201683872147710328571796558756343370029392287371967779108486 * 10 ^ 70 + 2513476437224419095959701958372833670876558105396760452316590590097383
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_78 :
Polynomial.coeff recurrence2Scalar2Main 78 = -(1592350834805553737050477620601815080573392746237958572900474742302 * 10 ^ 70 + 7908491377346243943261230898748501899247071695204412458584408175050602)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_79 :
Polynomial.coeff recurrence2Scalar2Main 79 = 12925103463121916259587994370275916529288955810068119624134121026079 * 10 ^ 70 + 9122982010030923601829964215864384989471093092384027127652184890332181
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_80 :
Polynomial.coeff recurrence2Scalar2Main 80 = -(100169923692549578647790418663685007325896745825145928516458787723804 * 10 ^ 70 + 7642563155422397883327135721609183116623080174215386944690841838579143)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_81 :
Polynomial.coeff recurrence2Scalar2Main 81 = 742438344420302227143250327220253089005130174850868175712772434237241 * 10 ^ 70 + 5924405154748368978056136006925984832504522174738516023741040746932221
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_82 :
Polynomial.coeff recurrence2Scalar2Main 82 = -(5269294915611503978343151251094510903097037281475443333521048096990425 * 10 ^ 70 + 6408399731431656827223869811031849899980923290595004139252053941589326)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_83 :
Polynomial.coeff recurrence2Scalar2Main 83 = (3 * 10 ^ 70 + 5847203690519808488161664430971685345726443219749709573386995262059605) * 10 ^ 70 + 5380581652139313405666936545251622061012697822253014730765289354140451
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_84 :
Polynomial.coeff recurrence2Scalar2Main 84 = -((23 * 10 ^ 70 + 3959980907054204163414342590175167475981846720357365334492238552267728) * 10 ^ 70 + 734219204577271433759105766904442160350676560920156133677610946684793)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_85 :
Polynomial.coeff recurrence2Scalar2Main 85 = (146 * 10 ^ 70 + 5996975800228024525028639652381313818085194087512867136790448936587823) * 10 ^ 70 + 2736010082754030124515781517745497861269690077633813914847709892163353
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_86 :
Polynomial.coeff recurrence2Scalar2Main 86 = -((882 * 10 ^ 70 + 4605783784036102227979101189213163764810606968418665458162872304975699) * 10 ^ 70 + 6416952126235487557300209366174985023976205598910791607672844504787618)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_87 :
Polynomial.coeff recurrence2Scalar2Main 87 = (5105 * 10 ^ 70 + 2396293060499439488724915973639603504616421977372981471919756405628192) * 10 ^ 70 + 2271017798123382181988875846331377792592293826129836432624550592493819
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_88 :
Polynomial.coeff recurrence2Scalar2Main 88 = -((28390 * 10 ^ 70 + 9575476638571668704462185970066425763543223699876009555049847235874278) * 10 ^ 70 + 7302248927740669524839155272133424175653403974387802347685888321677345)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_89 :
Polynomial.coeff recurrence2Scalar2Main 89 = (151758 * 10 ^ 70 + 5824340252178451158906946315736589403020617876611538410482848283918212) * 10 ^ 70 + 113335752941977260642322438158756374670845668298859671923784456177856
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_90 :
Polynomial.coeff recurrence2Scalar2Main 90 = -((779452 * 10 ^ 70 + 4844387313709757669527528220794941358354374796105816311531705081726379) * 10 ^ 70 + 7927635988459701512386616395146164329050939916503811934183645753891870)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_91 :
Polynomial.coeff recurrence2Scalar2Main 91 = (3844646 * 10 ^ 70 + 1267494430123415052291778898866379025539798531583060903511065915005689) * 10 ^ 70 + 8920790074024902472235898812634818382559375560084258512366802012784898