Recurrence 2 lookup certificate: Scalar2Main 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.recurrence2Scalar2Main_coeff_267 : Polynomial.coeff recurrence2Scalar2Main 267 = -((549492605826333407882961210611815299655168441778637131071375109697576 * 10 ^ 70 + 9944929094852294696217252001963871655061176556215211061466118722919498) * 10 ^ 70 + 8008107117930322571397285354956366644364244043193337826496706760303750)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_268 : Polynomial.coeff recurrence2Scalar2Main 268 = (306264134988927724846051224589739375578853412532457048302878374613408 * 10 ^ 70 + 7269898436994741459233732868367752234761133174906870407978875320470681) * 10 ^ 70 + 6296351363050183821059458095627905473062443978479894295752273388353452

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_269 : Polynomial.coeff recurrence2Scalar2Main 269 = -((160416191228229607576002654201804271262989758503174654874507711779999 * 10 ^ 70 + 3145262093816529567985070014240301192539006848450796153918576819039640) * 10 ^ 70 + 6658643560349355026489278304515435663328388607053701620915535606300065)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_270 : Polynomial.coeff recurrence2Scalar2Main 270 = (79269134563272607497622516922769240461561776228289125732254659504768 * 10 ^ 70 + 3587250585131834821245468999043176638782472780122475325634112443501839) * 10 ^ 70 + 8785311811726272850418990685173905841671418360507317159859417295156067

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_271 : Polynomial.coeff recurrence2Scalar2Main 271 = -((36995469238529394919541869624605459661737793804977916989209425633899 * 10 ^ 70 + 1984866484586637685772219248781212948026717865583177193494170510588367) * 10 ^ 70 + 5588399823950531777948145494523552312224499257720130217426386858902938)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_272 : Polynomial.coeff recurrence2Scalar2Main 272 = (16286755835953961107401289383757614770636488225938084683423348058080 * 10 ^ 70 + 9846462078480566108025319536085556334899341705487408965076709840669223) * 10 ^ 70 + 2489788054572493840473493843563549717392693314471499925155176635644185

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_273 : Polynomial.coeff recurrence2Scalar2Main 273 = -((6736729427519591723068259342610175420860900944764619599152659375707 * 10 ^ 70 + 5069139077685111359564834232906381125459293268963484791936653288077757) * 10 ^ 70 + 6916853609232619848648152943397266400066813789657553196374968829016117)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_274 : Polynomial.coeff recurrence2Scalar2Main 274 = (2597652122574117012413339249683334226918273737451370057437930700291 * 10 ^ 70 + 5613806658030564099352261365844268360048012147473751163361406989629126) * 10 ^ 70 + 3602870453664607168425502118833316096209233251184276626692646777745701

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_275 : Polynomial.coeff recurrence2Scalar2Main 275 = -((919939565792376187520826554769491900105751214555565449991646886935 * 10 ^ 70 + 6221103345524840530521212368209707483400815872168235599527323086328317) * 10 ^ 70 + 4607868860801230473779068245365478666917125999775743841043950492306791)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_276 : Polynomial.coeff recurrence2Scalar2Main 276 = (290217167241892235343962841633880221395597480539480542223613853715 * 10 ^ 70 + 4351645082687032969205075833156729298663707607245858697411590975650684) * 10 ^ 70 + 146485302160180449986969821164823476425982967700378227224792639702859

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_277 : Polynomial.coeff recurrence2Scalar2Main 277 = -((75565402286759361810779654574298062912186197065765294006230912317 * 10 ^ 70 + 1683547068607603409889921956173269500769366955479660303533334364590895) * 10 ^ 70 + 1814403002323955317138399576446456566866285214497056795160144344873960)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_278 : Polynomial.coeff recurrence2Scalar2Main 278 = (11905838933865149237596827828574198682008370488695388086783196204 * 10 ^ 70 + 5238391538680619092552885736502147838508966685452244074990719817004991) * 10 ^ 70 + 6796193007743938270229900376439577564630984817548794998728618435998445

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_279 : Polynomial.coeff recurrence2Scalar2Main 279 = (2608980850721175394130750376366960404572321165167116184222181492 * 10 ^ 70 + 9020957971763065491547727259410812034814472790045283040768215595016238) * 10 ^ 70 + 1725485086159211814385718608156400925743369282860076407313351743889441

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_280 : Polynomial.coeff recurrence2Scalar2Main 280 = -((3687282604064063503742719348563597201250266067237179900044947207 * 10 ^ 70 + 7738597805537798700955130982655786473329520589804527060640843361220946) * 10 ^ 70 + 810590872300610268650212312286272050058675063171370409286865344201510)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_281 : Polynomial.coeff recurrence2Scalar2Main 281 = (2303130722895288423781007074838149267855092822390977930910093139 * 10 ^ 70 + 5482467460416554302923152344695859504433608022250462728219504406923028) * 10 ^ 70 + 4930590220150504413914523460445099995961524280453727682380538055553934

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_282 : Polynomial.coeff recurrence2Scalar2Main 282 = -((1133512109024005592786304574314243075406491141769823352808949247 * 10 ^ 70 + 1619756381611237287707629339120004656028606565418474261289023861820756) * 10 ^ 70 + 8595063948590250807233807024287946177556314103333564353616031462991624)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_283 : Polynomial.coeff recurrence2Scalar2Main 283 = (487447081059325913106266634841282040577515448187192335325747769 * 10 ^ 70 + 9569006855622266171741675398003516770968079262628041188267542421989434) * 10 ^ 70 + 2581587156976798096763550191797886775608471619282085753657320762544138

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_284 : Polynomial.coeff recurrence2Scalar2Main 284 = -((189948169448797051263018753641285010000057339780862565595011535 * 10 ^ 70 + 945759357536562672415866660865471210107865854646210525456132689051336) * 10 ^ 70 + 6520917838347474930879716032584845611174862601144227451695407680627159)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_285 : Polynomial.coeff recurrence2Scalar2Main 285 = (68122893774986056522016523390946856109108719673402128444139261 * 10 ^ 70 + 949965392736071092155993315148700209976851953222505407451334386780605) * 10 ^ 70 + 3088596567078243695891003177358384198236706740242953280246235879287118

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_286 : Polynomial.coeff recurrence2Scalar2Main 286 = -((22623937723339795972969438327380893302678311036722831923501712 * 10 ^ 70 + 2652446082395787409100943665445858198246986056102552159469617047811637) * 10 ^ 70 + 1254508507102505961408643831484406486342116231542785851560869156236084)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_287 : Polynomial.coeff recurrence2Scalar2Main 287 = (6959588919816405881803990376468750781651287798525380472550904 * 10 ^ 70 + 1181719650894681798316023612929582750841994361400184244876455675642540) * 10 ^ 70 + 8647216941874172565104076435769384768032561028189896897398069636437957

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_288 : Polynomial.coeff recurrence2Scalar2Main 288 = -((1972977258346864230919998697669466957305710968875864774492505 * 10 ^ 70 + 3704662267155887872953170821004814767565599559445658842731377029095631) * 10 ^ 70 + 8039888416507433244136284600346322482587788567563056230897900414239813)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_289 : Polynomial.coeff recurrence2Scalar2Main 289 = (509017686387898206280465607481312262506373173096035175182971 * 10 ^ 70 + 2509965552068018384900421269243384673763413612487840093065885068135670) * 10 ^ 70 + 5639011945910309599327476976446163532879986455064314686465452593771701

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_290 : Polynomial.coeff recurrence2Scalar2Main 290 = -((116320384773557593605408958506766967039692822701938921044108 * 10 ^ 70 + 234129830690233992262386322595523709071991239054087501573037460583467) * 10 ^ 70 + 6932743823044777240698198361979221625645029067545333688237498426164691)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_291 : Polynomial.coeff recurrence2Scalar2Main 291 = (22031820569202299019410788020244606839505996074870224739221 * 10 ^ 70 + 5684623888406384067825627395899675847631644318203281448410372691922667) * 10 ^ 70 + 6014213940276636091465440974150320369077449360029256699751846047868989

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_292 : Polynomial.coeff recurrence2Scalar2Main 292 = -((2708539723630014127784335861591647173990984240127567417741 * 10 ^ 70 + 1420111803949631441321055483514703226296849444755680806705466262700871) * 10 ^ 70 + 8322918195360946599068384572675459758448463247013443900599854274358067)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_293 : Polynomial.coeff recurrence2Scalar2Main 293 = -((214763526904120708318864494479698773220776241418406368043 * 10 ^ 70 + 7240945744604641698415919102068987173786253174853639174154021477451139) * 10 ^ 70 + 1400949841806279307153508800090686146782169799387805157235222327384802)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_294 : Polynomial.coeff recurrence2Scalar2Main 294 = (294897427974398387339966268625694863092444697554211585656 * 10 ^ 70 + 684755078200266040535663879504540792090079808924109476660470712958570) * 10 ^ 70 + 9089247190482700232840197045645164583674601390245303864624231272203605

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_295 : Polynomial.coeff recurrence2Scalar2Main 295 = -((129234899516867506299605031844380419025265039297432697028 * 10 ^ 70 + 4149999310865022988867574189154490305672823291760117759285486933231938) * 10 ^ 70 + 6282374233848907262178654701131795819829384915085830349635595728595695)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_296 : Polynomial.coeff recurrence2Scalar2Main 296 = (42700250108501245101660528773708315298090270907663510139 * 10 ^ 70 + 5441013046448768769692318007792303007713177718601507937769254910987203) * 10 ^ 70 + 4411659045219303362605879535079353373578275158913839666751444713505321

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_297 : Polynomial.coeff recurrence2Scalar2Main 297 = -((11984458886787335292907275927683051870756298346568486403 * 10 ^ 70 + 2774026373439971913399646028564823880791994457665246003969840231659942) * 10 ^ 70 + 9032638420951608054740782492514367142668436944515628917412352041209083)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_298 : Polynomial.coeff recurrence2Scalar2Main 298 = (2963087577230663999902592914611915421387693680980808679 * 10 ^ 70 + 3276970036341246213456096570753103402475416596117258835224697940839909) * 10 ^ 70 + 7447116568473837746194752068375728455305271235442238649112857510798311

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_299 : Polynomial.coeff recurrence2Scalar2Main 299 = -((651647566002975579898403260187225410391270624931155849 * 10 ^ 70 + 9206894081042413441621992575139954665414005660562738465017142120371779) * 10 ^ 70 + 6331778137635623502857182538559297193432082361370981716942770837404619)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_300 : Polynomial.coeff recurrence2Scalar2Main 300 = (126643657052687210820113998274623964463639203294706105 * 10 ^ 70 + 8377499067805879290773443927537832353208645364698753858100224717405293) * 10 ^ 70 + 8359129600500241195003265526427015225318906615807333201204915246266917