Recurrence 4 lookup certificate: Scalar1Second 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.recurrence4Scalar1Second_coeff_142 : Polynomial.coeff recurrence4Scalar1Second 142 = ((21675592173221571353005074840392049849206993463366472096879386 * 10 ^ 70 + 8290869340941145676810682670811557617521263425687459684090370549031487) * 10 ^ 70 + 1638068220331227588164647361034360968054272911509886753227212917152909) * 10 ^ 70 + 2057686900117656413776137964067505313881216399955749465013638249241311

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_143 : Polynomial.coeff recurrence4Scalar1Second 143 = -(((107789435020436196442685134712808443309846503819060350360701016 * 10 ^ 70 + 8192568494840480992975673951912205995986025357969094280733674086221716) * 10 ^ 70 + 6989355735911731401432166437543073378432260806061252990772788122987891) * 10 ^ 70 + 2911397676719714576534425507106576526698041862681906281962681747138095)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_144 : Polynomial.coeff recurrence4Scalar1Second 144 = ((526586490306744904492838591808857365314439289808644936854496551 * 10 ^ 70 + 9216413491144511863124644558412274611705637485284802531250531165247222) * 10 ^ 70 + 9741032991364289756328887888680287413303837856510692849900180888071670) * 10 ^ 70 + 4645799069244275410324855770092985423564261916189759471171279123542436

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_145 : Polynomial.coeff recurrence4Scalar1Second 145 = -(((2527596624487934396822815036058854265028272626859917240558805019 * 10 ^ 70 + 1972983569431121653205953858595687727733637878717440311320619375305835) * 10 ^ 70 + 2761434872487970483582719301890787833730688446780312175538224478484172) * 10 ^ 70 + 9201007114714985712349723876466358306173619891627622866591835351928004)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_146 : Polynomial.coeff recurrence4Scalar1Second 146 = ((11921887096227140965737981048708551630116550850515118971691733259 * 10 ^ 70 + 2203541471287478373268407442087166179466813711776215527857040456878452) * 10 ^ 70 + 4753888987656516716612902486003022497466127710784608079241093430383565) * 10 ^ 70 + 7884686448409709510866219966411783642068245648727608546805319409784382

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_147 : Polynomial.coeff recurrence4Scalar1Second 147 = -(((55263009070622287955994140445807628178029185341031149751096112370 * 10 ^ 70 + 1816092156404794006061108171694844995782919450031497632356306929798491) * 10 ^ 70 + 5521064408188829543300204990920456600466669490955210792952151861138149) * 10 ^ 70 + 4494515663245299988421302533607507883342197477842525402160739433329934)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_148 : Polynomial.coeff recurrence4Scalar1Second 148 = ((251783891081903045370461255387868494109345208078857872401737601811 * 10 ^ 70 + 5798403182025761318801145638250233671496973726657870847096472255131913) * 10 ^ 70 + 4253474087803595043270492023870123523299961046131121703126185479069537) * 10 ^ 70 + 8807978574020378712288361971718385382430661297809938594451844807496512

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_149 : Polynomial.coeff recurrence4Scalar1Second 149 = -(((1127652763176749695648471435715279259109273039381214914347032753724 * 10 ^ 70 + 813435993276435513232014353442059485502752000921562363635715667172754) * 10 ^ 70 + 5858810485558902140505575741937562487530183579435021123031989263454678) * 10 ^ 70 + 32316921106902499844582889629971385393060325024606747762696284914265)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_150 : Polynomial.coeff recurrence4Scalar1Second 150 = ((4965072613333035337253281322455218553113823249994991067705598066498 * 10 ^ 70 + 7101063912614801435555751228172766419216466061404946444533552967223433) * 10 ^ 70 + 3666393713771011870636193290129058120410294228813147546064871664629889) * 10 ^ 70 + 4093623728211785433991553172359508842166317545656697145679327973864687

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_151 : Polynomial.coeff recurrence4Scalar1Second 151 = -(((21494430735765727801032669477624820331222220869400499227331660591315 * 10 ^ 70 + 8382164405221968869456638940348430780096319276347113049627768828174688) * 10 ^ 70 + 6934885380749464714010341348034603352886897178707864337825413670895091) * 10 ^ 70 + 5847234231289603626286678535770402460169789473685024294061208988421494)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_152 : Polynomial.coeff recurrence4Scalar1Second 152 = ((91500283726196738396664666737950130202682503988720481955238719465990 * 10 ^ 70 + 1577242959508985036378397559191047471657512185462049968378290856402369) * 10 ^ 70 + 6423788645432671049303467687627910261727532826588719313678398599681688) * 10 ^ 70 + 3460536930788980821455547884005126509886792599893041703828874532388923

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_153 : Polynomial.coeff recurrence4Scalar1Second 153 = -(((383053826905874075695607649650321187121192849119370251972318432209254 * 10 ^ 70 + 6524281965801552562947644648169390136657972173778115323535287833508116) * 10 ^ 70 + 3048573403118664490981789288819436484601097607048111741237419220608541) * 10 ^ 70 + 5549346709130187628310417680594823221025615063470163786293377060484349)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_154 : Polynomial.coeff recurrence4Scalar1Second 154 = ((1577180857748393775625656514130826866327977918238719139366878035640561 * 10 ^ 70 + 1507119760996135841799030093507565508351282797324588307256544424486898) * 10 ^ 70 + 4804747927704539108562559038833255728331984096125785233175940690048574) * 10 ^ 70 + 9249646807966630960718777710283178116026416438756867753936474796836594

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_155 : Polynomial.coeff recurrence4Scalar1Second 155 = -(((6387482715948361475325628092441834208357739497370079337910922637161244 * 10 ^ 70 + 6400865826095697104249409656476645529616367399130687483587557865633403) * 10 ^ 70 + 1637239574545499495762489117207752775279537628546418244745265810638075) * 10 ^ 70 + 3849416497533927335782151261415084047053264340502033933182454684663604)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_156 : Polynomial.coeff recurrence4Scalar1Second 156 = (((2 * 10 ^ 70 + 5447524799038498607078802672546999081086564396284684386464763753584585) * 10 ^ 70 + 7900670894199604967564620409547288564135166174834723263346791485016374) * 10 ^ 70 + 8648813618746883507772852753334837623998277233657403451071115481394484) * 10 ^ 70 + 839720742503378213706592827326959626320190110572656887304142850895003

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_157 : Polynomial.coeff recurrence4Scalar1Second 157 = -((((9 * 10 ^ 70 + 9739863266650916662845375860956317982406908032697302109544153699831994) * 10 ^ 70 + 7220700473108737044140833838798792350227759718541256735111280112442090) * 10 ^ 70 + 412755460102267854625202879203616536002050382071540754364928723637052) * 10 ^ 70 + 109158343082829128862652494970895782038585251819979603083419333478905)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_158 : Polynomial.coeff recurrence4Scalar1Second 158 = (((38 * 10 ^ 70 + 4625529155494507136261188248135359837334013342047142578811885156588820) * 10 ^ 70 + 473409363267143840090891551490056355567292503165234895923924757922781) * 10 ^ 70 + 394318224941729518540158745664928949614573387548053743888097960740266) * 10 ^ 70 + 287175397854658114559853357018281861978932990494580828084604093279086

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_159 : Polynomial.coeff recurrence4Scalar1Second 159 = -((((145 * 10 ^ 70 + 9456469884395722426263978835757580947977539325558143739560675951333571) * 10 ^ 70 + 9739156353433407243355082896004081540338262619195859686535493461410677) * 10 ^ 70 + 5735611991309723114808024667390124976735006524118082391094493712504514) * 10 ^ 70 + 5014294435135451264277875503435320990672660450570403399319293134457490)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_160 : Polynomial.coeff recurrence4Scalar1Second 160 = (((544 * 10 ^ 70 + 9596924512075697735774278195507254638770438067028366020969755058016147) * 10 ^ 70 + 6422575700536084743798286729349175351375504145450297171385934207225145) * 10 ^ 70 + 3660386142820250572245516511300187799198890604688421660229963191352288) * 10 ^ 70 + 6403936680545733210267630340741645213341370840371085224093304854666801

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_161 : Polynomial.coeff recurrence4Scalar1Second 161 = -((((2002 * 10 ^ 70 + 5955223363551748598586498848334115581715223205371419501482853301889365) * 10 ^ 70 + 7915627746647969758179523038939707716275459454407312131068220457859507) * 10 ^ 70 + 2155428526865947497597819709150509954309406758717043885627404766241733) * 10 ^ 70 + 4750772307832835767974420433567291270099082138588628188617458557614825)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_162 : Polynomial.coeff recurrence4Scalar1Second 162 = (((7242 * 10 ^ 70 + 8937147157132563688222792518359958691794259972662014177128333960314101) * 10 ^ 70 + 4418309891293676438284034008636129136639392055437483165041493664524366) * 10 ^ 70 + 3872040384605081813396418691004886947952771545216557844962888107360910) * 10 ^ 70 + 1888725917542647495710233273380109546530221104400457301229313907201349

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_163 : Polynomial.coeff recurrence4Scalar1Second 163 = -((((25784 * 10 ^ 70 + 2417406955171280050154114730008534193010739128041963992776403003002743) * 10 ^ 70 + 754857844124944659317573886961049319862172703026174436952408810118878) * 10 ^ 70 + 4147498096282193640066022366448932541296836852831383745101351067242238) * 10 ^ 70 + 6640862190196564058555976127151604734199253804641840380261043476616439)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_164 : Polynomial.coeff recurrence4Scalar1Second 164 = (((90355 * 10 ^ 70 + 371942864700056172575853643381531657548938728610825258140642541329203) * 10 ^ 70 + 11342386220157892011443726559169188440966472233516654821797725412054) * 10 ^ 70 + 2825839066869293580286293037102191205132118414034769859547536981470403) * 10 ^ 70 + 869069120439709467120308351933288275926676281773242759300093907376386

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_165 : Polynomial.coeff recurrence4Scalar1Second 165 = -((((311700 * 10 ^ 70 + 5173064469472296774178139757307465054829032606981895599916487412300282) * 10 ^ 70 + 8551473759752384106671867420938061647285997831211389585784603832316183) * 10 ^ 70 + 6558237530632514263823477246960046170971000270405579943544138532983460) * 10 ^ 70 + 7442181042828158960195741196958045755157096226040722039137347231163632)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_166 : Polynomial.coeff recurrence4Scalar1Second 166 = (((1058620 * 10 ^ 70 + 4210864060902671968822752444033669450490723094358064926379875153038090) * 10 ^ 70 + 8556572167011922687931033048353208659352849116661706832483154896525269) * 10 ^ 70 + 6982012382449393351044304553251088956956295648777828568098467118699525) * 10 ^ 70 + 4411460322740073215915572627724671711116274659693033003919417329571508

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_167 : Polynomial.coeff recurrence4Scalar1Second 167 = -((((3539892 * 10 ^ 70 + 7708247811335617116699158006829877278910946164877176965490262772066655) * 10 ^ 70 + 2666981400094963784237270241620650452624395781368362584011334398979194) * 10 ^ 70 + 3990119379624395312434700541396071134277380632181977884231407672229370) * 10 ^ 70 + 9469573493297320568824594593159157167480496786935945374871894370612325)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_168 : Polynomial.coeff recurrence4Scalar1Second 168 = (((11655089 * 10 ^ 70 + 8930355493236584436189644076992397469889188997409093494007718084714465) * 10 ^ 70 + 5754730320171181865008040683417508054934098365289364178833440063523711) * 10 ^ 70 + 2647135457557435563799512919805660373056219269831260023479420229720575) * 10 ^ 70 + 9958565227557103295602266030323242009070580846167550579794790176363859

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_169 : Polynomial.coeff recurrence4Scalar1Second 169 = -((((37787182 * 10 ^ 70 + 8503931119493113917872010817363658237208081260276333308379725292869924) * 10 ^ 70 + 6020815634272495319619592826111179097284506919178475871852243434297882) * 10 ^ 70 + 3749605197962905482104432896763467268962104320490046601170390767711732) * 10 ^ 70 + 2711300649601789057043939858028750008546487936560199904261593225182328)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_170 : Polynomial.coeff recurrence4Scalar1Second 170 = (((120643400 * 10 ^ 70 + 6943289571013872616859869164920639273552406967721995798784092139766561) * 10 ^ 70 + 1163110655540468294063638569795274685590965533146699008936293474930138) * 10 ^ 70 + 157273668898984511507473999981344835315257820270232436531885250277038) * 10 ^ 70 + 1325878257331215465905527437541965110340559967695411587929765421874130