Recurrence 4 lookup certificate: B3A3 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.recurrence4B3A3_coeff_139 : Polynomial.coeff recurrence4B3A3 139 = (31106999838469996347301180827047294676691427783403549959728 * 10 ^ 70 + 6498541140236245568603711041363120819391242517159564430669605706388048) * 10 ^ 70 + 3252098794584958349413998741969879556696308045621194426022789302811519

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_140 : Polynomial.coeff recurrence4B3A3 140 = -((58608304405330531747023074090998286980331879526790965041935 * 10 ^ 70 + 9141462466053605835226233219269592434960046587593067275185829638122373) * 10 ^ 70 + 4274912590194460110425483975618301021240545563149643235683211068032671)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_141 : Polynomial.coeff recurrence4B3A3 141 = (108196491156490751452033359075182768329565596130957578901653 * 10 ^ 70 + 8586776779915152044188881701712431161146308056759027095529986224482675) * 10 ^ 70 + 6501676969727501800322606218597423045611376549472453774449914039180635

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_142 : Polynomial.coeff recurrence4B3A3 142 = -((195716716265816140280273061559973450795402899784965825653508 * 10 ^ 70 + 9566010026914310436682885396331583272370272815123704935265585838499267) * 10 ^ 70 + 3112940448242822193747315708052019932204536661947809207085905343785279)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_143 : Polynomial.coeff recurrence4B3A3 143 = (346903672934333511869606377188023617239661527076155414454643 * 10 ^ 70 + 7540380247414331984925046597227036137705780028309387337355098791491929) * 10 ^ 70 + 4702820667629058257321267574569553458978570327175439513853808537666099

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_144 : Polynomial.coeff recurrence4B3A3 144 = -((602503095211752275763911563806412760227877831993435793197441 * 10 ^ 70 + 8356948994990980525043743490601866134246355229195371252156193280586087) * 10 ^ 70 + 6891995197535429228412021294252173772722156984888878638356554827618409)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_145 : Polynomial.coeff recurrence4B3A3 145 = (1025368045825957944087421429996888571074579357933563292528415 * 10 ^ 70 + 512649503971136137160144749012592407783184188392258628572010935689710) * 10 ^ 70 + 8699518366356306134692263257843816954390256963569705502516738879763442

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_146 : Polynomial.coeff recurrence4B3A3 146 = -((1709891185352521823174412113665389434430823536746237665786041 * 10 ^ 70 + 6910455482962648367793648115191717482747214837193172097501693384948936) * 10 ^ 70 + 6576020763814666416710374797741306397557533301377799750174711388640435)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_147 : Polynomial.coeff recurrence4B3A3 147 = (2793962995325535525150901131278449393391759952962880187724320 * 10 ^ 70 + 8048130959623638425455864001470118155397686383442602867204919467219768) * 10 ^ 70 + 984750864402898784100705720277244106885292297691011690402502327600003

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_148 : Polynomial.coeff recurrence4B3A3 148 = -((4473305726383182807269811642343978341625317921110594991326487 * 10 ^ 70 + 3636703229213294400971322363971015548213613895717858535527733834596553) * 10 ^ 70 + 9832882918563618874930502576344304392944619292483431860159241393120756)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_149 : Polynomial.coeff recurrence4B3A3 149 = (7017481563522007259568865988591635585634150731807058107965019 * 10 ^ 70 + 9755550492250989153443174476679625524831557822325621814692611952788559) * 10 ^ 70 + 2414570042016212157357380822554200181671889507796866046379547966567089

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_150 : Polynomial.coeff recurrence4B3A3 150 = -((10786094254107585943159905876206249355632070332261748905835248 * 10 ^ 70 + 6073102494312022726670712866419680423740957496375429991634273916540619) * 10 ^ 70 + 8776031873889871356733982031741437481816488403353279912269613591184611)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_151 : Polynomial.coeff recurrence4B3A3 151 = (16242726865979349046213687142785253191070595055244699801390769 * 10 ^ 70 + 6683372454624634961150968246470157054864873014954984062005548338351167) * 10 ^ 70 + 635929667171173882724794981088811480435234935495397574742301990879109

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_152 : Polynomial.coeff recurrence4B3A3 152 = -((23963085522024221970703911805363023478689029691718870524328925 * 10 ^ 70 + 2159376892370181370757116742034124209304280048047430123498003510562224) * 10 ^ 70 + 3340742991904093823585108119377337843103607850985042552247152912590735)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_153 : Polynomial.coeff recurrence4B3A3 153 = (34632837897181279520116791387965187610716727968309512443432298 * 10 ^ 70 + 4457650792678098648323704898588836591483783851164809488206055737844522) * 10 ^ 70 + 2999247551216269238547142918080932913559167131088335455489295511285777

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_154 : Polynomial.coeff recurrence4B3A3 154 = -((49030021475577363696495108523994464999843258886518306793316104 * 10 ^ 70 + 2342485311865605609028941295169866618539911959540760792432925062189446) * 10 ^ 70 + 4149899246724950825065644569978019181785833736117507061468014352732582)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_155 : Polynomial.coeff recurrence4B3A3 155 = (67986988084275692399015250660394769918282021745553919027300776 * 10 ^ 70 + 2118662998364778845974062541314696334552598966415054189583693693734195) * 10 ^ 70 + 8393088617015977132018414757214835599243219646431352445379475783295857

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_156 : Polynomial.coeff recurrence4B3A3 156 = -((92327991355693676015975645012880015029731727604541174724860798 * 10 ^ 70 + 4679778091569613461999498553781931606995570820191746000020138611845867) * 10 ^ 70 + 6643810157046015381952086750657843073205737619570080365125124794915487)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_157 : Polynomial.coeff recurrence4B3A3 157 = (122780972073354864295509063490084220396575685179391140611350519 * 10 ^ 70 + 456941778358044158605402022509673472535639080259519781439317564097006) * 10 ^ 70 + 3812852964749307041924008201640259224585779236289738629580787340187774

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_158 : Polynomial.coeff recurrence4B3A3 158 = -((159865919132386654653086659897830912396808057473960056504979509 * 10 ^ 70 + 5127502209750574112527797731770321146437409693609287920455846536869856) * 10 ^ 70 + 157886641771342537046878850865791407115809109555662082059684858238332)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_159 : Polynomial.coeff recurrence4B3A3 159 = (203767147980400874456403607141178866824186789836206738765460849 * 10 ^ 70 + 7978036157520320600242640048262639050189654319762528628308914364104629) * 10 ^ 70 + 4540334052502418538512335133761970569303739277951113213009238464445232

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_160 : Polynomial.coeff recurrence4B3A3 160 = -((254202342353099876119603625721826696226108873641996193282312392 * 10 ^ 70 + 4959665092863619072959531981559057206200934445630983544793873876502186) * 10 ^ 70 + 8470576596082524156625811305394274609146893653570870853674800372704391)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_161 : Polynomial.coeff recurrence4B3A3 161 = (310306283981203907711068273838388662406618521255651613012589728 * 10 ^ 70 + 7218038288802867731704952091344911416414438723877125624097820079398646) * 10 ^ 70 + 1145224906675756394605208821594475461941350359850360401428003423744220

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_162 : Polynomial.coeff recurrence4B3A3 162 = -((370550628152278456516496817921375182563085457148895534743042726 * 10 ^ 70 + 3622167061119693719641936347726352648348621474245375814195985375131873) * 10 ^ 70 + 4202229638534696716014832545869474126520364296001446855952444259373083)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_163 : Polynomial.coeff recurrence4B3A3 163 = (432721611759677644362794041679492276659903871333037423894915592 * 10 ^ 70 + 2204994143041886864794015226333066705032868264578131210441655087805949) * 10 ^ 70 + 6125391941385884670330001621268188996087757186038405442605240548303703

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_164 : Polynomial.coeff recurrence4B3A3 164 = -((493974210057674082837232702839513717465607860698181454798564247 * 10 ^ 70 + 7645552603912137171227448459732266261631826320028827641509275328938077) * 10 ^ 70 + 8915950132717133534796690167448858398865063581571678822617622083209962)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_165 : Polynomial.coeff recurrence4B3A3 165 = (550973585536137390143088789089709894292494747421910985995841218 * 10 ^ 70 + 1194576595255523381160181377719621519697908228001690500088276991857910) * 10 ^ 70 + 4979593328573270354012277064722145727779878412230113511241953839425591

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_166 : Polynomial.coeff recurrence4B3A3 166 = -((600123151126384659080602599617170020650917783411211070087994858 * 10 ^ 70 + 7652208476609957889838177923773374789143313206865367615355063611891881) * 10 ^ 70 + 6477087467922480071165646214589190063445802674555155889383967074034300)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_167 : Polynomial.coeff recurrence4B3A3 167 = (637864622435150427856460293550790557079203613400331299239875725 * 10 ^ 70 + 9543666160044838554016485255626317499087033757287985304743966199381807) * 10 ^ 70 + 2116626947703616284809993164444796552602504584010681029874204276458502

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_168 : Polynomial.coeff recurrence4B3A3 168 = -((661021334515346808894217123436631233761235370020806407574618873 * 10 ^ 70 + 8086069833147083338712456529322908185096173971325076374425982263420016) * 10 ^ 70 + 3418103379588794684281488876719170961180473614946448794499179452713550)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_169 : Polynomial.coeff recurrence4B3A3 169 = (667144612031060191667387017198445095168197636808878858564783085 * 10 ^ 70 + 2717161340806192280521407636048902781313270348437463198451664262632365) * 10 ^ 70 + 5990221415476607095062660052571269844593770921425551077721074623267604

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_170 : Polynomial.coeff recurrence4B3A3 170 = -((654816798918780315698029287970809862867470592395997881196755120 * 10 ^ 70 + 3860594415188845199053214410900386304111079708587981710700154773609494) * 10 ^ 70 + 5866770309036840779456334387354880996988905452893687055681162711763906)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_171 : Polynomial.coeff recurrence4B3A3 171 = (623865648171715869475235955250669278429343964516338643536341343 * 10 ^ 70 + 6235312635461266701060218286599959719804489732213789355597712618190297) * 10 ^ 70 + 9949715530101362820233072372688048915741599598971243390973294184528373

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_172 : Polynomial.coeff recurrence4B3A3 172 = -((575453833903713836866608607083042624881416155893842674711878322 * 10 ^ 70 + 4338937523454198416203511538873453217514231368298847644605557606102550) * 10 ^ 70 + 8037239149230108628783890936418483967169641568522704887937643593254570)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_173 : Polynomial.coeff recurrence4B3A3 173 = (512023461165849495410312654426073554394395592787119231954457114 * 10 ^ 70 + 1767220767022477902916110896925658490519540822281429682511766460477836) * 10 ^ 70 + 4100823907977231825463949418867736834696175357045769711271223916247291

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_174 : Polynomial.coeff recurrence4B3A3 174 = -((437096134517192447459991512594852252766943916529627859633266134 * 10 ^ 70 + 7798900439167822823909516932325380260625976087802422627358465511532105) * 10 ^ 70 + 1253720251960493536836178817522599463187067604116858850037362171423740)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_175 : Polynomial.coeff recurrence4B3A3 175 = (354950790613070429421501276972161288108388661155294298097416740 * 10 ^ 70 + 9348543761817751194605297512856177254531502667936934282194610594616406) * 10 ^ 70 + 9140628675696729538516599150046245990171945087270715589028037813384042

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_176 : Polynomial.coeff recurrence4B3A3 176 = -((270220096357562787156991173438171770481231685503232098989404788 * 10 ^ 70 + 4704538602710610278093811149937325324611188014594904729051987805331524) * 10 ^ 70 + 3925934274066937813911895392850705474750358996834238460066085611718400)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_177 : Polynomial.coeff recurrence4B3A3 177 = (187458240454192510567071157579519696890245154896413988247464884 * 10 ^ 70 + 9773492580475725232887652652738978470052583045677226408790773759673157) * 10 ^ 70 + 9575422100556926542415541918904979926304411754183235013418384489632736

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_178 : Polynomial.coeff recurrence4B3A3 178 = -((110736159065705114227980456621173529477631836909439572440597794 * 10 ^ 70 + 2456774212910502815384447654773324807444141793486607031112377325451162) * 10 ^ 70 + 7240830750977197054311743314208485186684097888080431145263772807320649)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_179 : Polynomial.coeff recurrence4B3A3 179 = (43314174095294902784035765242004831023725474108848411784955253 * 10 ^ 70 + 9863466086807884412316615756887802516191114278244399746126020571449455) * 10 ^ 70 + 9147441153713353600968480601663072486779429600146776538009386106822421

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_180 : Polynomial.coeff recurrence4B3A3 180 = (12571913531311917724017130136313838430782131657843206764459376 * 10 ^ 70 + 2400262598030703468681015175393296558062154796588470187366463067175771) * 10 ^ 70 + 1999804980521833260000212923210706968181614302365951305300478848336583

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_181 : Polynomial.coeff recurrence4B3A3 181 = -((55794137276075215525746725795093325876235488277936020896313856 * 10 ^ 70 + 5102265702333818652533442520939574813725053674085822197155933498498371) * 10 ^ 70 + 6599759089486682880254389144930266022765448414085935668521736809599854)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_182 : Polynomial.coeff recurrence4B3A3 182 = (86288103295905662099541584098819214964097876153192330498123314 * 10 ^ 70 + 1837714643319926212239754452228034057183075105412646781183109232388192) * 10 ^ 70 + 3680737674663191749948026038180143708152945460918817250870838046003533

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_183 : Polynomial.coeff recurrence4B3A3 183 = -((104901900275141593862421655037032277002775122788507307751610688 * 10 ^ 70 + 3188660969353961122705765648295254625194017551946102225318276455821762) * 10 ^ 70 + 3774339318705712239976204257982083102786198799602676675585270195685287)