Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupB3High

Recurrence 2 lookup certificate: B3 source coefficients, high half #

This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_72 :
Polynomial.coeff remainder3Coefficient3 72 = -(1388328 * 10 ^ 70 + 5238043731030330790713940511319626048720629589588888271371062127741683)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_73 :
Polynomial.coeff remainder3Coefficient3 73 = 3360117 * 10 ^ 70 + 3022606147947843767961852344442669454883776315937090545525310171456890
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_74 :
Polynomial.coeff remainder3Coefficient3 74 = -(4737072 * 10 ^ 70 + 6090936146674134016235557954779411823888514787882540198733169481900505)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_75 :
Polynomial.coeff remainder3Coefficient3 75 = -(2624724 * 10 ^ 70 + 9349164207924627981058158461225611093231614953451919208579934556741577)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_76 :
Polynomial.coeff remainder3Coefficient3 76 = 43858091 * 10 ^ 70 + 6870627634708516910743861745028824489961175600550351050985118436273973
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_77 :
Polynomial.coeff remainder3Coefficient3 77 = -(179070266 * 10 ^ 70 + 9589498380276133033847446918678790611709121963201680665644583381614252)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_78 :
Polynomial.coeff remainder3Coefficient3 78 = 527990088 * 10 ^ 70 + 8340514526258673613044406660446078556554308736616617662304479479782250
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_79 :
Polynomial.coeff remainder3Coefficient3 79 = -(1294338858 * 10 ^ 70 + 2705179224593434311536208709660555789228417679677276709994176807432123)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_80 :
Polynomial.coeff remainder3Coefficient3 80 = 2775345610 * 10 ^ 70 + 6047690258437353814777402512605564537582046174681702184106457413755760
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_81 :
Polynomial.coeff remainder3Coefficient3 81 = -(5336866711 * 10 ^ 70 + 5558757960545479947487715642796348842243313869284298765413118950184842)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_82 :
Polynomial.coeff remainder3Coefficient3 82 = 9338342491 * 10 ^ 70 + 4547747692476729917418390690293248150863797874617264376888690357768491
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_83 :
Polynomial.coeff remainder3Coefficient3 83 = -(15008426021 * 10 ^ 70 + 4766007516029025019068720450815586742536111508786637735926736770902335)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_84 :
Polynomial.coeff remainder3Coefficient3 84 = 22298983744 * 10 ^ 70 + 6311333400278246490275490085439078114621156373188308191957210496629154
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_85 :
Polynomial.coeff remainder3Coefficient3 85 = -(30770908587 * 10 ^ 70 + 3962394517062641398577928956726232725723719748535595804909727287053652)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_86 :
Polynomial.coeff remainder3Coefficient3 86 = 39573349213 * 10 ^ 70 + 6647448009893839264751098020944987601677521124506095793071558236422206
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_87 :
Polynomial.coeff remainder3Coefficient3 87 = -(47556504033 * 10 ^ 70 + 6437609330922112075418285296579677968383349922242309221418675982505726)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_88 :
Polynomial.coeff remainder3Coefficient3 88 = 53509432096 * 10 ^ 70 + 3488480646638594542506252603333993793146798225841484164917439507800935
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_89 :
Polynomial.coeff remainder3Coefficient3 89 = -(56458084786 * 10 ^ 70 + 4190690510083077567293854758366535306520954639804725071428367092560777)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_90 :
Polynomial.coeff remainder3Coefficient3 90 = 55923495037 * 10 ^ 70 + 1663278726519594183031856054849549265228373579997183202001302428425105
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_91 :
Polynomial.coeff remainder3Coefficient3 91 = -(52046919244 * 10 ^ 70 + 245729891983109826167165713221345673216761280993553561034618732248381)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_92 :
Polynomial.coeff remainder3Coefficient3 92 = 45537700168 * 10 ^ 70 + 7927812796731397167037375330900616752007443513407796330531380045117922
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_93 :
Polynomial.coeff remainder3Coefficient3 93 = -(37468036573 * 10 ^ 70 + 1299261936766892806590124135272301940041866259433318211287855773886541)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_94 :
Polynomial.coeff remainder3Coefficient3 94 = 28993920886 * 10 ^ 70 + 1927255211693879492053562977904542102246011966678349916340599005430064
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_95 :
Polynomial.coeff remainder3Coefficient3 95 = -(21098908481 * 10 ^ 70 + 7149769175338205653853808985071008687124120075140711826138067180319495)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_96 :
Polynomial.coeff remainder3Coefficient3 96 = 14433794727 * 10 ^ 70 + 5297024171563371299886010988785669209358853038954413551689331821253507
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_97 :
Polynomial.coeff remainder3Coefficient3 97 = -(9277620451 * 10 ^ 70 + 4688901997793636199505446776353229134476728368971836344352104289483319)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_98 :
Polynomial.coeff remainder3Coefficient3 98 = 5598843840 * 10 ^ 70 + 487964921127558627460459444195679199005768810394975681682793531194724
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_99 :
Polynomial.coeff remainder3Coefficient3 99 = -(3169045638 * 10 ^ 70 + 1798051743178479959276351563307044660311974116271001215314755904898043)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_100 :
Polynomial.coeff remainder3Coefficient3 100 = 1680225593 * 10 ^ 70 + 595853467055537199043237604617995086573765094092148094341971452703797
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_101 :
Polynomial.coeff remainder3Coefficient3 101 = -(833128963 * 10 ^ 70 + 849637918252301393369488890104479012971264621242663842813454319699453)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_102 :
Polynomial.coeff remainder3Coefficient3 102 = 385551666 * 10 ^ 70 + 5802135723426507085892522511470511019193367561640069117603190196179010
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_103 :
Polynomial.coeff remainder3Coefficient3 103 = -(166101569 * 10 ^ 70 + 9297761118541732804207642645869441274853708845063294583493587360428220)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_104 :
Polynomial.coeff remainder3Coefficient3 104 = 66401860 * 10 ^ 70 + 9132041892649150005780483092285101251834636417139194287863524890218134
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_105 :
Polynomial.coeff remainder3Coefficient3 105 = -(24528687 * 10 ^ 70 + 2579494794711164493822023948181353957641425698090298702202763332428513)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_106 :
Polynomial.coeff remainder3Coefficient3 106 = 8325256 * 10 ^ 70 + 7572990935712375096305050418191634016510237177049359517726662164307610
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_107 :
Polynomial.coeff remainder3Coefficient3 107 = -(2575608 * 10 ^ 70 + 4359140767751522153471209456351734930541495077954072566961230423326291)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_108 :
Polynomial.coeff remainder3Coefficient3 108 = 717577 * 10 ^ 70 + 9352112322493007564405383946748036764751487537894299807560164342323475
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_109 :
Polynomial.coeff remainder3Coefficient3 109 = -(176428 * 10 ^ 70 + 4169942141516794254625106998496771725351030659813117162976573989894870)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_110 :
Polynomial.coeff remainder3Coefficient3 110 = 36791 * 10 ^ 70 + 8324021014412159551117731191087868242145449506185478836464720893206693
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_111 :
Polynomial.coeff remainder3Coefficient3 111 = -(5877 * 10 ^ 70 + 610913316811161165320622211908368657604232622606418763067929277288747)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_112 :
Polynomial.coeff remainder3Coefficient3 112 = 430 * 10 ^ 70 + 2808007910672461271958621805881394611136629638456596163558895095506436
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_113 :
Polynomial.coeff remainder3Coefficient3 113 = 143 * 10 ^ 70 + 3357835678070583064988300991178019401959915876652541887820763526814519
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_114 :
Polynomial.coeff remainder3Coefficient3 114 = -(81 * 10 ^ 70 + 7802592660912823625378828639395904673124044039367492061682729383192345)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_115 :
Polynomial.coeff remainder3Coefficient3 115 = 25 * 10 ^ 70 + 6830603734648461069625921244941520037381800577978632773618583405051344
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_116 :
Polynomial.coeff remainder3Coefficient3 116 = -(6 * 10 ^ 70 + 2146558126475951742091459752987887047106399082475107324835575852357657)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_117 :
Polynomial.coeff remainder3Coefficient3 117 = 1 * 10 ^ 70 + 2478290413189209613386529064564346453881849061384461516582119428712943
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_118 :
Polynomial.coeff remainder3Coefficient3 118 = -2130607953765346486575979173587208401909940944070864743814160704988401
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_119 :
Polynomial.coeff remainder3Coefficient3 119 = 311562609388111263872074625058641185381641076702746853194821516905497
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_120 :
Polynomial.coeff remainder3Coefficient3 120 = -38960786157044998051481637794162861979218679962776265995678533141867
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_121 :
Polynomial.coeff remainder3Coefficient3 121 = 4136596077373626026460261570569508027070071107107547736180324465103
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_122 :
Polynomial.coeff remainder3Coefficient3 122 = -368471479737378690063548259471548224159713335063659997557754145579
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_123 :
Polynomial.coeff remainder3Coefficient3 123 = 27074914537599357484718731902120870451633524112286446682375692616
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_124 :
Polynomial.coeff remainder3Coefficient3 124 = -1604070201724773159251597259559365940215432279655332514103025681
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_125 :
Polynomial.coeff remainder3Coefficient3 125 = 74319461457584823064126825817146334370811950632684689276279227
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_126 :
Polynomial.coeff remainder3Coefficient3 126 = -2583260145960009593741024175832818295951192540568447153431089
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_127 :
Polynomial.coeff remainder3Coefficient3 127 = 63517628334480963461838776082852917472358213369521692408986
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_128 :
Polynomial.coeff remainder3Coefficient3 128 = -1008134748447768781584022993480510525609644882614813968103
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_129 :
Polynomial.coeff remainder3Coefficient3 129 = 8589632255858115315314958759907205405785857325245156640
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_130 :
Polynomial.coeff remainder3Coefficient3 130 = -15073910588387535089979214015962316457358706139149486
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_131 :
Polynomial.coeff remainder3Coefficient3 131 = -291052500416767275599138103498844807961572638140070
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_132 :
Polynomial.coeff remainder3Coefficient3 132 = 1674129651746526608831712981374666865668376926300
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_133 :
Polynomial.coeff remainder3Coefficient3 133 = -184976099149246181142891522461286707584146859
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_134 :
Polynomial.coeff remainder3Coefficient3 134 = -16928129819723046431748708882310310971802853
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_135 :
Polynomial.coeff remainder3Coefficient3 135 = 41524351678912399764784036074579321890738
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_136 :
Polynomial.coeff remainder3Coefficient3 136 = -37355076014988173036934365236226010977
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_137 :
Polynomial.coeff remainder3Coefficient3 137 = 12630803349999293373479468844937253
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_138 :
Polynomial.coeff remainder3Coefficient3 138 = -1353108127151867760064049878816
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_139 :
Polynomial.coeff remainder3Coefficient3 139 = 34612852489926112713304677
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_140 :
Polynomial.coeff remainder3Coefficient3 140 = -134652616023164963796
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_141 :
Polynomial.coeff remainder3Coefficient3 141 = 34032965680161
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B3_coeff_142 :
Polynomial.coeff remainder3Coefficient3 142 = -51783