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_67 : Polynomial.coeff recurrence4LeadingSquare 67 = -((10825190616939704997447355 * 10 ^ 70 + 8211179006893203856342581955328764598527985091313486445381554470094062) * 10 ^ 70 + 6214993600708324796821844815826433071961133232933447659344114910505604)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_68 : Polynomial.coeff recurrence4LeadingSquare 68 = (118533709488669808349652447 * 10 ^ 70 + 499472392943932522872702693471261423005140852865127914981644343275112) * 10 ^ 70 + 7711635852661516090290240932307215259562371212857638431476076237491697

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_69 : Polynomial.coeff recurrence4LeadingSquare 69 = -((1236783883198566475426153712 * 10 ^ 70 + 3060258314537551798177648041400944758988323387561644132363132794051120) * 10 ^ 70 + 7226908589573750745776275185606369335713116178542094673802444002754702)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_70 : Polynomial.coeff recurrence4LeadingSquare 70 = (12324616775014453059658391841 * 10 ^ 70 + 109640590312846582141519131056648830260188232206081568284356824419590) * 10 ^ 70 + 9752187882985703294528994392473248359366958159916182289603603216548308

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_71 : Polynomial.coeff recurrence4LeadingSquare 71 = -((117518149462740668527966334030 * 10 ^ 70 + 8644798158954764064494547903605507601028460245966919156001841665854382) * 10 ^ 70 + 9720635214980388580826371572159082903313818990705146047568318795941016)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_72 : Polynomial.coeff recurrence4LeadingSquare 72 = (1073976470745713767517014733895 * 10 ^ 70 + 6537396547155318159202252965631537977745619801461019078847409034135444) * 10 ^ 70 + 1627976035860434396553520614418769741861482368792901547448579916282963

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_73 : Polynomial.coeff recurrence4LeadingSquare 73 = -((9420170553458137521542643077315 * 10 ^ 70 + 1159578646732249376791986830386620796270297390581005142219475782244716) * 10 ^ 70 + 7734824376684834673531029047846591697181927125929205502037463975674160)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_74 : Polynomial.coeff recurrence4LeadingSquare 74 = (79403855380629573690349110019263 * 10 ^ 70 + 3685607299199232507765489880107204463422803450753683556909660670886263) * 10 ^ 70 + 6137978215745583985631597541060069518948951404259125783984462164218564

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_75 : Polynomial.coeff recurrence4LeadingSquare 75 = -((643918094023282498155839848433966 * 10 ^ 70 + 8703633217394536472061228110684214670839304442644609365515740950972168) * 10 ^ 70 + 2721329106442750182927801943030532268283826407893535986191050754707668)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_76 : Polynomial.coeff recurrence4LeadingSquare 76 = (5028823145706774086805009233585213 * 10 ^ 70 + 6433613085876441128904193414900926982248711344649669425983429644150511) * 10 ^ 70 + 2090676790787952503253865677862911779069311775822256444167084339672574

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_77 : Polynomial.coeff recurrence4LeadingSquare 77 = -((37857347169172669406882482515506731 * 10 ^ 70 + 4388726581991606403994477954083118172326179114725723423339869548663565) * 10 ^ 70 + 4615333540318785386576873696726255882934502608131653331994532915360306)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_78 : Polynomial.coeff recurrence4LeadingSquare 78 = (274947886176762820381285841479499957 * 10 ^ 70 + 3865301967018559564073723497945672053107750458565466738378339606263772) * 10 ^ 70 + 9667094442543903359838842156400218303856207193967654746438706004833300

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_79 : Polynomial.coeff recurrence4LeadingSquare 79 = -((1927999523016928427581929226143956845 * 10 ^ 70 + 8816621773633776955624063705238888590393608882513685298045523317812505) * 10 ^ 70 + 188069623676898446479847740542975242732195900317594412969511218650088)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_80 : Polynomial.coeff recurrence4LeadingSquare 80 = (13062764097208551746853395050264234350 * 10 ^ 70 + 8871632529578972211133928717396167454567939641239690007474930043966493) * 10 ^ 70 + 7360200751566980854305243055761902548432658140994230481507533467653522

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_81 : Polynomial.coeff recurrence4LeadingSquare 81 = -((85571377401899485845534406150698980948 * 10 ^ 70 + 1395865576131313624267599542668080904049553697398520938901896905595348) * 10 ^ 70 + 1852982632731724357160093193536342972667845949498501290652065558771734)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_82 : Polynomial.coeff recurrence4LeadingSquare 82 = (542327576584186814737309305524569304954 * 10 ^ 70 + 698693912005233427221370489213957187678694333988286042060358627941090) * 10 ^ 70 + 9489397233689123817264556698289201942701245199067071537037701713289355

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_83 : Polynomial.coeff recurrence4LeadingSquare 83 = -((3327299058362642892536710153236172786187 * 10 ^ 70 + 2226706509250001996661183063408368354992029039162212587152358551981022) * 10 ^ 70 + 1873870230048963288345612819287219604946238347292543203310822361558568)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_84 : Polynomial.coeff recurrence4LeadingSquare 84 = (19772459902080243603177205932199551155847 * 10 ^ 70 + 6336244526579378741154528894694529668947378956362379182876426300119056) * 10 ^ 70 + 4323008720568493605866802666314735410914142573992961126834115580494444

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_85 : Polynomial.coeff recurrence4LeadingSquare 85 = -((113866482153954838984673694957877119654173 * 10 ^ 70 + 1502616598896440401560430917597828378837508699713273196978694506701633) * 10 ^ 70 + 1559240276684061309495147296277810667567243164047503889712148750398604)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_86 : Polynomial.coeff recurrence4LeadingSquare 86 = (635787706957963195244847539490817137894928 * 10 ^ 70 + 6387847890637164610748256879812191796473170318692618921251959293853725) * 10 ^ 70 + 7263005456716951081182387575445079019140082376707334950763617563206775

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_87 : Polynomial.coeff recurrence4LeadingSquare 87 = -((3443595677585662928971715051826476022578928 * 10 ^ 70 + 2982919053131278840503666579472600367611139931999064450733286896521354) * 10 ^ 70 + 4553761137177880013547064228803510775720071389091706509891868470694450)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_88 : Polynomial.coeff recurrence4LeadingSquare 88 = (18100381990765664787367057918050935105425019 * 10 ^ 70 + 947789006651775955224746932667740080139136751021977909008701847094053) * 10 ^ 70 + 9962051052752567888373760443474236734899841576104083741282494289324129

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_89 : Polynomial.coeff recurrence4LeadingSquare 89 = -((92367752935442866396609530301228298362998651 * 10 ^ 70 + 6025321433719699700327297578688613454445311237961758893210346642929858) * 10 ^ 70 + 7956936933951820975167348960965538174880941425315892143074448000228250)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_90 : Polynomial.coeff recurrence4LeadingSquare 90 = (457806519183626738408938688562838085347895753 * 10 ^ 70 + 5362783499739549714712136943378022231917158272362124832298029290803783) * 10 ^ 70 + 5470418908918067384510493329323799282772775700102821330983999547743889

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_91 : Polynomial.coeff recurrence4LeadingSquare 91 = -((2204628578028991654002262591059919288247262362 * 10 ^ 70 + 3195856080369869064148670370423734163693235636587064062014067723591830) * 10 ^ 70 + 5277549535883856549035105296497859346757953352707403073669482706989146)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_92 : Polynomial.coeff recurrence4LeadingSquare 92 = (10318942753419855700588519582831043173814225768 * 10 ^ 70 + 9629866606457071811483490536605549051905316698275225772810269397402283) * 10 ^ 70 + 1340567092585591059249726810102350630770934477962151392809917574021625

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_93 : Polynomial.coeff recurrence4LeadingSquare 93 = -((46959962126852759729356954327744168782915244504 * 10 ^ 70 + 5606214595230155805949010505151851154553648006606074106466858625527035) * 10 ^ 70 + 3077240305775705761195539667976655460220992504551493440849155882044892)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_94 : Polynomial.coeff recurrence4LeadingSquare 94 = (207850909640583460205928355907956912457396209518 * 10 ^ 70 + 9499471421216904749596476681198345653058793414740580216079151995228510) * 10 ^ 70 + 5859413480374580324877194745141087976073461623186918168328631456146326

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_95 : Polynomial.coeff recurrence4LeadingSquare 95 = -((895033924605611575721077205407008485052290869589 * 10 ^ 70 + 7973629344439624202817273637319831139290594911431041540531355648859840) * 10 ^ 70 + 5812403667930276471440051651699372042747219572050669657741580001412614)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_96 : Polynomial.coeff recurrence4LeadingSquare 96 = (3750726016612099671120043584572220071840959498765 * 10 ^ 70 + 893066291316169359994107281752349921607769935243356771598467090418108) * 10 ^ 70 + 2762588132811719307020899284002397573153199085067515938345374606611020

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_97 : Polynomial.coeff recurrence4LeadingSquare 97 = -((15300226888036302197706370099693500426900610128474 * 10 ^ 70 + 534085847952808091122805885766919282298366547831709076394479710503637) * 10 ^ 70 + 6571013163716057354746893424113331048954673646414377334483325362076198)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_98 : Polynomial.coeff recurrence4LeadingSquare 98 = (60771408805166216512274812615945960814251061148003 * 10 ^ 70 + 5504057762802868615781813644650884718503765897059340511620801844917421) * 10 ^ 70 + 524444704702715243701594705205520513043852217147158913478427430094303

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_99 : Polynomial.coeff recurrence4LeadingSquare 99 = -((235085554622581685562352460911796427213040461517877 * 10 ^ 70 + 5820760466999613935473605963616491083136402985430837297660201242722835) * 10 ^ 70 + 9963919824938196863530573654258064419148798060919628613244944242883126)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_100 : Polynomial.coeff recurrence4LeadingSquare 100 = (885887218756959391447407091301005084311979404307172 * 10 ^ 70 + 7659733528952159901060635394219840137492481503002961247685264877405142) * 10 ^ 70 + 5641506619614754762183241227499637192983912882926464715578335505397654

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_101 : Polynomial.coeff recurrence4LeadingSquare 101 = -((3252759925004934940090285398699491582023776306426784 * 10 ^ 70 + 9594791864269207102301067068799371168026237453558111565326187955541611) * 10 ^ 70 + 3603346519881053667572705958937987254538444765460396752439406606773908)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_102 : Polynomial.coeff recurrence4LeadingSquare 102 = (11639563781897580721363332187997374895850480446481835 * 10 ^ 70 + 7891222468680511180683780427244183818790320668327846702449369545116105) * 10 ^ 70 + 4227798584326099756376952295304222148486212401502067378218702651482986

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_103 : Polynomial.coeff recurrence4LeadingSquare 103 = -((40599208646965873394247136684361658632760155174023947 * 10 ^ 70 + 1043809818607322531037548332446374401105836714794912661025154043535730) * 10 ^ 70 + 5772712148403344657883397240588483107653073712629540159129394702035240)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_104 : Polynomial.coeff recurrence4LeadingSquare 104 = (138062223284583280219717935169449580474268931504703849 * 10 ^ 70 + 3974978147387189445292065412732885151558427609908346237075813631102585) * 10 ^ 70 + 1097178661363146078053441574498493387552331459233691400812781509192267

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_105 : Polynomial.coeff recurrence4LeadingSquare 105 = -((457808906477719544127630426669468391967715145119034297 * 10 ^ 70 + 1823224549727340577469378293720447451421017424592429028678298038197265) * 10 ^ 70 + 8005796118799348259974579720059237436101037661110760888133397603379226)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_106 : Polynomial.coeff recurrence4LeadingSquare 106 = (1480528938919711688035013632578713703614718248810984379 * 10 ^ 70 + 9521956479925824204798306891019541047242066906015366545965871798639882) * 10 ^ 70 + 3490425900932523742614572517905276600941386103095407668873525361121910

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_107 : Polynomial.coeff recurrence4LeadingSquare 107 = -((4670246191100687692108181809857095463212609653833355526 * 10 ^ 70 + 5332159279896051795738918720670939337895589617307216132135385572031183) * 10 ^ 70 + 5990144661263794290829786750929269336660683950047073955993452594364170)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_108 : Polynomial.coeff recurrence4LeadingSquare 108 = (14371948122510060683347845271140109275172159002275051667 * 10 ^ 70 + 7407470968681426220499547231297557676549683365499473391757116410818659) * 10 ^ 70 + 4346298768362300732592110920095023994642128542283982085590117950430225

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_109 : Polynomial.coeff recurrence4LeadingSquare 109 = -((43152232583116293205435696660613217052575140696056416044 * 10 ^ 70 + 3456986948818826220208688942862882036856741905300451567729391859509649) * 10 ^ 70 + 8172303281471487953942221923252823462434683076125120642975124590141848)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_110 : Polynomial.coeff recurrence4LeadingSquare 110 = (126432156100739535271304464909839781935525646121318721431 * 10 ^ 70 + 3659252686117285539168072656851828607629205227411870974020691499985929) * 10 ^ 70 + 8898426086026408063258450160967284293555663867256084556453757082152586

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_111 : Polynomial.coeff recurrence4LeadingSquare 111 = -((361517700312779795700715053207872604024457189016816215573 * 10 ^ 70 + 5166455618330460517847797741605982889188580270442640806938723804287949) * 10 ^ 70 + 2405238453734916010982409950431044185596144688580519615685431394369998)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_112 : Polynomial.coeff recurrence4LeadingSquare 112 = (1008943280170373215600251090206979530680179923128411877190 * 10 ^ 70 + 5814404049255936669040567215151647332335197329604872157135924034364895) * 10 ^ 70 + 3292249165026485362688052198823008929955147169475804717071933040295702

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_113 : Polynomial.coeff recurrence4LeadingSquare 113 = -((2748608728716449547945655963297806016216702969377790030426 * 10 ^ 70 + 3699954939913370409493265214994111241914336174352519389269399552067928) * 10 ^ 70 + 7914400404338335656596991741869562375344463341787586266753377168231586)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_114 : Polynomial.coeff recurrence4LeadingSquare 114 = (7309848263007492082929239796027167407535447320210629990208 * 10 ^ 70 + 6027984279218925360253224152090475676080058390696772974011739977521704) * 10 ^ 70 + 5404146151534014818390306538312255036728745675900342111968500921975798

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_115 : Polynomial.coeff recurrence4LeadingSquare 115 = -((18979723954188548646709832426851990974347132569269407510330 * 10 ^ 70 + 1891860153148404594618801881015583555673728712260810604533440566071655) * 10 ^ 70 + 5971723606987576815880426163951412287367249951951229674905214061998536)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_116 : Polynomial.coeff recurrence4LeadingSquare 116 = (48116153309017656246279198657315239364214067382612953296259 * 10 ^ 70 + 6219441911146573423138315304044027623277875106755368256409009682517242) * 10 ^ 70 + 3628448726641245956296818849437933059455526599174838289340970307111317

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4LeadingSquare_coeff_117 : Polynomial.coeff recurrence4LeadingSquare 117 = -((119108122134068516403509272875981518525209353831613677903299 * 10 ^ 70 + 4682291341548528847146534267269572300119899564145621301484175800785178) * 10 ^ 70 + 3252327029774976487494113990724249719140681744402108350572667162223990)