Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupLeadingSquarePart0.Coefficients96To149

Recurrence 2 lookup certificate: LeadingSquare 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.recurrence2LeadingSquare_coeff_96 :
Polynomial.coeff recurrence2LeadingSquare 96 = 157846186778598447908164418970692465306467415584558434727 * 10 ^ 70 + 8128447157884899476689042547928480677143660965109184228561630879825972
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_97 :
Polynomial.coeff recurrence2LeadingSquare 97 = -(1670429066990176734232327998742154398578612149133627457689 * 10 ^ 70 + 3720401662922000921343488847023861156470370919124917429576305220827090)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_98 :
Polynomial.coeff recurrence2LeadingSquare 98 = 7725143053335460835965367296797683514233644579300017387671 * 10 ^ 70 + 5067911669526184849763609866155337930041890431314384270076861332236055
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_99 :
Polynomial.coeff recurrence2LeadingSquare 99 = -(20603394452310131154964617401398347196975129439636699403343 * 10 ^ 70 + 1785996162018714235616266223468497153518629961363489912641374411728908)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_100 :
Polynomial.coeff recurrence2LeadingSquare 100 = 15261406093131292905059057272689885263933029884955280910443 * 10 ^ 70 + 1342865675694480756557780616720085523959343634311884784694203106923463
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_101 :
Polynomial.coeff recurrence2LeadingSquare 101 = 163356324785470515027778279245006027767206694934607601267964 * 10 ^ 70 + 3113176368620682901699138952626392676860522829638632025940592993443346
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_102 :
Polynomial.coeff recurrence2LeadingSquare 102 = -(1102326691753237734382163760530621342138217551764984257815714 * 10 ^ 70 + 9727736450256423514491544259336255439251458689412594182561213377916927)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_103 :
Polynomial.coeff recurrence2LeadingSquare 103 = 4584396483976878663569583194660126858025253455187353860826006 * 10 ^ 70 + 475075755888784775599454846323587853086065878876688810808467747032230
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_104 :
Polynomial.coeff recurrence2LeadingSquare 104 = -(14548421100598952294859432809750726934168811060316681742443453 * 10 ^ 70 + 6097275216637973005367129975542385059472830216365693168472744855537050)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_105 :
Polynomial.coeff recurrence2LeadingSquare 105 = 29373365727822772651315534907765947170908203867612735218605949 * 10 ^ 70 + 9441111297606913566222959716387382354545305151612205724482111473981622
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_106 :
Polynomial.coeff recurrence2LeadingSquare 106 = 33119853375609169307101594881972325381718010916073502782035683 * 10 ^ 70 + 9981087170846709784090457454395853809781705476415923588685033252816250
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_107 :
Polynomial.coeff recurrence2LeadingSquare 107 = -(685284804867397969506277035574958163410462114861229669519407748 * 10 ^ 70 + 7365007408015039121316552526604154693879845086650303244501712971096492)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_108 :
Polynomial.coeff recurrence2LeadingSquare 108 = 3743093430141601083750949604430527541968293612345933606710459077 * 10 ^ 70 + 7436505697414459669084226242535476828966221810251772086745659793612198
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_109 :
Polynomial.coeff recurrence2LeadingSquare 109 = -(12124058065726019354730138251233727366761802976115680870295572758 * 10 ^ 70 + 8474091074526797743126596296322445472795872083649834876789133535575094)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_110 :
Polynomial.coeff recurrence2LeadingSquare 110 = 17773536928767036460537532885963490567387372039480937327616296707 * 10 ^ 70 + 6334235737908574609538108804047837503005640652103287609141659319344273
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_111 :
Polynomial.coeff recurrence2LeadingSquare 111 = 52073771648209923075933990668844144266680550152265407245473791750 * 10 ^ 70 + 4248707029660271032073164635585126160435931742792672014487583794933366
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_112 :
Polynomial.coeff recurrence2LeadingSquare 112 = -(439295910728159856955971496979837235606592925397556078319432121881 * 10 ^ 70 + 7576975876066425738256229728570143708173586108439006319863296316067675)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_113 :
Polynomial.coeff recurrence2LeadingSquare 113 = 1446903836750173139053468137495081414387795592654926675287977725060 * 10 ^ 70 + 9537264637972036066516306319811442755068509019853484140107614297089066
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_114 :
Polynomial.coeff recurrence2LeadingSquare 114 = -(2092866325862145812716324095455641809639770088505334894415880428798 * 10 ^ 70 + 5755248581907852012935952901814775196365298190982278649910928645277364)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_115 :
Polynomial.coeff recurrence2LeadingSquare 115 = -(3307688722500730860915948909298574561245873549985076619759800432378 * 10 ^ 70 + 4648429580238387640212392773461591125625320554605934272649794462494998)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_116 :
Polynomial.coeff recurrence2LeadingSquare 116 = 22218468420369964324535673889224781727985507726600152421943770600965 * 10 ^ 70 + 3977230501862702121561585632753289185806369088348618888042812324162710
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_117 :
Polynomial.coeff recurrence2LeadingSquare 117 = -(13055671636421636162079515526591490776496110134790595129118555889178 * 10 ^ 70 + 9598392539234822003856857388930033038409510835697549023939940428901924)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_118 :
Polynomial.coeff recurrence2LeadingSquare 118 = -(279779800014477396606459215756382846142641694873276805329868884778647 * 10 ^ 70 + 8029528746635877991564320465931982263080230458347220807711243653454049)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_119 :
Polynomial.coeff recurrence2LeadingSquare 119 = 1393319114033394439029819835769816224318705326995900886869257427694368 * 10 ^ 70 + 8912501832527321760409916153879472697233542915138858094130767003822902
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_120 :
Polynomial.coeff recurrence2LeadingSquare 120 = -(2472438213610324242786198977464171957645031803439339978851413313679951 * 10 ^ 70 + 2070755573060900821317347820743577414159782899862321451211016063898669)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_121 :
Polynomial.coeff recurrence2LeadingSquare 121 = -(6814088707675147899554930422067721085540997021707608564447334461376861 * 10 ^ 70 + 5944475427116201893611318460546207823563924769082237679730582020349292)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_122 :
Polynomial.coeff recurrence2LeadingSquare 122 = (6 * 10 ^ 70 + 3423570036753966360206743459199024000555822784112802400939567385026733) * 10 ^ 70 + 155210296633810079538353155240110984683065164021086506850098254003094
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_123 :
Polynomial.coeff recurrence2LeadingSquare 123 = -((22 * 10 ^ 70 + 1960907548154617623545659641519969580531095315760597439535733178547826) * 10 ^ 70 + 5366437919030372441789884648544813195800492198565141735401435334960000)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_124 :
Polynomial.coeff recurrence2LeadingSquare 124 = (34 * 10 ^ 70 + 9612944165184439303148036766982546315986163008374216009496531943587984) * 10 ^ 70 + 6527635019298971556653511055679971263613145026873267892800930454289025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_125 :
Polynomial.coeff recurrence2LeadingSquare 125 = (63 * 10 ^ 70 + 9719438783264085538409550553002109183745669353649001421797263542765112) * 10 ^ 70 + 7682031645400903767994399767816405280865468604258427561526787346229610
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_126 :
Polynomial.coeff recurrence2LeadingSquare 126 = -((604 * 10 ^ 70 + 615642135954055356341977900701838952077255321877669633645376833649151) * 10 ^ 70 + 3619934009002787473999624522352534794405780449290125472679214555288911)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_127 :
Polynomial.coeff recurrence2LeadingSquare 127 = (1952 * 10 ^ 70 + 1707632110454729277662781600251795563947306926103907226282384685516579) * 10 ^ 70 + 6889755074215391479558761148607299224829114762974382057757384830627120
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_128 :
Polynomial.coeff recurrence2LeadingSquare 128 = -((2613 * 10 ^ 70 + 3545369177609399455890395614331703802246369704296182880269184418655870) * 10 ^ 70 + 7283359220335406268953379690545375239934159721778095995408245147581345)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_129 :
Polynomial.coeff recurrence2LeadingSquare 129 = -((7091 * 10 ^ 70 + 5691864577149768926810929255568430357691676325082267752345436059414901) * 10 ^ 70 + 6336734843057492176949660243425412051882869500778933932767234410358566)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_130 :
Polynomial.coeff recurrence2LeadingSquare 130 = (55117 * 10 ^ 70 + 5694623889764030871145432116318841685712692433020241134280636991406442) * 10 ^ 70 + 5791031783297270032539055078284053524254708730354145637430735054371585
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_131 :
Polynomial.coeff recurrence2LeadingSquare 131 = -((176760 * 10 ^ 70 + 4034590504280409570926728531885847408550061124162402356471873642544606) * 10 ^ 70 + 3587716140110992780900711070724538028297719863833485704742388558025464)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_132 :
Polynomial.coeff recurrence2LeadingSquare 132 = (286009 * 10 ^ 70 + 2046735638879719840769902486434859493487410921943053844931752171039040) * 10 ^ 70 + 9036110816913150421308376503012183185535325704814288243677816683952566
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_133 :
Polynomial.coeff recurrence2LeadingSquare 133 = (275662 * 10 ^ 70 + 6186128227347169050744280682499727262922021103926008786179405074967604) * 10 ^ 70 + 2641114264806503043557665585755214944560262949271222465890255445310792
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_134 :
Polynomial.coeff recurrence2LeadingSquare 134 = -((3623464 * 10 ^ 70 + 5464072136910748223539869469800293570484387924943389890994291568748586) * 10 ^ 70 + 4775821912114220047945951446925971448353991270267780694933629703020337)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_135 :
Polynomial.coeff recurrence2LeadingSquare 135 = (13590907 * 10 ^ 70 + 4745195424752098118103703517193268842403414982506677004514271849854132) * 10 ^ 70 + 1394167966908160736082283861410363808030843663674022193708770943967368
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_136 :
Polynomial.coeff recurrence2LeadingSquare 136 = -((30245024 * 10 ^ 70 + 413615064541133901438792852709589264407368312482878403665295029387273) * 10 ^ 70 + 6922024675802288246888690380443452949953909323938873267433903664257660)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_137 :
Polynomial.coeff recurrence2LeadingSquare 137 = (25007527 * 10 ^ 70 + 7522352301898421103830143795787611488123060391563640800199516627574736) * 10 ^ 70 + 5517742950918946852479265179109352711348131893297811516653471660136760
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_138 :
Polynomial.coeff recurrence2LeadingSquare 138 = (124750169 * 10 ^ 70 + 7215321067478409163691452154640468245967876360716674413920597722133017) * 10 ^ 70 + 5010518363274600465709541149849203777141078740249228458145811924408812
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_139 :
Polynomial.coeff recurrence2LeadingSquare 139 = -((738017727 * 10 ^ 70 + 3947936090539073303376616748107206482061787932786178395077098356391322) * 10 ^ 70 + 4216401372827148516844860012725962057969097247387769875756914183025586)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_140 :
Polynomial.coeff recurrence2LeadingSquare 140 = (2318862789 * 10 ^ 70 + 4228720405061066879614481958599753494807435633363267687624221435887136) * 10 ^ 70 + 5778944569515939199929900980244875778131912911605879265443678989941987
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_141 :
Polynomial.coeff recurrence2LeadingSquare 141 = -((4839192002 * 10 ^ 70 + 1062759374922098142608987701986882614892218945552616525120573862564905) * 10 ^ 70 + 5519709293228537002744909432556539322558955854168562518293379414331722)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_142 :
Polynomial.coeff recurrence2LeadingSquare 142 = (4809602106 * 10 ^ 70 + 1338661827595414025462406821169814448229667671925164321375052813598835) * 10 ^ 70 + 8212034820825667458635825776729392236312840385836440742362631072457931
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_143 :
Polynomial.coeff recurrence2LeadingSquare 143 = (12519173615 * 10 ^ 70 + 4695317005208545369364065390327730318625002707922312563168684742511286) * 10 ^ 70 + 8140394040176269186718330663406016538496013852635235241721014444096802
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_144 :
Polynomial.coeff recurrence2LeadingSquare 144 = -((88066892556 * 10 ^ 70 + 7552921090909069505610040974415789009715718740905405632945626882074022) * 10 ^ 70 + 5330248499955107861215400167035476019069401150292329679010738810568846)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_145 :
Polynomial.coeff recurrence2LeadingSquare 145 = (305432375529 * 10 ^ 70 + 4087940249589223722023879402786940708439660669362923102388038121118301) * 10 ^ 70 + 9890232713257129213073023894348858517586720482446642819095092562375940
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_146 :
Polynomial.coeff recurrence2LeadingSquare 146 = -((774808611791 * 10 ^ 70 + 1400061978681725633010584534741957188038533809761026786215722729856771) * 10 ^ 70 + 6644980729176630721819064282424621461093659529089084128927557856591460)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_147 :
Polynomial.coeff recurrence2LeadingSquare 147 = (1474787002410 * 10 ^ 70 + 6372141496634960211141421921448609751302027119427342315804677288664001) * 10 ^ 70 + 8260390615905870445831248501843141642749154276027059874903362776491762
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_148 :
Polynomial.coeff recurrence2LeadingSquare 148 = -((1680899995858 * 10 ^ 70 + 1183219590352725847962921900759382545374071679525590875062757812356931) * 10 ^ 70 + 5663146268865874482641583156592039313815314546398006877840262174624803)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_149 :
Polynomial.coeff recurrence2LeadingSquare 149 = -((1585107786913 * 10 ^ 70 + 5550653012737987363500830326285951538596939471403320568102016159033243) * 10 ^ 70 + 3148812983325335498117729879801095408148339201654025793702354158501974)