Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar1MainPart0.Coefficients0To91

Recurrence 2 lookup certificate: Scalar1Main 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.recurrence2Scalar1Main_coeff_0 :
Polynomial.coeff recurrence2Scalar1Main 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_1 :
Polynomial.coeff recurrence2Scalar1Main 1 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_2 :
Polynomial.coeff recurrence2Scalar1Main 2 = -404480
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_3 :
Polynomial.coeff recurrence2Scalar1Main 3 = -7348271328
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_4 :
Polynomial.coeff recurrence2Scalar1Main 4 = 27503329618720
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_5 :
Polynomial.coeff recurrence2Scalar1Main 5 = 538904871211337216
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_6 :
Polynomial.coeff recurrence2Scalar1Main 6 = -296005742115410499016
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_7 :
Polynomial.coeff recurrence2Scalar1Main 7 = 1708202552210422463458008
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_8 :
Polynomial.coeff recurrence2Scalar1Main 8 = -1025243188921851347644877096
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_9 :
Polynomial.coeff recurrence2Scalar1Main 9 = 1365451106918446934295896550140
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_10 :
Polynomial.coeff recurrence2Scalar1Main 10 = -661840139115459282124790182357960
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_11 :
Polynomial.coeff recurrence2Scalar1Main 11 = -60648465426694726364646443539838206
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_12 :
Polynomial.coeff recurrence2Scalar1Main 12 = 222826559137399597751455285522451469514
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_13 :
Polynomial.coeff recurrence2Scalar1Main 13 = -161377741426687435966241388574604056602798
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_14 :
Polynomial.coeff recurrence2Scalar1Main 14 = 68671137490440094730676841776760187964848747
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_15 :
Polynomial.coeff recurrence2Scalar1Main 15 = -21424633508222065040026149323869502664658304069
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_16 :
Polynomial.coeff recurrence2Scalar1Main 16 = 5072864742099636339743123904044248584016409919599
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_17 :
Polynomial.coeff recurrence2Scalar1Main 17 = -934052118624257740092206118849360570344417851699105
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_18 :
Polynomial.coeff recurrence2Scalar1Main 18 = 135379422407535178404332361835089895577716006371104633
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_19 :
Polynomial.coeff recurrence2Scalar1Main 19 = -15506300564302540802252214762873854131671967491900055764
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_20 :
Polynomial.coeff recurrence2Scalar1Main 20 = 1396019350994075881665134755901682861441575756760200550892
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_21 :
Polynomial.coeff recurrence2Scalar1Main 21 = -96260319390396100006063937643843331388398051575850180997055
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_22 :
Polynomial.coeff recurrence2Scalar1Main 22 = 4701866091695443197454099641498692346662593918121691132976221
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_23 :
Polynomial.coeff recurrence2Scalar1Main 23 = -112315147744846049777095088300482603335425044502457101968594789
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_24 :
Polynomial.coeff recurrence2Scalar1Main 24 = -5392348049145314384686997890410462278900834525148867504511703832
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_25 :
Polynomial.coeff recurrence2Scalar1Main 25 = 833117414863121478375929309177168416131469189831147329134180879896
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_26 :
Polynomial.coeff recurrence2Scalar1Main 26 = -56276018611075344787030528639539874377580979940513594692862033306993
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_27 :
Polynomial.coeff recurrence2Scalar1Main 27 = 2429882723784907340489488364573425269264039444919970312020728452962855
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_28 :
Polynomial.coeff recurrence2Scalar1Main 28 = -(4 * 10 ^ 70 + 9496465773818816777147103165738750401987465629787580880064130721901309)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_29 :
Polynomial.coeff recurrence2Scalar1Main 29 = -(239 * 10 ^ 70 + 7984718649543281840431706707903077393276682523166533614421548827224573)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_30 :
Polynomial.coeff recurrence2Scalar1Main 30 = 32574 * 10 ^ 70 + 6579276448250686830231781295024322411467995596253242502467851361525671
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_31 :
Polynomial.coeff recurrence2Scalar1Main 31 = -(2066182 * 10 ^ 70 + 9928643141770216725830770826538412462401806258729422114760252247524874)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_32 :
Polynomial.coeff recurrence2Scalar1Main 32 = 93069002 * 10 ^ 70 + 2596625238780606588642259157679673076580483812034123646117656845883919
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_33 :
Polynomial.coeff recurrence2Scalar1Main 33 = -(3267789411 * 10 ^ 70 + 4117214080864099353511039214854394855072687091691285951910149809348465)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_34 :
Polynomial.coeff recurrence2Scalar1Main 34 = 95989580213 * 10 ^ 70 + 6704367900236852189459338342404439542204670447135177274398729260034533
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_35 :
Polynomial.coeff recurrence2Scalar1Main 35 = -(2650347667847 * 10 ^ 70 + 4363517537362964151361988147257111119221767611152389626081098646389096)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_36 :
Polynomial.coeff recurrence2Scalar1Main 36 = 77832862946232 * 10 ^ 70 + 7417068631974196509983742946559945370651963717431840653679639336800276
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_37 :
Polynomial.coeff recurrence2Scalar1Main 37 = -(2343215353179504 * 10 ^ 70 + 1343541607965179749237070876193935545280025633456127243725812014602631)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_38 :
Polynomial.coeff recurrence2Scalar1Main 38 = 59524120772250411 * 10 ^ 70 + 4887121068060794630872692365678055317788819669232270992778401804175946
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_39 :
Polynomial.coeff recurrence2Scalar1Main 39 = -(948059817801156898 * 10 ^ 70 + 9501904236042326817358309685902817437973108188017265946548626667206815)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_40 :
Polynomial.coeff recurrence2Scalar1Main 40 = -(2552186954070680897 * 10 ^ 70 + 4286175996513293029626038691455261670453913804876350340762214010241343)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_41 :
Polynomial.coeff recurrence2Scalar1Main 41 = 695430214858881129297 * 10 ^ 70 + 714122320962420878876811020612541349022952881943627085897743067703635
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_42 :
Polynomial.coeff recurrence2Scalar1Main 42 = -(23419380155485433182531 * 10 ^ 70 + 2503947477078998438663450595710498197846702406202783433536011580012493)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_43 :
Polynomial.coeff recurrence2Scalar1Main 43 = 464670242570584806694477 * 10 ^ 70 + 6158566439523202601978197104795750987289907700628144823221866769946886
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_44 :
Polynomial.coeff recurrence2Scalar1Main 44 = -(6300844871831645099887089 * 10 ^ 70 + 4023566743909061528534908388124781026440054146576304197434342207337241)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_45 :
Polynomial.coeff recurrence2Scalar1Main 45 = 88054799003419434541631224 * 10 ^ 70 + 3900123982173823651791334773217235733094270038502649455199491804815619
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_46 :
Polynomial.coeff recurrence2Scalar1Main 46 = -(2691464803067863149931941531 * 10 ^ 70 + 8423329037407446935435646626640803805409701156737772821608520664618221)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_47 :
Polynomial.coeff recurrence2Scalar1Main 47 = 98868615440425352767919467385 * 10 ^ 70 + 6510853723080090769914159049722164380893815353034021255682189599603985
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_48 :
Polynomial.coeff recurrence2Scalar1Main 48 = -(2792095737168049920992795187693 * 10 ^ 70 + 384660404432817466810874308573895686015420915440852381294492783171294)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_49 :
Polynomial.coeff recurrence2Scalar1Main 49 = 60970287206435439787376454130222 * 10 ^ 70 + 8104293824427032578746618341030751544722208467306381039693460502436296
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_50 :
Polynomial.coeff recurrence2Scalar1Main 50 = -(1095898766205144908119734651348016 * 10 ^ 70 + 8427304923325742441115579812833979130255501214273090181808488212604333)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_51 :
Polynomial.coeff recurrence2Scalar1Main 51 = 16701132505900644405956119721706941 * 10 ^ 70 + 9026828776451916985226009692032777511396178226063851908440528631794428
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_52 :
Polynomial.coeff recurrence2Scalar1Main 52 = -(185792198217506512647000125855689807 * 10 ^ 70 + 9828826233062524206909930431042911054620909141253929205760279627376500)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_53 :
Polynomial.coeff recurrence2Scalar1Main 53 = -(532648834361887448162952525846528439 * 10 ^ 70 + 4009397681313590589038286826209870579203854993630744794914182247041680)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_54 :
Polynomial.coeff recurrence2Scalar1Main 54 = 124226680586890560221362090754954110420 * 10 ^ 70 + 1226824552694873181525837178623251855277747113017518090550565842031985
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_55 :
Polynomial.coeff recurrence2Scalar1Main 55 = -(5008628603416346363399313104715842809868 * 10 ^ 70 + 1998308500077039539997292445452229272624603694853126194869898424717942)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_56 :
Polynomial.coeff recurrence2Scalar1Main 56 = 143976398620895209947940638866607620117489 * 10 ^ 70 + 734637857239934386944639896837226433964703142614838897020707492735430
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_57 :
Polynomial.coeff recurrence2Scalar1Main 57 = -(3417759356268425598524790752537551923658110 * 10 ^ 70 + 1447902304290072333908537361850020299007792150900088359539154518547567)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_58 :
Polynomial.coeff recurrence2Scalar1Main 58 = 70848926596123942838280474886921236110545674 * 10 ^ 70 + 9494092833770405242903004327110661719354197522571037936219599744635656
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_59 :
Polynomial.coeff recurrence2Scalar1Main 59 = -(1322778709174206268057257202980228696443158578 * 10 ^ 70 + 9358359054833073790360433232373951443045218686050604115801062730457725)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_60 :
Polynomial.coeff recurrence2Scalar1Main 60 = 22660709697092966518527839158828478654651007579 * 10 ^ 70 + 8013314759036560213753880980410372318983761207342469298570703273882099
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_61 :
Polynomial.coeff recurrence2Scalar1Main 61 = -(359629113391084778861715201409383441003518377442 * 10 ^ 70 + 2076760657464508704756370254662171625846952967779352044593515793182354)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_62 :
Polynomial.coeff recurrence2Scalar1Main 62 = 5298519760321517447173800528159733324887340026084 * 10 ^ 70 + 5205055178798587582929030079721702857310794468284268647550370534623371
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_63 :
Polynomial.coeff recurrence2Scalar1Main 63 = -(72176403775744670061346019032557865474485281049797 * 10 ^ 70 + 9375544545085215644781271534284489391504351481799524184437196224669370)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_64 :
Polynomial.coeff recurrence2Scalar1Main 64 = 900001489129288170066131942788182352606317634380067 * 10 ^ 70 + 399016707224666185080390412937027081850175808038087234892397395209460
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_65 :
Polynomial.coeff recurrence2Scalar1Main 65 = -(10086072119495610816201955012154962200116064944656783 * 10 ^ 70 + 6572857186333802505782361165002577858170612832253832295397692081604025)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_66 :
Polynomial.coeff recurrence2Scalar1Main 66 = 97860811228733046858863620203226036898236980114696959 * 10 ^ 70 + 8030289863896854596308725172840979948220412445237966364639224236031849
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_67 :
Polynomial.coeff recurrence2Scalar1Main 67 = -(743655135514497580949540782058846005545994758703276631 * 10 ^ 70 + 4029743608036365279531802516036974562101969709168367753993149560156992)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_68 :
Polynomial.coeff recurrence2Scalar1Main 68 = 2594633835842055714197028199569958997829551893152822739 * 10 ^ 70 + 2645576311216716347952955489848672141890894007623452370953792487463280
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_69 :
Polynomial.coeff recurrence2Scalar1Main 69 = 47926469819311982078630379475983806053845686288724750369 * 10 ^ 70 + 2722861656081119515004087852248540226935728246634529961423375469127729
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_70 :
Polynomial.coeff recurrence2Scalar1Main 70 = -(1429952894272029150101227091865038038192316505411441933224 * 10 ^ 70 + 2579791382681927670397006026074993880242649769449141839999412172432725)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_71 :
Polynomial.coeff recurrence2Scalar1Main 71 = 25042414023656400537496715762783001119091515753022753730277 * 10 ^ 70 + 2798113552139974819055108802105172093627087821179811216821226971533505
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_72 :
Polynomial.coeff recurrence2Scalar1Main 72 = -(358117409025632293055897421022882221020052820153494627768194 * 10 ^ 70 + 3962227974207287006295525675057782736752763714837072656792644109022175)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_73 :
Polynomial.coeff recurrence2Scalar1Main 73 = 4529105763921921667403145270503419779007523860699585870791339 * 10 ^ 70 + 2873387399782963736501805501124315148725220038941582986437188238886514
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_74 :
Polynomial.coeff recurrence2Scalar1Main 74 = -(52315961946842683782890281473071816197482863294799643737096109 * 10 ^ 70 + 7412019718874967444026929345917169853229474765128098078895549548002368)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_75 :
Polynomial.coeff recurrence2Scalar1Main 75 = 561071544179665125521262432460805147338211005232769314111231237 * 10 ^ 70 + 2315236178485531711627171902099275187317115683852970851210427864576759
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_76 :
Polynomial.coeff recurrence2Scalar1Main 76 = -(5641138234403647416874283335759011704651422110177901282289692423 * 10 ^ 70 + 3595580657492332379615873041003832650927678714091112526883834749288759)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_77 :
Polynomial.coeff recurrence2Scalar1Main 77 = 53510784380351411584058042675456752990428369312089082345984584736 * 10 ^ 70 + 1382890718283854349087660836004393753385983349213899476997373007494355
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_78 :
Polynomial.coeff recurrence2Scalar1Main 78 = -(481069585183334979900567072423333887047278673063500331809057169935 * 10 ^ 70 + 871910168448025277687928460903430771724132038888710398709239774986352)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_79 :
Polynomial.coeff recurrence2Scalar1Main 79 = 4112796493553615662262923192518723940853126108213762762731628089772 * 10 ^ 70 + 4393840682938271095743894889876622209321438357979514606231762758329879
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_80 :
Polynomial.coeff recurrence2Scalar1Main 80 = -(33523761606097133292085217086913138088999882077940758179304982839997 * 10 ^ 70 + 6221420378787328599779277801187507192495069977499767489973449793791200)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_81 :
Polynomial.coeff recurrence2Scalar1Main 81 = 261044163304667706425859677349703023187705445136244417236039089701008 * 10 ^ 70 + 2876550957751473693838944411493339828724446966125678372436110951010704
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_82 :
Polynomial.coeff recurrence2Scalar1Main 82 = -(1944810592300583545306135957104472727549435164250704681542212777440127 * 10 ^ 70 + 8062010046087725853588103367335529351052410056585655422727101800191964)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_83 :
Polynomial.coeff recurrence2Scalar1Main 83 = (1 * 10 ^ 70 + 3878759949605777002931215768881769934474336777404513554065549224938256) * 10 ^ 70 + 3034000184276056497752357392325758290143425103584284946400322845647969
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_84 :
Polynomial.coeff recurrence2Scalar1Main 84 = -((9 * 10 ^ 70 + 4960550102132254384824658019434282775208275613380915510937480505574267) * 10 ^ 70 + 4496780986316892615456553995509828227744998792014450868439822938386941)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_85 :
Polynomial.coeff recurrence2Scalar1Main 85 = (62 * 10 ^ 70 + 3452189834112498344824294281162958716749485959450616652541674175341990) * 10 ^ 70 + 5561473837162202926431442946788513647846643945066864034062905471750766
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_86 :
Polynomial.coeff recurrence2Scalar1Main 86 = -((393 * 10 ^ 70 + 393666532922090258312884085779814997181639373840525911874628094531079) * 10 ^ 70 + 5724582889263391233384819085006797008334327316943800252934435542411298)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_87 :
Polynomial.coeff recurrence2Scalar1Main 87 = (2380 * 10 ^ 70 + 6808693995215384856285111189662462331257910196327611740287447918433565) * 10 ^ 70 + 9869053108031793457856903955337689859785322416095799045428906146297836
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_88 :
Polynomial.coeff recurrence2Scalar1Main 88 = -((13860 * 10 ^ 70 + 8620543073106564486703725697885318969624107915578771563965135804119817) * 10 ^ 70 + 3136916926442286575649313438688461237464007618430846012187270106532963)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_89 :
Polynomial.coeff recurrence2Scalar1Main 89 = (77589 * 10 ^ 70 + 30874147902910264447256154281275540668922099486798547838947261439264) * 10 ^ 70 + 9143546526333389472440519004089338972320482086399523289359418041451803
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_90 :
Polynomial.coeff recurrence2Scalar1Main 90 = -((417556 * 10 ^ 70 + 319007535294007941415738964155240658313357915663116802107771935339282) * 10 ^ 70 + 8459753598067074261212040007352160900723932885072519996135846832414351)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_91 :
Polynomial.coeff recurrence2Scalar1Main 91 = (2159764 * 10 ^ 70 + 4974053201254642808961679805238981978833929511118497200270998441844221) * 10 ^ 70 + 3772823342236850435109220911182101915461017615042370178265028095273732