Recurrence 2 lookup certificate: Scalar4Shift 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.recurrence2Scalar4Shift_coeff_193 : Polynomial.coeff recurrence2Scalar4Shift 193 = -((1108176316892556890194767511471607538939153116838090144583406 * 10 ^ 70 + 3051708278648302524093191826732860917652223613070177381239312949485703) * 10 ^ 70 + 607642603043160979960483014442238310355317077609754092523822398842748)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_194 : Polynomial.coeff recurrence2Scalar4Shift 194 = (3967287310818661371058342784316242854354287378304728959233209 * 10 ^ 70 + 579865925745752482717191508111247587778761345009618068374783293704023) * 10 ^ 70 + 4255650978207206665015031511116069892682748103697806718157748071871454

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_195 : Polynomial.coeff recurrence2Scalar4Shift 195 = -((8528131848827713704372861852153561298649129436014225260712562 * 10 ^ 70 + 7071115615044323088651353332050726417909307970528761967772266229240248) * 10 ^ 70 + 3048492972253650690145526533169088480672402818346753253042660006768931)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_196 : Polynomial.coeff recurrence2Scalar4Shift 196 = (9341917669020349014738180003092612326816516920901630763817892 * 10 ^ 70 + 9334398091190506336435966030535465385210243729412780347313710079475691) * 10 ^ 70 + 5283881268403476263513788489468120716006414477252325798560271665686219

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_197 : Polynomial.coeff recurrence2Scalar4Shift 197 = (13234056965340719596169109628569644066085232238608347611439670 * 10 ^ 70 + 4749807397956948293515701743932271521749824197624068049321896412602811) * 10 ^ 70 + 2229872248523280251836956467817449607272754834521755372331824136708398

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_198 : Polynomial.coeff recurrence2Scalar4Shift 198 = -((102880642230624481798609416043226026135121984851300053617193539 * 10 ^ 70 + 6232170210263543015106017546153208516341696272165788075303713780624773) * 10 ^ 70 + 9096517146537669339658537129540042567918281991394183057056981556965539)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_199 : Polynomial.coeff recurrence2Scalar4Shift 199 = (319051702582347653912112364313047234330871922372118782173645246 * 10 ^ 70 + 9559462039487816408165287880880096267657755374623158864240762717737343) * 10 ^ 70 + 5804109855732073703408279085053009012953099036568957065299516288037924

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_200 : Polynomial.coeff recurrence2Scalar4Shift 200 = -((659997902108447249470933707955539487519588453048987821042552225 * 10 ^ 70 + 91317170138589730641497601998564817411839144782735614000425966231970) * 10 ^ 70 + 8538614143612104737053867266847665661841142105630185623962323746095932)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_201 : Polynomial.coeff recurrence2Scalar4Shift 201 = (826523375628248415814202240210083760668753735365770210124234295 * 10 ^ 70 + 5954477383735931159707338694987780674990350846623101641057953734263725) * 10 ^ 70 + 770494101955985629955860290394114014731917108046511845806745904095744

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_202 : Polynomial.coeff recurrence2Scalar4Shift 202 = (268360470607741488985375466817237910964099464816523253174963317 * 10 ^ 70 + 1819225966916553351306600945211002852596734234212037370051614946946463) * 10 ^ 70 + 1767697345980858593030270994016299834124203419418553238210295134091426

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_203 : Polynomial.coeff recurrence2Scalar4Shift 203 = -((5193245321086838167070949834149537643608500599959957560397885535 * 10 ^ 70 + 8665214740321199702942359726135762255486989298328286900924701082459504) * 10 ^ 70 + 4308069359018674972882111807222478963861017504301671830826490003547621)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_204 : Polynomial.coeff recurrence2Scalar4Shift 204 = (18345750438529610931380437124801759757749843658593670799468863670 * 10 ^ 70 + 8725744758313621932517314422912040900019309443182245564905798902223833) * 10 ^ 70 + 3904928762040562963630901205987670694580694669596963450925167810853473

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_205 : Polynomial.coeff recurrence2Scalar4Shift 205 = -((44301025481912905175586646457673576360374793832060372773879855688 * 10 ^ 70 + 373202398156448005861515930270420346605221593172187858703164043861716) * 10 ^ 70 + 6137639411088609194004791862873933720750492941974505137206980031160120)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_206 : Polynomial.coeff recurrence2Scalar4Shift 206 = (80690049390591223425173722850045931212832012990759052577985728715 * 10 ^ 70 + 6826548240627908835250208146490567232047711535861905461536804248325810) * 10 ^ 70 + 4339888778756467510653673538850601915030834013555557830887731897115121

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_207 : Polynomial.coeff recurrence2Scalar4Shift 207 = -((100007632651447990319014897747128265285905637250794183489712308607 * 10 ^ 70 + 1460319489487225276714697816910362824858003143504994286110226392136409) * 10 ^ 70 + 5296263510580508851756676620303458955467180950156835121506969280829585)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_208 : Polynomial.coeff recurrence2Scalar4Shift 208 = (13777440814600569883304124972726668657062315383557319834350167884 * 10 ^ 70 + 1735670847766130475105990331064593627401104802312674104992514198100034) * 10 ^ 70 + 5226055733690688270577606460948794940238751728355118915439039915329017

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_209 : Polynomial.coeff recurrence2Scalar4Shift 209 = (384330804778115113451999917440108346659423561229921587219892590616 * 10 ^ 70 + 1319693861197946527978641313626915158037412181572965539115836256318885) * 10 ^ 70 + 9211775509895907033627660511750498390173594379015637001136872237920125

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_210 : Polynomial.coeff recurrence2Scalar4Shift 210 = -((1488165640670238782317002780218022012127274673864237220219444339850 * 10 ^ 70 + 2740612848487665188963051188352502274699033203272039761096466782128059) * 10 ^ 70 + 1318256328200117886187020844427971319898740383280760943234406442662129)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_211 : Polynomial.coeff recurrence2Scalar4Shift 211 = (3928775326638094291914742502976973513752338444505660792540143097147 * 10 ^ 70 + 2070689148852856453438368124295467823511220300190330923939884387797411) * 10 ^ 70 + 5945598207678643618709196337437327996388344673427557038828208199423818

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_212 : Polynomial.coeff recurrence2Scalar4Shift 212 = -((8532914843404104624978460029277269302431653783939049982401237327196 * 10 ^ 70 + 7523993846282045556750667421045077102438366652594356191876568132574631) * 10 ^ 70 + 2382024845865857245477247126420239505733284001712947092648336720494026)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_213 : Polynomial.coeff recurrence2Scalar4Shift 213 = (16073568929362138444366371877435073112528030556339983051458561346833 * 10 ^ 70 + 740347343371276879890088778070116878701117447977826607275056278869097) * 10 ^ 70 + 8755065380588490205512885144156756947662251152840047614822118156365453

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_214 : Polynomial.coeff recurrence2Scalar4Shift 214 = -((26661758601730006129417186526139315987310691761899571726190935932406 * 10 ^ 70 + 1298188241231066931578009577480341942674451395664406388434374190985879) * 10 ^ 70 + 8304723396213528860059340171495594958862371377129102024689160348512385)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_215 : Polynomial.coeff recurrence2Scalar4Shift 215 = (38638407938448034922246725517316822848263734627567563118298194343582 * 10 ^ 70 + 5930981479132010848298760070947015557480977310575037468077087773085859) * 10 ^ 70 + 957659937586668157385033119177129089605120485440188457006631177545341

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_216 : Polynomial.coeff recurrence2Scalar4Shift 216 = -((46915811157730499780291194072313460578563439877082812798287253323768 * 10 ^ 70 + 3214746216895218126488485862064386772097113988150945516648771318157885) * 10 ^ 70 + 677119367263069228869497170365339694114580098872840107268480600801361)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_217 : Polynomial.coeff recurrence2Scalar4Shift 217 = (40917679726341016148759205179258835271006069518356739090427122251707 * 10 ^ 70 + 2684457872982525572760766235467668067053632784301846595097053474626748) * 10 ^ 70 + 1356034953392954690255131415054608893982689052355664098099458429804468

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_218 : Polynomial.coeff recurrence2Scalar4Shift 218 = -((2567960061104802135530853600895543991082191666741602888612815652686 * 10 ^ 70 + 4211595109070195805197408235872227027295537864648723859971283140886085) * 10 ^ 70 + 6127151299923237062148731333007996623369177492902715313020793160666858)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_219 : Polynomial.coeff recurrence2Scalar4Shift 219 = -((94882272982341255891761637602606441323270523351677981317832171325200 * 10 ^ 70 + 2625176105771725940213278796278656455055177894250628089178831375401692) * 10 ^ 70 + 9046860830822305327819639697404052636188377665319493731964310093038490)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_220 : Polynomial.coeff recurrence2Scalar4Shift 220 = (286151495081751617676204159989801262478607810103248798893087681280940 * 10 ^ 70 + 8165550583204348120057617794004106964496604498216525824908332361403749) * 10 ^ 70 + 9065179799695645553320532640987049698543575253480079003398674114311122

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_221 : Polynomial.coeff recurrence2Scalar4Shift 221 = -((610320037790941098849979941332198372705968826947972531772668020612510 * 10 ^ 70 + 2521495556728346888648632030624802271046424202774587899994954557553556) * 10 ^ 70 + 1177167119909437158118417568118628351051267300236323282834466516380809)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_222 : Polynomial.coeff recurrence2Scalar4Shift 222 = (1103712461135685285253837287108245518929873239169338234846712942082294 * 10 ^ 70 + 251481163496233339358645450906481970986641349852628102142624587955265) * 10 ^ 70 + 1201652280472944426500981362790451551513015879418075279011785978641454

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_223 : Polynomial.coeff recurrence2Scalar4Shift 223 = -((1789551936949647950546497559448600318666705767343590240183699888331462 * 10 ^ 70 + 101846827660236449920337725992527948712750086030720943925110623451629) * 10 ^ 70 + 2253140601669221940655981006784644751418216685298763166783828905683197)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_224 : Polynomial.coeff recurrence2Scalar4Shift 224 = (2665898986340770259981757556345200951337477788947697273012042658227720 * 10 ^ 70 + 1204237777080786278732770594891425216874644903341352141388655888857587) * 10 ^ 70 + 2173756187585166832889156715135197425672712775311436189561155527135082

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_225 : Polynomial.coeff recurrence2Scalar4Shift 225 = -((3694635631810303304831017485315241365779830292608298247325864236021878 * 10 ^ 70 + 2927831344793771423024316043770246183714029277128969358948061856414769) * 10 ^ 70 + 2158224349551091003772804545669106456542890076698898813883982430572725)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_226 : Polynomial.coeff recurrence2Scalar4Shift 226 = (4795053354832713641279171837883537321887786523127669535471051850596829 * 10 ^ 70 + 4663679200434132778822532102005102814986989936928927948073472150539453) * 10 ^ 70 + 4265502129787088910500963859470541524313913067976954021814819821243084

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_227 : Polynomial.coeff recurrence2Scalar4Shift 227 = -((5845481659448807250347887251569950139616716733547588448720226329807260 * 10 ^ 70 + 3663558391679332846529515752031700131079861459217585665198537611360723) * 10 ^ 70 + 248450765077104098435463084268261339281966471138598908162352513642193)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_228 : Polynomial.coeff recurrence2Scalar4Shift 228 = (6695087413355434278963436130610979867061713792974687187440323555719355 * 10 ^ 70 + 971289941124919807085106086058696582812333754243025165782276629938246) * 10 ^ 70 + 1728239075694753201524862572581389332143807365553795735896239588621984

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_229 : Polynomial.coeff recurrence2Scalar4Shift 229 = -((7185592857191140378901910868699009346327143883097330297266108718101655 * 10 ^ 70 + 6634333712940207479897678789027724027608560421618891001367696716663626) * 10 ^ 70 + 9794852124691484858428910995709624973592118350434249467223341407661278)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_230 : Polynomial.coeff recurrence2Scalar4Shift 230 = (7179747803390456370591800592224333098949730457500471884525271634010917 * 10 ^ 70 + 9508234848458695181618392773461960292296322340004965685285609086075821) * 10 ^ 70 + 6993566403621841645016386401781538534507547128005806725642601293277150

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_231 : Polynomial.coeff recurrence2Scalar4Shift 231 = -((6590820565115051223215244093325225291394135346052244044052505286299671 * 10 ^ 70 + 7038384466984522801350527047204056262037631846078186693777802252991000) * 10 ^ 70 + 9260674595616957323248682051220905339749202259696005505594231913419530)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_232 : Polynomial.coeff recurrence2Scalar4Shift 232 = (5406068495469509730357788307194440990462258844981794942584063214649577 * 10 ^ 70 + 5205270267115203227309921076530510938654174349625052690180340754536783) * 10 ^ 70 + 5303911361340902350066032891167001556931232210139590014774575520046949