Recurrence 2 lookup certificate: Scalar2Shift 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.recurrence2Scalar2Shift_coeff_195 : Polynomial.coeff recurrence2Scalar2Shift 195 = -((80857572653422753480029033911645202442516117947894239049997887 * 10 ^ 70 + 9607911957583569827927355099258353605705347998496325331529520873234276) * 10 ^ 70 + 3463010824393264351282590248398722488993564503165193797973479353126949)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_196 : Polynomial.coeff recurrence2Scalar2Shift 196 = (253118345400424050365763043956413517587284084435059867399135921 * 10 ^ 70 + 6804495450759907617632829554393091789995357176544717837951468999829007) * 10 ^ 70 + 3463937056783310804610140261749132012528146453282846569159875474578773

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_197 : Polynomial.coeff recurrence2Scalar2Shift 197 = -((489982380019561085711090536349657150209489970852968946438069283 * 10 ^ 70 + 2676858885142467644308833697403348085593484731403483948273456359301067) * 10 ^ 70 + 8687964793617567373018256539359645463088009969974951218248356958322593)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_198 : Polynomial.coeff recurrence2Scalar2Shift 198 = (397249819807995605994465814098289009768631792961851523597067578 * 10 ^ 70 + 7302863506366374776074110863978264308797350342082216454623353796466056) * 10 ^ 70 + 2836751598462571455592317309585180446160185398413208700720932122446467

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_199 : Polynomial.coeff recurrence2Scalar2Shift 199 = (1299382299019606193962326425085955638831372478784414950782688019 * 10 ^ 70 + 87732478917281216347717560399866029570955027436671902390716056693132) * 10 ^ 70 + 1970433115924146071572927865066334072060144175817338524859626958586189

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_200 : Polynomial.coeff recurrence2Scalar2Shift 200 = -((7250289458326654614164573132928498667803644199755491170658546771 * 10 ^ 70 + 2637981152741310883246070684559740805109539246646619212228634021559035) * 10 ^ 70 + 2186754171839869821785184769619885463770946646529007208536888157302914)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_201 : Polynomial.coeff recurrence2Scalar2Shift 201 = (20680748176253943790049793588622396198711795642160841582417806641 * 10 ^ 70 + 8407187033120157421829920618299063371825753031273614791624403325881745) * 10 ^ 70 + 7346204508627949253311722151456693335345101176739889756626336215878356

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_202 : Polynomial.coeff recurrence2Scalar2Shift 202 = -((40079428343563468284083267537336367834117063767591034528933793473 * 10 ^ 70 + 4055735287008250201803267119975203478360454791821311059606054544769675) * 10 ^ 70 + 9072487163009131570638246117124720667316241959060607888539031602281674)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_203 : Polynomial.coeff recurrence2Scalar2Shift 203 = (43807165950837305325730549061673597726032293126093872156252910256 * 10 ^ 70 + 5219814379118993470356153798356611319437918734862402356251372620642897) * 10 ^ 70 + 5676957510218541572604124732642023611093860538580647426951829990034127

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_204 : Polynomial.coeff recurrence2Scalar2Shift 204 = (40850468188280832979421005954474424398901208048608250643047381349 * 10 ^ 70 + 2751531694023129312530160070437133699542991155125429092105228718803282) * 10 ^ 70 + 5343855315993206756400972505587253498692748268065261777467924402606629

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_205 : Polynomial.coeff recurrence2Scalar2Shift 205 = -((379823550260820297929017044854312568111942197673089814397543175440 * 10 ^ 70 + 4377040003169415928230324444132486320899004105716381331181947332294744) * 10 ^ 70 + 1387069795570353226628618861062491243051060549390809132784556236761374)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_206 : Polynomial.coeff recurrence2Scalar2Shift 206 = (1248551128347889367327839234619306373642219684682474716091375506179 * 10 ^ 70 + 6524126490229544613055587588275974869820289956811480057502014530883676) * 10 ^ 70 + 925886921182565782476761837529171055694022334570096850162367257206632

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_207 : Polynomial.coeff recurrence2Scalar2Shift 207 = -((2913517881148996143047450086657885194635729705243602807543473673870 * 10 ^ 70 + 7961205933399602832639956118877493858527692118411514011107819675305963) * 10 ^ 70 + 5715616466940308126910067948046218990691239291953691909878970843306659)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_208 : Polynomial.coeff recurrence2Scalar2Shift 208 = (5150627112407339328851537096977126371871123732957404526640985611205 * 10 ^ 70 + 6523848209751620779736344907166980439698573723064965919305503329557870) * 10 ^ 70 + 3181239053712762686416306669109645797899255378459201499620958655063211

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_209 : Polynomial.coeff recurrence2Scalar2Shift 209 = -((6028435969873723977574483056377229722968859746522187994319771932309 * 10 ^ 70 + 7009120697969388971312263432155204098180018322334960654373092970880255) * 10 ^ 70 + 4061413096915087365861230652526991170155421217553715723204121977633608)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_210 : Polynomial.coeff recurrence2Scalar2Shift 210 = -((492210451638030436958460427262454208885195424070470376384726779958 * 10 ^ 70 + 9246586488565607984161973739099587020763712925458991917854203178342508) * 10 ^ 70 + 5334753125109845717031256649586099583276071912497367510627209931410577)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_211 : Polynomial.coeff recurrence2Scalar2Shift 211 = (28408129587559168122442816448026169404354034336678439756782648314099 * 10 ^ 70 + 5861846808291506325097002992152604312054682625261041036840713264215238) * 10 ^ 70 + 8600940254522487028163428048119569250584553240004315228941048975602437

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_212 : Polynomial.coeff recurrence2Scalar2Shift 212 = -((104506111070129178980394764441012388701179385969983061163802792822915 * 10 ^ 70 + 8776156242775043389423535865315188704539239677609819267241652225414725) * 10 ^ 70 + 1603157156224675761156725245696019607607185703007575972905351575357082)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_213 : Polynomial.coeff recurrence2Scalar2Shift 213 = (272114745037601505249014246833005612045696459039230652070922735617284 * 10 ^ 70 + 3786275621903952688416750507007541863419097094345146528231976984732605) * 10 ^ 70 + 6234617756529107654568987524123951915038847161010320759533401130327811

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_214 : Polynomial.coeff recurrence2Scalar2Shift 214 = -((589120119181771273041249671579133711247075755311477326479300032293494 * 10 ^ 70 + 7866038088195839486915578747458522030732074583206737243839654339990017) * 10 ^ 70 + 3679957201305317819408680596576986243678014517006641581132110395117829)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_215 : Polynomial.coeff recurrence2Scalar2Shift 215 = (1112347588941508331119066683345941877007523774826167482552743629772067 * 10 ^ 70 + 2850172616314001030446842476347723989788432988461091793579347688979856) * 10 ^ 70 + 9855090970078883119241343903326255181107523394958275707127356784621377

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_216 : Polynomial.coeff recurrence2Scalar2Shift 216 = -((1857668712079931159689408022731416911401687685298103118967641727772040 * 10 ^ 70 + 7807231035978835344317984019718286829712850417584191459128995143270535) * 10 ^ 70 + 8870326777143205245302926021486783920402396892104973014898915598883591)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_217 : Polynomial.coeff recurrence2Scalar2Shift 217 = (2725023203616782515507890360798495157461860211612696727478068102939344 * 10 ^ 70 + 3326902179777471315140329802836569942586471973762365102888006873344618) * 10 ^ 70 + 7733638568092240734181153549748368426264207567531790860746293587839459

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_218 : Polynomial.coeff recurrence2Scalar2Shift 218 = -((3382619363583176941298880466905741344708006610378225149964927731023956 * 10 ^ 70 + 1923629702760828167104734061120039123910956154298083517255911626635136) * 10 ^ 70 + 3088043345082745005953904371205583259415177430741022132681239281006425)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_219 : Polynomial.coeff recurrence2Scalar2Shift 219 = (3117166408671960348942321353347700458491924696597281775030414387600789 * 10 ^ 70 + 6404873988019085730987937400455244958441731575562544949410515142401368) * 10 ^ 70 + 2717487924196178479444339451764523425578957394785374294059779105353813

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_220 : Polynomial.coeff recurrence2Scalar2Shift 220 = -((677389847695129354413315819741867097638101398215992367976306385514873 * 10 ^ 70 + 2274641333774478469383330504308037781882257614016492267259072289935851) * 10 ^ 70 + 7212398284331859162666172963855742992105325395149519405127370010843030)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_221 : Polynomial.coeff recurrence2Scalar2Shift 221 = -((5837107092950645108737320866790503974391237515701210534597324222979392 * 10 ^ 70 + 5421386969227239980632905849151455400516429680726517871416685717626991) * 10 ^ 70 + 6951629373691406516670920590844311117655127694939706345245360720915008)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_222 : Polynomial.coeff recurrence2Scalar2Shift 222 = ((1 * 10 ^ 70 + 8968341517775886297860535252170783324584113489801423581871862954660410) * 10 ^ 70 + 1872062699059015853023979317927609483588467969210301619783701286000320) * 10 ^ 70 + 6137254820535176406744670380490453730857846647064699589918522638491138

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_223 : Polynomial.coeff recurrence2Scalar2Shift 223 = -(((4 * 10 ^ 70 + 1694540127248820068233441742452974421501902510550356503563986736911849) * 10 ^ 70 + 2818778104687491870636983555181546779118725458947933984105857186210483) * 10 ^ 70 + 8348953888629904987195392929586649579690980849612998787308701089261039)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_224 : Polynomial.coeff recurrence2Scalar2Shift 224 = ((7 * 10 ^ 70 + 6968796122285844752819293686425512475628733810152379264877632735021731) * 10 ^ 70 + 2516807154432069045714620854648289602902581657834429671606732754327435) * 10 ^ 70 + 6441142983422739446034580759464301887889479803688338670100325111748836

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_225 : Polynomial.coeff recurrence2Scalar2Shift 225 = -(((12 * 10 ^ 70 + 6998973675250049230269839836440871654071019561980558269217659269314281) * 10 ^ 70 + 4285109204879581947796763946421609547521964504023986410099600529930734) * 10 ^ 70 + 5815004286747597063544816957921014883312804653572322759872624571385174)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_226 : Polynomial.coeff recurrence2Scalar2Shift 226 = ((19 * 10 ^ 70 + 2350856552405785945607447261285974960008982003593687772516292840371395) * 10 ^ 70 + 3160978692754845054251327709067186733088726366370273800209068895244947) * 10 ^ 70 + 1196171097584883708502928175852725636329317158427783484818316344054129

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_227 : Polynomial.coeff recurrence2Scalar2Shift 227 = -(((27 * 10 ^ 70 + 1052121693730977138670722542042940318475214208522900393288825150373012) * 10 ^ 70 + 3877619780865006154409909595420889545050857003793319667360100808713031) * 10 ^ 70 + 455352693348616115019725282312217694887571858708367425713501128004008)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_228 : Polynomial.coeff recurrence2Scalar2Shift 228 = ((35 * 10 ^ 70 + 7949583095207759988391588847606735652844931927039605903065567455784196) * 10 ^ 70 + 27035398642781178720591528565452872237718248586014049664094580476234) * 10 ^ 70 + 9446953746962029877381833390523461181390421879649752760709193445469343

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_229 : Polynomial.coeff recurrence2Scalar2Shift 229 = -(((44 * 10 ^ 70 + 4590589946701429721533166125959956766531361652348878652243241042744527) * 10 ^ 70 + 9303002811302274307714151585479011181239143700225339252172312252346199) * 10 ^ 70 + 7039380694643870870234494173871373256234976609257957713802765474426622)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_230 : Polynomial.coeff recurrence2Scalar2Shift 230 = ((51 * 10 ^ 70 + 9835006141198050793365714000193505681042133352552604637345976626955558) * 10 ^ 70 + 1231356282927619159443902245874813939335952430510518773647015061539080) * 10 ^ 70 + 6792767813198202488672438658531177522489313340428092961645950967407822

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_231 : Polynomial.coeff recurrence2Scalar2Shift 231 = -(((57 * 10 ^ 70 + 1253532065081593217145559535413131275087719901193629943595470244674161) * 10 ^ 70 + 976196913428080206379186406576589018503590407095301688726307457611137) * 10 ^ 70 + 9482656703857379736170473118983771407681372476844247974353319780569893)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_232 : Polynomial.coeff recurrence2Scalar2Shift 232 = ((58 * 10 ^ 70 + 7159227628366394327324523634496561189253741307980312137612178913764995) * 10 ^ 70 + 4316909553006048060189304054776530391525628977425270772831273703193620) * 10 ^ 70 + 8707956103113244129267006406567776963745266917588825573606340774699176

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_233 : Polynomial.coeff recurrence2Scalar2Shift 233 = -(((55 * 10 ^ 70 + 8908297672419694350669448567548336578715385167409530993167550216915865) * 10 ^ 70 + 6566754078367508783420804706628361098513962044628073786604111580471285) * 10 ^ 70 + 2255531601441408682658185201695079699584751376016970818329917540948498)