Recurrence 2 lookup certificate: Scalar1Left 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.recurrence2Scalar1Left_coeff_145 : Polynomial.coeff recurrence2Scalar1Left 145 = (31820362652380089243468123162456601072 * 10 ^ 70 + 1962957275696682424924907265743155401657304165790736867818173800289964) * 10 ^ 70 + 5444691827183195792633063605155591843592102619463159560522862584272285

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_146 : Polynomial.coeff recurrence2Scalar1Left 146 = -((235330746419562023688155495883195025596 * 10 ^ 70 + 2986102147191078083390460803411400816976963994139352921266737680217682) * 10 ^ 70 + 8344220618994903511276485369937285516411643800683468740365579151724791)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_147 : Polynomial.coeff recurrence2Scalar1Left 147 = (383224190085423470424286790263888278744 * 10 ^ 70 + 7779865555908358052690185708412418527130620173868228137811980829792439) * 10 ^ 70 + 8530056638983647147054342630801344813785701175207218682463214131851731

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_148 : Polynomial.coeff recurrence2Scalar1Left 148 = (1687459308805876336081443314082449112576 * 10 ^ 70 + 3900898909911879685061471526706032309318814285216125084531155005324728) * 10 ^ 70 + 7527572681596142797801797713470598639087290204891958908503732710030185

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_149 : Polynomial.coeff recurrence2Scalar1Left 149 = -((10033975541588596032659981707968330613508 * 10 ^ 70 + 641759841002179023184646479808711757304606937779876669010295461086732) * 10 ^ 70 + 5900077905805175965243277242065790577046437894240235481840191682565602)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_150 : Polynomial.coeff recurrence2Scalar1Left 150 = (9756584650265180654801222517314861812702 * 10 ^ 70 + 7120018603558154789647749768751842147833720094600406951222232222479777) * 10 ^ 70 + 2989320453968277295442934481910703387942931070903129132404914147095989

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_151 : Polynomial.coeff recurrence2Scalar1Left 151 = (98126030626529138286845642102770298235477 * 10 ^ 70 + 8295038136803159376649247185826302587470031883447467291392046826505036) * 10 ^ 70 + 3574289155593990990995244593104019799783044180839284172802221428791607

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_152 : Polynomial.coeff recurrence2Scalar1Left 152 = -((429909733404163788992105087470623891746324 * 10 ^ 70 + 1191583633475948792363097910320330251223272002584710002040187515519717) * 10 ^ 70 + 860008667124367529349320509033390606434265254895427011928941893782800)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_153 : Polynomial.coeff recurrence2Scalar1Left 153 = (20316122568169086500118202241828860054782 * 10 ^ 70 + 7573506556273966607836372177271256456191910480943680592359350843795863) * 10 ^ 70 + 1238950764399437018573108865789038624321841332559703557814863101657835

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_154 : Polynomial.coeff recurrence2Scalar1Left 154 = (6067462494969625532128302114397135893829169 * 10 ^ 70 + 6722457276567641368456007672700463169252551955325824538959638877877538) * 10 ^ 70 + 3561487122112230886032946701757091096301596997323525852944018135827851

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_155 : Polynomial.coeff recurrence2Scalar1Left 155 = -((22288164145983650556192829863014886336599084 * 10 ^ 70 + 700830085341303062232914372512807292631497827253761247156266561979090) * 10 ^ 70 + 3886444790899230600610990728669291088243553368567105904140863712522905)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_156 : Polynomial.coeff recurrence2Scalar1Left 156 = -((1673573281707107958958050185341373720918107 * 10 ^ 70 + 569926917130006465187006889910835843833029859360602562101883928877593) * 10 ^ 70 + 1521891898024487585268340642100360218651196751080820506386256297562590)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_157 : Polynomial.coeff recurrence2Scalar1Left 157 = (313592723996693401090006227784180129932531424 * 10 ^ 70 + 771518363385479181111852807783316339362051243905578807763422306234559) * 10 ^ 70 + 9250799785630654601369716979019690223281816946531495251511105631164882

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_158 : Polynomial.coeff recurrence2Scalar1Left 158 = -((1205548280645098160003720143658148364377226563 * 10 ^ 70 + 7310176812201661393343119089942303838696754900489093232776899581379181) * 10 ^ 70 + 1074939399973672632906818230127808766875041056408696360402004650053036)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_159 : Polynomial.coeff recurrence2Scalar1Left 159 = (686155695774553080981139102667191890699380015 * 10 ^ 70 + 1467174349217026574976484386768821642488038440153246104690756738402365) * 10 ^ 70 + 4645372047621395593605284772272486321604137244877628044831809750523974

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_160 : Polynomial.coeff recurrence2Scalar1Left 160 = (12429064750314347853717149646214781249127719641 * 10 ^ 70 + 8614088807439084023141545876272014971414200182405326956876231724074420) * 10 ^ 70 + 4696231615550979162370350720989966142200928770998233726583335805404891

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_161 : Polynomial.coeff recurrence2Scalar1Left 161 = -((57341770361257862766199781608213590749193822376 * 10 ^ 70 + 7417785937360664331335934463865782600298942674811631205821905027634143) * 10 ^ 70 + 9636974201949079251628236560701008233564901526569385986950789953741639)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_162 : Polynomial.coeff recurrence2Scalar1Left 162 = (78440864589606378228440756293921587889785745492 * 10 ^ 70 + 3710913159091691466517948591680022768436228028277271279905050828664123) * 10 ^ 70 + 1164641813743434288029708642993726489350888745962325939971791997657403

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_163 : Polynomial.coeff recurrence2Scalar1Left 163 = (351182212514311385194474739527360198264778178911 * 10 ^ 70 + 48008428008543543233658746123556652627516362746510319731799103803745) * 10 ^ 70 + 881386803155492769418372487651351596786983970906163997693424569366407

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_164 : Polynomial.coeff recurrence2Scalar1Left 164 = -((2238867529449222886539011144110206664665004686713 * 10 ^ 70 + 9191926306296552751078176910037287249150348262607415989652561248724705) * 10 ^ 70 + 923543060551434764306577177075404695868203102186540858023136307813254)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_165 : Polynomial.coeff recurrence2Scalar1Left 165 = (4818005143432084743625589909215474051659151200472 * 10 ^ 70 + 7588145030192998046415656571546831083657143422749047256871037161534695) * 10 ^ 70 + 2144116896058516358557050088296349655560268197249990270000332476028342

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_166 : Polynomial.coeff recurrence2Scalar1Left 166 = (5313020058310928035767136107409925130246638495881 * 10 ^ 70 + 8372638748568522264031126332988326644503196405822870834393501899591654) * 10 ^ 70 + 3196602352145708477212569662551115333168049009764242529777980290391813

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_167 : Polynomial.coeff recurrence2Scalar1Left 167 = -((70352432812767977215251378082023850570161722467236 * 10 ^ 70 + 6133121760968913683222243049937813874582325033293843329715833010027740) * 10 ^ 70 + 5873529809480673411491548329527984540290629279703070274990364987376953)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_168 : Polynomial.coeff recurrence2Scalar1Left 168 = (212705662561740215877276523180085609695961585585373 * 10 ^ 70 + 4649107947818129235085324691514572836403445405113591102943632464153429) * 10 ^ 70 + 7814302447245323637399317297674501359276537205432770115458429391261787

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_169 : Polynomial.coeff recurrence2Scalar1Left 169 = -((98784486397810614303877112309493465608037010352768 * 10 ^ 70 + 2736595293553341780238359782865828851041502722507681700329508910726774) * 10 ^ 70 + 6537352488243837335771014342798498063244304767835849794782207116723151)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_170 : Polynomial.coeff recurrence2Scalar1Left 170 = -((1726976465038031450723123548307209120709674417486350 * 10 ^ 70 + 583522064638399232421823204173539871895707504125571213135899409454140) * 10 ^ 70 + 6985290455129985913451234190410001570507222406173083346123014544357408)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_171 : Polynomial.coeff recurrence2Scalar1Left 171 = (7471706993208087036697715549152727840601222778059216 * 10 ^ 70 + 3910655783553118929511897844275599863974917692738047736538374057246823) * 10 ^ 70 + 1233214147078976958759416396579541000555483756423448364128662936206284

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_172 : Polynomial.coeff recurrence2Scalar1Left 172 = -((11598505754996078272925804581532852191180258575100609 * 10 ^ 70 + 5404922749435973786803360204696593528415790154912167458598270728452463) * 10 ^ 70 + 8509141052899927819175207420869289992177508059300412404408405696318225)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_173 : Polynomial.coeff recurrence2Scalar1Left 173 = -((27031955744644789153632798851229023180415461498974644 * 10 ^ 70 + 8973568289951753915513236686815564026027536902756904080021200354414298) * 10 ^ 70 + 5141770476208591456219662516519223846267751568118546357462817813131629)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_174 : Polynomial.coeff recurrence2Scalar1Left 174 = (211155297799683640884147505965414073754741129880673374 * 10 ^ 70 + 1485096734250436090871255398405411270492541948015461192932066480964211) * 10 ^ 70 + 2812540533442130769809117441622681954926207828742691191010584503745879

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_175 : Polynomial.coeff recurrence2Scalar1Left 175 = -((553619258051833272751899371111120509973774765172347900 * 10 ^ 70 + 7968896683953490334830350468972925502835060161747155062592878712787427) * 10 ^ 70 + 4976219973426058619809841979927893213860242160573064093923627807481632)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_176 : Polynomial.coeff recurrence2Scalar1Left 176 = (189366444459218339938018135752120175780719198014480444 * 10 ^ 70 + 5327730288257602198031538644722970491134317793622217993768327628686303) * 10 ^ 70 + 8349647519372698032608351930671056891971518034938306738962401520493395

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_177 : Polynomial.coeff recurrence2Scalar1Left 177 = (4246607073861641298219466616841283998969734604809597489 * 10 ^ 70 + 9394478431872831408153462747525509584273461396528845507433545487362225) * 10 ^ 70 + 2274887844312974942660682556907217098911973965040401773234718928338811

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_178 : Polynomial.coeff recurrence2Scalar1Left 178 = -((17996337963904997698528298496482538870349295547531740837 * 10 ^ 70 + 51147353911203804723514109160507270813818778812250255944613084593685) * 10 ^ 70 + 1058725016431089023952763767431491184420487876347722939201785511304749)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_179 : Polynomial.coeff recurrence2Scalar1Left 179 = (32421302778106321162915786715362414775299480104112455610 * 10 ^ 70 + 1997604797837404183293946857116698806811003633389526209484910945545031) * 10 ^ 70 + 9156028179753974698143105158123171973900997878331995662258517129644202

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_180 : Polynomial.coeff recurrence2Scalar1Left 180 = (28600538568494755590373031140775705482131322616007655615 * 10 ^ 70 + 863571127217549823256056669023307764030966584735368624645348728485296) * 10 ^ 70 + 5225057913703116838018103696496657651765517779182017855693694714097875

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_181 : Polynomial.coeff recurrence2Scalar1Left 181 = -((382579151696174486219208148688236269021759647039006728731 * 10 ^ 70 + 9058645718039466657281942734426487924004185139941564313090882099941834) * 10 ^ 70 + 9053145696025389182273457372631194627741628017782920688329841577573445)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_182 : Polynomial.coeff recurrence2Scalar1Left 182 = (1243917066731898455049958741343439877711956748221409491777 * 10 ^ 70 + 9825691220424830907809684884405345511275427605535851713412797414291770) * 10 ^ 70 + 7469476217380312259472975237680855140236158753543706109988938622491443

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_183 : Polynomial.coeff recurrence2Scalar1Left 183 = -((1717053111808679803322874170877488161817421099885737897151 * 10 ^ 70 + 7608117177620822720690558893205778619646213114217380745106096691786242) * 10 ^ 70 + 4675313867674983857747091020410278680164103197138763416187698062136246)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_184 : Polynomial.coeff recurrence2Scalar1Left 184 = -((3240693682060716306664439127492514935843338284085842098032 * 10 ^ 70 + 1738820301762707299905955548219763759756151830263175669039827840556596) * 10 ^ 70 + 5071721462616139189251731965878929849952924521148316528687448579372158)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_185 : Polynomial.coeff recurrence2Scalar1Left 185 = (25951896717950121597458827779500576402397225167201068197188 * 10 ^ 70 + 583746294635132310939579315170079925784633029921063240499727796948612) * 10 ^ 70 + 6991336759771536390246531276113499014089650656779589660923311452580709

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_186 : Polynomial.coeff recurrence2Scalar1Left 186 = -((75642194237127787638837120490795471146539582452971690357823 * 10 ^ 70 + 4617303903009975078314859349838760769370204763529903410967405616176005) * 10 ^ 70 + 931720502773601912530894375782974781106710548510483614604161629892373)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_187 : Polynomial.coeff recurrence2Scalar1Left 187 = (97407497985861939567199574714384591019499200866586076499415 * 10 ^ 70 + 1909716079055525426632408380494235915907332943673790042196323920591906) * 10 ^ 70 + 5536043808237834485404032716850027337122632434905559430346562537938765

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_188 : Polynomial.coeff recurrence2Scalar1Left 188 = (182894997702681246640615346065576464877181307788793677338366 * 10 ^ 70 + 1300400645780445795737061980381103517057058084292450889046500162435839) * 10 ^ 70 + 1681951424529895848692082239873888271159083126543096431932885761896320