Recurrence 4 lookup certificate: LeadingSquare coefficient convolution #
This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_217 :
Polynomial.coeff recurrence4LeadingSquare 217 = -((48301683586353311190834066546538797934869372262681652681 * 10 ^ 70 + 6766433316626920552027532818752376308442617859878330833860941722459376) * 10 ^ 70 + 2916945120679827676284128003840514813396830415645795436370002825720110)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_218 :
Polynomial.coeff recurrence4LeadingSquare 218 = (24093216566173387368632616370739996423407835149317026632 * 10 ^ 70 + 1646908569486428632738759641589487637251118359702920272253950613067396) * 10 ^ 70 + 1240659926648550910691118398254140804226698902107228458979359754954763
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_219 :
Polynomial.coeff recurrence4LeadingSquare 219 = -((11634967875776707200779703184680047438899699745578394664 * 10 ^ 70 + 3665067275435640215702996276237448686630695241167699497058356162760583) * 10 ^ 70 + 9297617529956802863052285531563934742393063430503334180415804354372668)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_220 :
Polynomial.coeff recurrence4LeadingSquare 220 = (5442226222184442181022090389434098931140587687063668512 * 10 ^ 70 + 3212941975014319931583593597890625019164956987962300936934450230948893) * 10 ^ 70 + 595164195662066107904580517682071005426620000539647367268258574348266
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_221 :
Polynomial.coeff recurrence4LeadingSquare 221 = -((2465108799776060159298239468653878378689171468462338266 * 10 ^ 70 + 4033922956080004122413582367714588462161857783785998194627890438878644) * 10 ^ 70 + 254881036569507116881406067943759404679147190750771959268826227231080)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_222 :
Polynomial.coeff recurrence4LeadingSquare 222 = (1080416654695396955216837384590593432977152084487628607 * 10 ^ 70 + 5351069845601064579351605469813805208994374062108528835594639777402731) * 10 ^ 70 + 8001076633225130037156676121389643820785260787219509680109800172974581
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_223 :
Polynomial.coeff recurrence4LeadingSquare 223 = -((457543485806284131044013816400958949230193828866963174 * 10 ^ 70 + 1212176691362584648481060205714136178004900882611299264566078998326938) * 10 ^ 70 + 8926132646635553798433425073844365784898365414481822551158778353662890)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_224 :
Polynomial.coeff recurrence4LeadingSquare 224 = (186835514282463161218474385329571653255473007466068745 * 10 ^ 70 + 1736990535502648469029649287251855144628759060159764860680830513223728) * 10 ^ 70 + 8583433976169974785165586435471184177310826363745540971080773570858511
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_225 :
Polynomial.coeff recurrence4LeadingSquare 225 = -((73350452192243548026873980533639164248273316908141114 * 10 ^ 70 + 8347215043818725235399138572730869609592573060580871711349733752374136) * 10 ^ 70 + 2965828945300128914676533020393090203337343216062467165316333052023910)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_226 :
Polynomial.coeff recurrence4LeadingSquare 226 = (27572018997020516490081561002710623332273845057601440 * 10 ^ 70 + 3888734135939594201927074789832156959837910715219924742158803638995549) * 10 ^ 70 + 8591416631759839059855517503321589572056126191379844836319586521784128
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_227 :
Polynomial.coeff recurrence4LeadingSquare 227 = -((9863786106060946659895243164038940582835547008739481 * 10 ^ 70 + 6268962158020213180539098267664061281320550355558310670720150515228631) * 10 ^ 70 + 4660546637758217690907648061103474862876356803521759168123542488275154)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_228 :
Polynomial.coeff recurrence4LeadingSquare 228 = (3327390662253230065263585741053257804594838508238441 * 10 ^ 70 + 34262328033077576094649164565491525339297236444574295995392376857624) * 10 ^ 70 + 9016985906538316220016824270310622904242563127019359931075899334609742
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_229 :
Polynomial.coeff recurrence4LeadingSquare 229 = -((1042080273441837026274620434825161832200176618316262 * 10 ^ 70 + 7534378460067765729379544213631771075849571508175698367657603068213755) * 10 ^ 70 + 9742534600781918019541202881550787397344244715678160996826995080833454)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_230 :
Polynomial.coeff recurrence4LeadingSquare 230 = (294141735903972541675598794454111604051753641289028 * 10 ^ 70 + 7346232118413586022497792591820616375561285177939680961970376745638991) * 10 ^ 70 + 3696038297573702563916907870919654801775277554595251981083731398111005
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_231 :
Polynomial.coeff recurrence4LeadingSquare 231 = -((69757301151839119149616984101688122321836041758324 * 10 ^ 70 + 4332869409351501319543651916850252145753528290610465769088702035746084) * 10 ^ 70 + 201442661457077328203292803245536315760737854862653905520864459214850)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_232 :
Polynomial.coeff recurrence4LeadingSquare 232 = (10698422328704931630203383659249240987334220674228 * 10 ^ 70 + 1373757185287399210843455314523946972404339149365724733598118903654697) * 10 ^ 70 + 6411824475133086503759627463383734474210153929987718537522420516703881
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_233 :
Polynomial.coeff recurrence4LeadingSquare 233 = (1356979953850069694260420975309982046995547994428 * 10 ^ 70 + 9377658407004220761627916830792815205434853015803241034857808260888672) * 10 ^ 70 + 3805743759958373153469129447085670773656527631958735379191888274528044
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_234 :
Polynomial.coeff recurrence4LeadingSquare 234 = -((2187898632086072669765957228404204122600800525894 * 10 ^ 70 + 8273195283863500947014341580921937259053540796906149344259232886493019) * 10 ^ 70 + 5295866940852682412749839596665464288332940593064468438027492362991758)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_235 :
Polynomial.coeff recurrence4LeadingSquare 235 = (1277816701540295082897364844916533770982724376376 * 10 ^ 70 + 5536827200072258773751221782701161940634733913862976040301710424489730) * 10 ^ 70 + 8142230156759574306179911089994000499076544364263951490789741007775896
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_236 :
Polynomial.coeff recurrence4LeadingSquare 236 = -((577510491766728576647334737969185702025823382398 * 10 ^ 70 + 9737845706284430134284707483358877161037015399578535806495267709370024) * 10 ^ 70 + 4489163116976033864509274350570459948278984340358298226142119690700602)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_237 :
Polynomial.coeff recurrence4LeadingSquare 237 = (226335984191438391201701292385604159407366477915 * 10 ^ 70 + 8171223627044796790598385197882056530655783540740513040180653913736191) * 10 ^ 70 + 9913357034217465001681479128972203185904311209083391722417391803572366
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_238 :
Polynomial.coeff recurrence4LeadingSquare 238 = -((79648411145801183209372473226741802496692629164 * 10 ^ 70 + 5175424143104495514808915443212401617679447022970479913754385401606201) * 10 ^ 70 + 3478615753608091916893215821174545184697309890708848039746486837985956)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_239 :
Polynomial.coeff recurrence4LeadingSquare 239 = (25340169337212719312257500430828255890530738381 * 10 ^ 70 + 1384466588995233411081456477540927575349131185347917409720284013035625) * 10 ^ 70 + 2700762255881772524070097615191039079509682982866300128940098224319758
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_240 :
Polynomial.coeff recurrence4LeadingSquare 240 = -((7173465154104085860331003750167322418113094192 * 10 ^ 70 + 3134916351181252165802645152999419722442259801051704237771838049736923) * 10 ^ 70 + 1269809166469419063623986418544404180777525979322647184412335409161806)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_241 :
Polynomial.coeff recurrence4LeadingSquare 241 = (1698876651408819349440568767394749332995193260 * 10 ^ 70 + 3017688737393751981508609409980090511444743392990176648592547716755437) * 10 ^ 70 + 8136659518758265552187763018577203090208661116673163949509411407521774
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_242 :
Polynomial.coeff recurrence4LeadingSquare 242 = -((258028669874922555141849154914948531531143068 * 10 ^ 70 + 4185002420862762208270501550420846948854391443655219083016159429884023) * 10 ^ 70 + 8291426642499723222070565953119665989206108824628475345746537603177036)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_243 :
Polynomial.coeff recurrence4LeadingSquare 243 = -((38135404313704202673643798871465364499112633 * 10 ^ 70 + 3595482093135690549096720891169163075886847219251028977950712098162354) * 10 ^ 70 + 828411257292884179088003057531966676919118051127322508216469366229928)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_244 :
Polynomial.coeff recurrence4LeadingSquare 244 = (59734163286858137181817486877296014763373384 * 10 ^ 70 + 1760074355016729546754166240576593299999875147884788495396009949473132) * 10 ^ 70 + 4736739783631726080470501376985246673371637875967456242665297441315642
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_245 :
Polynomial.coeff recurrence4LeadingSquare 245 = -((36950416214128490212349369616234088842314699 * 10 ^ 70 + 7937770025912132248673896929661582681831539065424445432842951779492486) * 10 ^ 70 + 1264391037193204330437217860367342617044860801250676466763306675423176)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_246 :
Polynomial.coeff recurrence4LeadingSquare 246 = (18248522266597075142797297626612555868278423 * 10 ^ 70 + 5355866542985201301979270670978220616999755525236248257301986789879521) * 10 ^ 70 + 6984533006018987394775679445467939829791018643935999879823161056193044
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_247 :
Polynomial.coeff recurrence4LeadingSquare 247 = -((8055925369670958836565011096383408302769762 * 10 ^ 70 + 2197859761516452868020194188484721838975774366184712266581142456388709) * 10 ^ 70 + 8964639350534164149820331257568324997294799557849004600290900043185134)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_248 :
Polynomial.coeff recurrence4LeadingSquare 248 = (3303358796667169242072138135497849002249370 * 10 ^ 70 + 8542946355904278356391972704929879756478874033661941931600568713269966) * 10 ^ 70 + 9902215613607257913742423408451127996352377203699121715219939025867094
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_249 :
Polynomial.coeff recurrence4LeadingSquare 249 = -((1278484688740372886546168658312401438064294 * 10 ^ 70 + 9144948454214835618964753958380741902132379083308684218492318165970949) * 10 ^ 70 + 1903589423481883932809440808930995838813875966492399353228625727793712)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_250 :
Polynomial.coeff recurrence4LeadingSquare 250 = (470138887996661974735376645374857914551367 * 10 ^ 70 + 6057712251240985076990272319199005019744482851105622985801828335792455) * 10 ^ 70 + 5343593201009107219869170205681939150584155516427621843475428436576789
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_251 :
Polynomial.coeff recurrence4LeadingSquare 251 = -((164544163191224738147058766609017939163831 * 10 ^ 70 + 9780593611452194163646029210642185814675821336937300339601711899781935) * 10 ^ 70 + 2501575891864956754917897045872894347620059423788879461092334134957618)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_252 :
Polynomial.coeff recurrence4LeadingSquare 252 = (54704517564068850334116312370239481653997 * 10 ^ 70 + 7317138072052655232059693396377100800116380849676586988246048393310951) * 10 ^ 70 + 8582372297185505932721437206853128631802049403470144723737853115146962
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_253 :
Polynomial.coeff recurrence4LeadingSquare 253 = -((17174242424763704066846818173457531031785 * 10 ^ 70 + 1805455673394700875682585630646390359499226067578541719550201145458015) * 10 ^ 70 + 9673618630167568701175693534502847015347853567398400569388319552177882)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_254 :
Polynomial.coeff recurrence4LeadingSquare 254 = (5030344123167268553006210486394499626029 * 10 ^ 70 + 1965192448883004677936527687895510834754258827088651253200751021044405) * 10 ^ 70 + 535010667741323358696784724913071338402535353692927514191132633458168
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_255 :
Polynomial.coeff recurrence4LeadingSquare 255 = -((1341605559374980456473750047628504408089 * 10 ^ 70 + 6654621921636803413906733082327756053769564253579520223537590109146588) * 10 ^ 70 + 1260931267207237585430900218591489225792350640693572475820619443579456)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_256 :
Polynomial.coeff recurrence4LeadingSquare 256 = (308142034316075907110093010684945385238 * 10 ^ 70 + 1152036472428270852420567875473275427292273764597343362517201412169998) * 10 ^ 70 + 6589517508955064504984670998901097305963004884587480272591587069098425
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_257 :
Polynomial.coeff recurrence4LeadingSquare 257 = -((50911662331316659281509188252154254661 * 10 ^ 70 + 9671203364048383514738810638220613144716787905961663921770358855669260) * 10 ^ 70 + 2423466363005084817294606517645323484708243924985953793441001200095692)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_258 :
Polynomial.coeff recurrence4LeadingSquare 258 = -((574186009104048688978227298701855868 * 10 ^ 70 + 6464632530820291052208130890460484552878936252806683913962563975890103) * 10 ^ 70 + 6516093241494538100535483005055785963010393628565651921026346454862899)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_259 :
Polynomial.coeff recurrence4LeadingSquare 259 = (5578668773984236591091009196510017645 * 10 ^ 70 + 8999249563864875742830357087007609452850480638803261688526505094402288) * 10 ^ 70 + 7702568928516920617608291215583564483568382458492442507898480978357092
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_260 :
Polynomial.coeff recurrence4LeadingSquare 260 = -((3334112660647948060575286417910211398 * 10 ^ 70 + 7651907855022458592531008900445434367523684297426857641417032228124720) * 10 ^ 70 + 5948763890431048923864495227524428533600508031678286034497707629567942)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_261 :
Polynomial.coeff recurrence4LeadingSquare 261 = (1455768857478374444014651615142791987 * 10 ^ 70 + 6830811326724179512477290716215888118500591738744504196790363291984189) * 10 ^ 70 + 5158962923358532380026370955869923661703683711100039827203700552434410
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_262 :
Polynomial.coeff recurrence4LeadingSquare 262 = -((545044450038199306489132070840234251 * 10 ^ 70 + 3924424866766999831658997047259623956915413462849598760375293488014315) * 10 ^ 70 + 5344256197727913316517825041066732081144577987877587266516353125509603)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_263 :
Polynomial.coeff recurrence4LeadingSquare 263 = (183721024687946961337704768433862225 * 10 ^ 70 + 8521529644921271095100586702880714206389371424107778026763234004351546) * 10 ^ 70 + 683034661267868638055431137389473970732495100854206676515090717151762
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_264 :
Polynomial.coeff recurrence4LeadingSquare 264 = -((56678292895620847571572813203507415 * 10 ^ 70 + 212615416121228937855683161144890322265702602585470854359499563289961) * 10 ^ 70 + 8850328713233594771633016095512339774948271537466366827591929773336191)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_265 :
Polynomial.coeff recurrence4LeadingSquare 265 = (15941262851573140534019573045660360 * 10 ^ 70 + 944166358771266867303326432388661403236963035216827780138522054578531) * 10 ^ 70 + 1729579863340965506408134596030603710526744834452347525558413163829008
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_266 :
Polynomial.coeff recurrence4LeadingSquare 266 = -((3953267780498142550257384714043971 * 10 ^ 70 + 1834059623786669298691571819313447859796415947366391712903435609202176) * 10 ^ 70 + 8734474365554066791052758579723958042265026360162179282358710673127788)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_267 :
Polynomial.coeff recurrence4LeadingSquare 267 = (766892369303211169671441666501498 * 10 ^ 70 + 367261518632822623423600771744624257479045595235285693655530353148234) * 10 ^ 70 + 5261151465305579970057120273901355400706245110276001779398700918554636
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_268 :
Polynomial.coeff recurrence4LeadingSquare 268 = -((48072498642739110898786226971134 * 10 ^ 70 + 3844869347445869772000763398748001749206199136276406287102896372700778) * 10 ^ 70 + 4069345588104466708594022116585772453270303866031774831257512275216206)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_269 :
Polynomial.coeff recurrence4LeadingSquare 269 = -((58080386054114705175765005529005 * 10 ^ 70 + 5710310171084920914007420747272214652558339974890808652278204354717063) * 10 ^ 70 + 6395625081101474708619572645258651026191200912840574180357884510624062)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_270 :
Polynomial.coeff recurrence4LeadingSquare 270 = (44521501645932358387402491497651 * 10 ^ 70 + 1746618052231392041759640060399553650616463268818241193757677490775830) * 10 ^ 70 + 9908076144595218649648175528314173087312265359600310589131862066668773
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_271 :
Polynomial.coeff recurrence4LeadingSquare 271 = -((22952261970391898698392704459081 * 10 ^ 70 + 6812156067680055994476223993403945376417390723514408448067566525352757) * 10 ^ 70 + 7877550128686187284625895739021501400918327903946343553032020190593340)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_272 :
Polynomial.coeff recurrence4LeadingSquare 272 = (10122461015220483253867581322286 * 10 ^ 70 + 3808353127084238359400328243600115387765516379970859688249924474044741) * 10 ^ 70 + 8686831950385050515760309760341609487821545969952658731862767789259513
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_273 :
Polynomial.coeff recurrence4LeadingSquare 273 = -((4078468639387832061993873054170 * 10 ^ 70 + 1315650817977266988024870976931737535632801287385431956248721731958537) * 10 ^ 70 + 8195105717597863808537723357415919744218725053903421743319202191981190)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_274 :
Polynomial.coeff recurrence4LeadingSquare 274 = (1542268978599714547719110761198 * 10 ^ 70 + 7343392751782459136743796641247670993018411279847251985765011486984497) * 10 ^ 70 + 6510200429684408848744089431231372521773281929270730796220522786241769
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_275 :
Polynomial.coeff recurrence4LeadingSquare 275 = -((554280908756674928419392652157 * 10 ^ 70 + 4081640091510426882318701139257758736083797561739204261634844276557759) * 10 ^ 70 + 5501901233976921968827968822123054901653009791207224014513147442443858)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_276 :
Polynomial.coeff recurrence4LeadingSquare 276 = (190380601057782506908449348647 * 10 ^ 70 + 342450857566265762870245846720024150353546525064515238212168173840461) * 10 ^ 70 + 9814305985146992539367056841919876415106936717513567013255825498024470
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_277 :
Polynomial.coeff recurrence4LeadingSquare 277 = -((62599117109886620794378052715 * 10 ^ 70 + 1196906821022107757011110780208084346488703106896774423798381985688554) * 10 ^ 70 + 9264222501682931558048847240924956805306726471740759029874534839981648)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_278 :
Polynomial.coeff recurrence4LeadingSquare 278 = (19694568437178122814253513316 * 10 ^ 70 + 8394229879795067756925778384768204842654589793671597378939521825686360) * 10 ^ 70 + 7153961166288385468443728217913439515838527984850879843912224346682176
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_279 :
Polynomial.coeff recurrence4LeadingSquare 279 = -((5918942964183119052958189008 * 10 ^ 70 + 7342992400360799440162157172124518284697427307453465032252990020837111) * 10 ^ 70 + 3783557644155988241374030826113527431944656146378681134591321153498034)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_280 :
Polynomial.coeff recurrence4LeadingSquare 280 = (1695649302820669129330498759 * 10 ^ 70 + 6461903114954060796125462570509336052790442307798937406581569922960427) * 10 ^ 70 + 192446835191285881760159521088132637219268982971366232028879233331636
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_281 :
Polynomial.coeff recurrence4LeadingSquare 281 = -((461999393161967501771354651 * 10 ^ 70 + 4959452704497053233963000343947176414707262148817915407555066158783376) * 10 ^ 70 + 8424730623528663979899715676262739573980066332059808078329188615989472)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_282 :
Polynomial.coeff recurrence4LeadingSquare 282 = (119451949604813817865202471 * 10 ^ 70 + 5161213903776152066887100537313408202691622567615654535507313861430529) * 10 ^ 70 + 4999207593450708661545048330327703007492182360610871011037898070205901
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_283 :
Polynomial.coeff recurrence4LeadingSquare 283 = -((29244970562886960795673399 * 10 ^ 70 + 2901012461385279094548165313112450960898681421393981587160772078794418) * 10 ^ 70 + 8805705355418529919209630045111211920695801794051948107399256743676882)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_284 :
Polynomial.coeff recurrence4LeadingSquare 284 = (6765221369495189324079888 * 10 ^ 70 + 1160289132511444932672873449456386230345585477992657863858511836869806) * 10 ^ 70 + 874579998026914122868117081397781552843159016632761268236524820659060
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_285 :
Polynomial.coeff recurrence4LeadingSquare 285 = -((1475448547878403200060148 * 10 ^ 70 + 6814222860669077437287494930949892086173042224234184096470217698388343) * 10 ^ 70 + 9226442704938463583174088460508036178392392694575751678240564219044646)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_286 :
Polynomial.coeff recurrence4LeadingSquare 286 = (302654078777630204714546 * 10 ^ 70 + 4358998162296185008913817888963156929822698146488899478862138986372066) * 10 ^ 70 + 6933180931336054894913362245572971118593097268356780348283853479286004
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_287 :
Polynomial.coeff recurrence4LeadingSquare 287 = -((58238450266995685155655 * 10 ^ 70 + 3787543609657986333508687856603131952917480400435599030403815421844585) * 10 ^ 70 + 4965075340818367395513351304100599533920021224780554537115901934037196)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_288 :
Polynomial.coeff recurrence4LeadingSquare 288 = (10481663149626812092189 * 10 ^ 70 + 7804350972734008760725525884244019458867937409394470081820004922124789) * 10 ^ 70 + 1329009947913932855900008173383201528478235506124799217321004107895744
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_289 :
Polynomial.coeff recurrence4LeadingSquare 289 = -((1758526262210859554112 * 10 ^ 70 + 5105626005878662583436209303545463588614700747105183489631728545348543) * 10 ^ 70 + 6290327784864622836697683809237634635167535603947754712279874636119864)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_290 :
Polynomial.coeff recurrence4LeadingSquare 290 = (273969934025153770595 * 10 ^ 70 + 7456811772330498773637642418937815078685873668449008759712655260869811) * 10 ^ 70 + 1365283298216877735336627051077938337279028800451563302834096389346671
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_291 :
Polynomial.coeff recurrence4LeadingSquare 291 = -((39463404540982304115 * 10 ^ 70 + 2840729307440414769911907200915892049564714523975714815767165105061040) * 10 ^ 70 + 7934784633772434205867729707790874479120638008854858824326902046166190)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_292 :
Polynomial.coeff recurrence4LeadingSquare 292 = (5229414189201611741 * 10 ^ 70 + 3716208942460500640744006023284100592023587951659596469786587219766177) * 10 ^ 70 + 3909399734859177476338441963174293567022899108390776586916896860554297
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_293 :
Polynomial.coeff recurrence4LeadingSquare 293 = -((633845387183558878 * 10 ^ 70 + 9199672629182752492799354246078231801479410285461333085054363829963082) * 10 ^ 70 + 4645745548157280173767049389857032874154880073112961469131170896588404)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_294 :
Polynomial.coeff recurrence4LeadingSquare 294 = (69806284288509420 * 10 ^ 70 + 9560213536261259621804292352403006764608915082908526639799565365037631) * 10 ^ 70 + 5722542392041327429791704155141829829559786060833095711999389927629977
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_295 :
Polynomial.coeff recurrence4LeadingSquare 295 = -((6931057780659151 * 10 ^ 70 + 2047498751079061699422210273318695820717479795422234758137255025608459) * 10 ^ 70 + 1276194635041047070545349758317066266198193596051453396109224594500396)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_296 :
Polynomial.coeff recurrence4LeadingSquare 296 = (614715863798566 * 10 ^ 70 + 9494460432831125133625257992144350067828909366587238516187844586923137) * 10 ^ 70 + 4446502443216354619274533839157310773473202480608701144151773461333427
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_297 :
Polynomial.coeff recurrence4LeadingSquare 297 = -((48157068228405 * 10 ^ 70 + 2701810787263081337791567371729838829306502890256082209462312606505834) * 10 ^ 70 + 6075982186912188641820533800227722216405635993570993782061372713798580)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_298 :
Polynomial.coeff recurrence4LeadingSquare 298 = (3286827349838 * 10 ^ 70 + 7225916710738763496753209552819384659514463355623220742938410489868177) * 10 ^ 70 + 6627554129305416424788557909965027780118606618665512914729831862716444
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_299 :
Polynomial.coeff recurrence4LeadingSquare 299 = -((192089079007 * 10 ^ 70 + 1969338356489078373357762435889063287228861224309344759110154138833234) * 10 ^ 70 + 9851493333403677501754571364466956906753167710673987151226724187473046)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_300 :
Polynomial.coeff recurrence4LeadingSquare 300 = (9399708580 * 10 ^ 70 + 9243121967758831171504504339871085030370588618559514721066881414170775) * 10 ^ 70 + 5841757850458586364106618202119478896469971263380817028479068712264709
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_301 :
Polynomial.coeff recurrence4LeadingSquare 301 = -((373755627 * 10 ^ 70 + 8147347608710570688531307420560735247905797751427616003957751283687667) * 10 ^ 70 + 3271776295228360451051967273530194858470183137401407991580911383983580)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_302 :
Polynomial.coeff recurrence4LeadingSquare 302 = (11575777 * 10 ^ 70 + 9814599602151425079968707566788103547489491208816553136990129267197878) * 10 ^ 70 + 7629472352946818604818304923689918020150317870046300430677685955811321
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_303 :
Polynomial.coeff recurrence4LeadingSquare 303 = -((261694 * 10 ^ 70 + 4242677505594319933698639285251104172195265031434906540912523530194674) * 10 ^ 70 + 4868512975174056605108806998111597416646769841043349044332357322010704)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_304 :
Polynomial.coeff recurrence4LeadingSquare 304 = (3839 * 10 ^ 70 + 5112050897449543659250277204485963495740658861527567230192019895921378) * 10 ^ 70 + 8123978817539029311280896976948534750687766546308232012781742173484114
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_305 :
Polynomial.coeff recurrence4LeadingSquare 305 = -((26 * 10 ^ 70 + 4474039972910565838052603047929525215008676546368240032243117378540226) * 10 ^ 70 + 5333815919415776002778368297253590920793285517254534228486580747151222)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_306 :
Polynomial.coeff recurrence4LeadingSquare 306 = -(937433506104227471393748967511953799678356274990619109995157688579351 * 10 ^ 70 + 5803649828711483924039227039398330657924892131161670532901997506589812)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_307 :
Polynomial.coeff recurrence4LeadingSquare 307 = 25993103418066985617822222331691928534433551155115168043121016655876 * 10 ^ 70 + 3080628030693263157967154793434253987100698266568364240141677238991018
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_308 :
Polynomial.coeff recurrence4LeadingSquare 308 = -(79188936327513919866752083172769693709328446061569890576571553326 * 10 ^ 70 + 5091902987070446415739796213514701779832864883322838339645867449733542)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_309 :
Polynomial.coeff recurrence4LeadingSquare 309 = -(625584334897587809044914756931576755282454844020749915023661940 * 10 ^ 70 + 6324517527199252377178483028419406473470364763600115782971504372094742)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_310 :
Polynomial.coeff recurrence4LeadingSquare 310 = 3535026303961947425808689691962913211671356946009334892524920 * 10 ^ 70 + 8523945221329146445487948697198119371337803485295592256566049764889063
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_311 :
Polynomial.coeff recurrence4LeadingSquare 311 = 2755404344530431856213457165457351666040131708548581351891 * 10 ^ 70 + 8598431588982605150721058880833009242069264307139896895606750330963164
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_312 :
Polynomial.coeff recurrence4LeadingSquare 312 = -(47513713868037048200876314139975885644575788628414207444 * 10 ^ 70 + 6884346110801441112941905109076140714773923712457380407245606534967605)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_313 :
Polynomial.coeff recurrence4LeadingSquare 313 = 69952752977058559634686574631001659966011705678281149 * 10 ^ 70 + 3026967103996441368854280329311313239307791317403279693782263545813322
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_314 :
Polynomial.coeff recurrence4LeadingSquare 314 = 149909517188307078121606304917827767429010422933656 * 10 ^ 70 + 8023817422379335841935952656127065771965346568761314816410766868616799
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_315 :
Polynomial.coeff recurrence4LeadingSquare 315 = -(602953141586486985811567593177822596796161489808 * 10 ^ 70 + 5544246356046565852266195404404352770160150161739938281027403937616370)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_316 :
Polynomial.coeff recurrence4LeadingSquare 316 = 808726760972795614457223427656192202615119131 * 10 ^ 70 + 3116387326760182629529323290063713031863425233161848087531768478288812
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_317 :
Polynomial.coeff recurrence4LeadingSquare 317 = -(544505801333708889402628326164057376240395 * 10 ^ 70 + 2897015696681291611822817939298425879357386504627771232557829632559702)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_318 :
Polynomial.coeff recurrence4LeadingSquare 318 = 194964409002729381555431851899968787852 * 10 ^ 70 + 2029935872165317440585893475663173733689245933194966321416325250165218
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_319 :
Polynomial.coeff recurrence4LeadingSquare 319 = -(36509083097803262436104081023829972 * 10 ^ 70 + 3304129092544908279450638911405225780478534690342960433969123674111304)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_320 :
Polynomial.coeff recurrence4LeadingSquare 320 = 3476408299107804651543331965290 * 10 ^ 70 + 6071056074221424024120914087442208907376150534546815806931392027499127
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_321 :
Polynomial.coeff recurrence4LeadingSquare 321 = -(157836352738029978700968527 * 10 ^ 70 + 9979867435919201664910418608124239477841212685064215038592859470768954)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_322 :
Polynomial.coeff recurrence4LeadingSquare 322 = 3283541447647637420673 * 10 ^ 70 + 9560151338221273107522710557452491861497630329586840292210065399626187
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_323 :
Polynomial.coeff recurrence4LeadingSquare 323 = -(27685621699707067 * 10 ^ 70 + 7911923049586780301925861014365666926507197652274744283673423370550416)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_324 :
Polynomial.coeff recurrence4LeadingSquare 324 = 92390336030 * 10 ^ 70 + 4862674184059383380194461061521389401939160748837053599620802961376459
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_325 :
Polynomial.coeff recurrence4LeadingSquare 325 = -(92635 * 10 ^ 70 + 1053503340676856800368102710160145593663195394413934181959839690562070)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_326 :
Polynomial.coeff recurrence4LeadingSquare 326 = 304717060906988227195731028688210479477394036078029906072821559728989
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_327 :
Polynomial.coeff recurrence4LeadingSquare 327 = -14966805652273259687694045024995476360256283255894241831875660
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_328 :
Polynomial.coeff recurrence4LeadingSquare 328 = 199944508519179168873514110594451712887216908764160100