Recurrence 2 lookup certificate: Scalar3Left coefficient convolution

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_143 : Polynomial.coeff recurrence2Scalar3Left 143 = (2009024418202604696162928084955915129 * 10 ^ 70 + 5692285771269903349816698488693847648615734599869915142672399452464392) * 10 ^ 70 + 4573226701133528694372947386560554228311921269453406698937634466777637

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_144 : Polynomial.coeff recurrence2Scalar3Left 144 = -((5900019878993257546007213070669656214 * 10 ^ 70 + 1786179150995706897837643539078349258685835356279848574931180721336776) * 10 ^ 70 + 5904159342302229329334411454875608150556622076878366255553638610226750)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_145 : Polynomial.coeff recurrence2Scalar3Left 145 = -((5942728167108887040019758744039403471 * 10 ^ 70 + 9380496376672800167560529182362937516812962911232268346783686857625543) * 10 ^ 70 + 260809829995413782593176338935278631654504881627529149051245613723471)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_146 : Polynomial.coeff recurrence2Scalar3Left 146 = (92324814218846992341167338889323271564 * 10 ^ 70 + 2666396547019309426320395130599828142869164427582466836036192331404130) * 10 ^ 70 + 3406683581704047665285543354289238533767285309518727668374496196810170

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_147 : Polynomial.coeff recurrence2Scalar3Left 147 = -((213052435032793665097015250341928409471 * 10 ^ 70 + 8574547249638490657659357900624458875449686248230598283650019210759403) * 10 ^ 70 + 7825560123736881559662945553297298980206993690074745440925341300915715)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_148 : Polynomial.coeff recurrence2Scalar3Left 148 = -((512900683669948921759666543932801395096 * 10 ^ 70 + 3932454622149861975430960650489897809688371760553198391455995902001202) * 10 ^ 70 + 7864662112005768429855381424875458771224768246916274820322068137575063)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_149 : Polynomial.coeff recurrence2Scalar3Left 149 = (4335670100927251382601282677530736186974 * 10 ^ 70 + 5746878030646038414598625806658563270776263553417884602277309751040982) * 10 ^ 70 + 5021039477375597659729887787272521817260023629289150426682916318380746

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_150 : Polynomial.coeff recurrence2Scalar3Left 150 = -((6703398764974515088659339001425166658397 * 10 ^ 70 + 9611573509427575091864634834112979535648732072835885264686719912043843) * 10 ^ 70 + 7409194788726790598985854061106960396145329493716586467693405522195713)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_151 : Polynomial.coeff recurrence2Scalar3Left 151 = -((38614815188984721040919862625304037713964 * 10 ^ 70 + 6426335891033077977036597051940144172717851732721966498196872790368613) * 10 ^ 70 + 6058472475815940915363198630413369303297384009591106923035204992279533)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_152 : Polynomial.coeff recurrence2Scalar3Left 152 = (232246658752287030585021998023706676230489 * 10 ^ 70 + 5963939894197252452444532855167587308942266178100013302528195978681376) * 10 ^ 70 + 6499728839871943722247973622652231326458957641394345801002294915603522

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_153 : Polynomial.coeff recurrence2Scalar3Left 153 = -((313078704343761405774143064014991123697946 * 10 ^ 70 + 4141954367051828652713320651027594030382925898167512241859388007409424) * 10 ^ 70 + 5445404887442518750392955612778771660946678735435457622828144540020335)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_154 : Polynomial.coeff recurrence2Scalar3Left 154 = -((2028823038558636617910099449922526865946444 * 10 ^ 70 + 471581576570683320253338620369259536155099864668500397205908785842736) * 10 ^ 70 + 5999615306676906442406882241765754015444300570153911854063813969473534)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_155 : Polynomial.coeff recurrence2Scalar3Left 155 = (12106235507761723709481412718113763828591195 * 10 ^ 70 + 11889704690463255475253423282784300832031151559147763297191354465166) * 10 ^ 70 + 2357274714810835339239087912272928382592705623523243367775368497016640

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_156 : Polynomial.coeff recurrence2Scalar3Left 156 = -((20866046941090793907221752032045870165528658 * 10 ^ 70 + 3878545408383245514540754021247089608343465011190718899944041994883525) * 10 ^ 70 + 149034069479937990020606553859807817462196886590934901473512798951776)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_157 : Polynomial.coeff recurrence2Scalar3Left 157 = -((71668986560716364131170007278728546214943167 * 10 ^ 70 + 3581778991077425310849725689837687894508914241087461036020941488239820) * 10 ^ 70 + 3064186094769332834660678167904887115725794782139414175859203809793838)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_158 : Polynomial.coeff recurrence2Scalar3Left 158 = (538885170224139691660203758206410118834423024 * 10 ^ 70 + 6473410125457283064784134242536370229605939417499448433455105008744541) * 10 ^ 70 + 4715489276701468128122558993748211789319617400890059032705229862434327

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_159 : Polynomial.coeff recurrence2Scalar3Left 159 = -((1258596178147366633365190643395849495701665330 * 10 ^ 70 + 9124327731063065275561208891033734461880029699580882577648569858443380) * 10 ^ 70 + 118585987509681677480202573900849127298300400368320451539153996274217)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_160 : Polynomial.coeff recurrence2Scalar3Left 160 = -((1333828244055002734480867511641900060062974945 * 10 ^ 70 + 4427745176118211423028046177231335603073785975249162541420594923182645) * 10 ^ 70 + 1610075950279469387283549116958468480630917190462143972744436359600744)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_161 : Polynomial.coeff recurrence2Scalar3Left 161 = (19382246042479875811501288484560887381053165673 * 10 ^ 70 + 5389679307415429370108905848600704002316623453131973486824455868067728) * 10 ^ 70 + 3010243829746091531731102870900934744060914117641920900405787472569023

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_162 : Polynomial.coeff recurrence2Scalar3Left 162 = -((60198534800153602222200663055464206896545341677 * 10 ^ 70 + 2245870253559466997600407363844251529838986601568411625865066166005441) * 10 ^ 70 + 9205572509414563074220015647217309847056523610350796151129118090244238)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_163 : Polynomial.coeff recurrence2Scalar3Left 163 = (23156488026304377162319007767601186307480966010 * 10 ^ 70 + 428983233740373196260696333917678494674220842666747676434569817151990) * 10 ^ 70 + 852559955743498661357086340406244263412477087783875497522990638108571

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_164 : Polynomial.coeff recurrence2Scalar3Left 164 = (543164316382102489288461160232169317785313355431 * 10 ^ 70 + 434524609675774341467948858811861055553237704256131375317393011583847) * 10 ^ 70 + 3034539686803176376086153929737508509833357991367263313454086453560727

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_165 : Polynomial.coeff recurrence2Scalar3Left 165 = -((2300363545209386506483905856818668796767698300679 * 10 ^ 70 + 2477369313096952000374802328601976420095631330515152897933592870266449) * 10 ^ 70 + 6529037909490741793499730640122469507942140247420758775486812251411786)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_166 : Polynomial.coeff recurrence2Scalar3Left 166 = (3215201748917490317809399554335160471799694073953 * 10 ^ 70 + 7295249982150557130581722728308776729581801433266011097365666771887942) * 10 ^ 70 + 6785262193276739883729593945299821127183301060107450969469702205651676

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_167 : Polynomial.coeff recurrence2Scalar3Left 167 = (10722217551525109399169578751064069752503511310348 * 10 ^ 70 + 3074432273003270652635532063368856648971190218890311794131385737100867) * 10 ^ 70 + 3649835759284670426093052718504184335515282085639387735011547051256919

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_168 : Polynomial.coeff recurrence2Scalar3Left 168 = -((71846410819585812568221198840679619918799373590284 * 10 ^ 70 + 607377766105453667753495726233303025147000374559602758175301210462821) * 10 ^ 70 + 8468236256339107173871223593355028598748132706328307260908381933591898)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_169 : Polynomial.coeff recurrence2Scalar3Left 169 = (167111267733090785222041643166789205374385906200812 * 10 ^ 70 + 1296287058335634080112808095712038208726488596097410873206503017396928) * 10 ^ 70 + 3521465480028670015636236769859124997935057157329758781174988572483987

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_170 : Polynomial.coeff recurrence2Scalar3Left 170 = (54324962932303328043713297802290909625056072429042 * 10 ^ 70 + 8471269138181053193386577457051327398458608559090792825583719147128096) * 10 ^ 70 + 9141137014816205666949154155783475288598772830920165613661453761813313

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_171 : Polynomial.coeff recurrence2Scalar3Left 171 = -((1777812816944616077195247881145751537144587473629348 * 10 ^ 70 + 9347631912581663935012743260155624704816088626700976452593047598827377) * 10 ^ 70 + 844409281043985850306936601906624016503377162033714924743670285028554)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_172 : Polynomial.coeff recurrence2Scalar3Left 172 = (6239633556678417314762311336780821712331564593194380 * 10 ^ 70 + 6703014281669258085307296207051305589182965091691221057745761213300833) * 10 ^ 70 + 2644404934394238265130630448629215000572213648552075641489790273314745

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_173 : Polynomial.coeff recurrence2Scalar3Left 173 = -((7465441920806590457458492046793823840335006043896967 * 10 ^ 70 + 2475711373527639267905827910909543536786430250675131017787217055499315) * 10 ^ 70 + 7117484287961718743645945445865169071261538726319554674867978068673151)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_174 : Polynomial.coeff recurrence2Scalar3Left 174 = -((27822449330021422610130733872159812559130294235865333 * 10 ^ 70 + 2948843007361827546876515061518193904009312371441587403790599945542445) * 10 ^ 70 + 3780320937541196408081142886217448901294437142976903696988307415972248)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_175 : Polynomial.coeff recurrence2Scalar3Left 175 = (172978659433033501906963671255301289086401018525689799 * 10 ^ 70 + 2688466793539896221639483947257870264829741235106652003172236837072305) * 10 ^ 70 + 1317860974548593635086656420459046985931760058456401040282583191618477

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_176 : Polynomial.coeff recurrence2Scalar3Left 176 = -((421174721687331079078152859988593118944966495470124373 * 10 ^ 70 + 8192230847871375813966818349869248829606904648206967248175250286042708) * 10 ^ 70 + 4257914498968441408444020272231054675230720809260169534273579971067915)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_177 : Polynomial.coeff recurrence2Scalar3Left 177 = (133978207489105288293880145879786611587102414579488309 * 10 ^ 70 + 9483783504605251225565180309059856385679288240103505198593464780678782) * 10 ^ 70 + 6605518807014757822098188441803071543882226527192350860548651264522746

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_178 : Polynomial.coeff recurrence2Scalar3Left 178 = (3041578743686462163066897774962673481477464902011388653 * 10 ^ 70 + 9894783776912387972994515948067112097059551680649799110488311032199429) * 10 ^ 70 + 6706865411549051923422964842694352707039241873923208250651027044612472

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_179 : Polynomial.coeff recurrence2Scalar3Left 179 = -((12849130351341234646451094824018673369652886728459054864 * 10 ^ 70 + 7415292521108959833272508507436922533122728322085602970928814193391462) * 10 ^ 70 + 2668902427541302103563393967100778154226309917023691932458911753126117)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_180 : Polynomial.coeff recurrence2Scalar3Left 180 = (24831071690516085398876027266646744244273313875398660002 * 10 ^ 70 + 4489847797206258077090219504904045097647216924870669743015964230048608) * 10 ^ 70 + 359197473067833951318448295951135877873279901635500398738336751698340

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_181 : Polynomial.coeff recurrence2Scalar3Left 181 = (6906150232257897113311297784961912509013108728764321626 * 10 ^ 70 + 7621713275982994713281325651808808977764856850445388897424284188328108) * 10 ^ 70 + 1643349675044743416362973756005300809139394962631355999178735550317821

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_182 : Polynomial.coeff recurrence2Scalar3Left 182 = -((221863064333506162807236981203421443049823853001802141571 * 10 ^ 70 + 1295551138893209537418490612813612093395283336296716976417782178247132) * 10 ^ 70 + 6456139036167747306379030839152287402747276087412629615269633306724207)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_183 : Polynomial.coeff recurrence2Scalar3Left 183 = (804164828017363127235597635497664572880544751163332125965 * 10 ^ 70 + 885637382871845133321051579277707979601423775920594228260894810186558) * 10 ^ 70 + 493588591724412080494679164178600003300470850425532897848524378684438

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_184 : Polynomial.coeff recurrence2Scalar3Left 184 = -((1425671847700117014294720867653443801758376625329421622175 * 10 ^ 70 + 3938786220501076567293426136512518226873825802342996778843915312257489) * 10 ^ 70 + 6244575605409016105574760836216267344727010591444956229143807419512202)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_185 : Polynomial.coeff recurrence2Scalar3Left 185 = -((482153638534590983617175435671762737022314268337193522341 * 10 ^ 70 + 745159908354992598067356745225176727197766859516640751719092767858009) * 10 ^ 70 + 9315556784812556285112108403320549110169876262000128351858560240133862)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_186 : Polynomial.coeff recurrence2Scalar3Left 186 = (12313836090897832156557011726420577622180637669689946497142 * 10 ^ 70 + 7418323376262378508435276327669537117465120114321982145485775942650301) * 10 ^ 70 + 769292776265675489292193034638128707284343450705983216413037316173662