Recurrence 5 lookup certificate: ExceptionalProduct coefficient convolution

This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_260 : Polynomial.coeff recurrence5ExceptionalProduct 260 = ((3668802775283294796859799126676963782591877 * 10 ^ 70 + 8243931959622275345636016343971354819115749075940857156672239473137964) * 10 ^ 70 + 7134420100652461746604140331709275065278186704947851830104717093770337) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_261 : Polynomial.coeff recurrence5ExceptionalProduct 261 = -((47771003560827778788010359273446315361529 * 10 ^ 70 + 9887202467657363985745388929182211741029366771787613584398915370271593) * 10 ^ 70 + 269068612588620093150926705196515001447508217767266529521823046760619) / 1092344269624365921334084

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_262 : Polynomial.coeff recurrence5ExceptionalProduct 262 = ((71172230022126832427772026064154956793329 * 10 ^ 70 + 1775276863978026368159209242445998442172238373456966496173243131689884) * 10 ^ 70 + 5283686791269777588325765638209559761744328968869466411812743728281137) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_263 : Polynomial.coeff recurrence5ExceptionalProduct 263 = -((46213248278164795593794943656760186589901 * 10 ^ 70 + 6795681222731433857482662075583349912090437897835881512262926359563263) * 10 ^ 70 + 4591922884656141960149156810538543820903876272200900396626935889941933) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_264 : Polynomial.coeff recurrence5ExceptionalProduct 264 = ((18086098509168081270391247136095382142137 * 10 ^ 70 + 6952850923372036427028532513256508932964911426520375463424503716789438) * 10 ^ 70 + 3974647745452948077351823321415130038461932929865982910063646397384171) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_265 : Polynomial.coeff recurrence5ExceptionalProduct 265 = -((662151873334928204218505743302450667289 * 10 ^ 70 + 4350056613390840590792876892049193461330426493467462838490126444710161) * 10 ^ 70 + 4344632008229462294972160927391263325736695444947601367294452047801177) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_266 : Polynomial.coeff recurrence5ExceptionalProduct 266 = -((452180290170649140751834065314061524476 * 10 ^ 70 + 6316665703376772629999522498236339989694003576002122102258374419097201) * 10 ^ 70 + 2407210537512407748010253867325143592180776504860620871277103827685866) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_267 : Polynomial.coeff recurrence5ExceptionalProduct 267 = ((51817429165007476920562097431181835685 * 10 ^ 70 + 1419522120866546121320132958275408060135865190827644081831695643883187) * 10 ^ 70 + 1362757680951315345326820137029000987928148626721170217708914807560859) / 1092344269624365921334084

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_268 : Polynomial.coeff recurrence5ExceptionalProduct 268 = -((64251494341114576977193957068561208781 * 10 ^ 70 + 7859662345398970920879948273282989374889281660742427880193641105268291) * 10 ^ 70 + 6489619879623210521570074743133402091514079833180679921557524377046589) / 2730860674060914803335210

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_269 : Polynomial.coeff recurrence5ExceptionalProduct 269 = ((53791493244814027827341190689982668358 * 10 ^ 70 + 2282017236362406893896850545650936169019261427334630003822210061841385) * 10 ^ 70 + 8825682362121041285668920719113964519540986276205223101925092854123921) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_270 : Polynomial.coeff recurrence5ExceptionalProduct 270 = -((25049939246660146611646472040446321711 * 10 ^ 70 + 5542199883777864612492472412595826516138060353090438999767310115623342) * 10 ^ 70 + 2265595918672501795937970262285782959405315987989931103519296379912941) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_271 : Polynomial.coeff recurrence5ExceptionalProduct 271 = ((6746449254898487958593294248886472029 * 10 ^ 70 + 2152108310847189919731082600128739765768534620835779983860651141341190) * 10 ^ 70 + 7243203510298848499373033081820301055011898718838949470607838446632459) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_272 : Polynomial.coeff recurrence5ExceptionalProduct 272 = -((10198577550024844195414498758133936567 * 10 ^ 70 + 3753912112428824174887227223601300708422581945468681559299484318655961) * 10 ^ 70 + 2942685793887354053846394679703319349657568271395470163771989378547361) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_273 : Polynomial.coeff recurrence5ExceptionalProduct 273 = ((1336160455518235172191898046751426211 * 10 ^ 70 + 9460029285058986035673743046938165923106370648915066448261016719734264) * 10 ^ 70 + 2837116497244339445796861869990840542954856324644171657292714882003673) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_274 : Polynomial.coeff recurrence5ExceptionalProduct 274 = -((53549545709424675430783372455443704 * 10 ^ 70 + 9943369745747236497622765247634036928285400069055234764207321174006137) * 10 ^ 70 + 753439219652115535681695281480244570496121543893304151216760306907211) / 2730860674060914803335210

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_275 : Polynomial.coeff recurrence5ExceptionalProduct 275 = ((7365965149627348009536135170668136 * 10 ^ 70 + 625221356384526517477349394776596594957983378338994807886664929851324) * 10 ^ 70 + 4014643397599310456400763999983365795816641326930123881757137736220441) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_276 : Polynomial.coeff recurrence5ExceptionalProduct 276 = ((23650950092311123428160720674142411 * 10 ^ 70 + 5712588631839022360512350669190114023387721201422590048172787848989630) * 10 ^ 70 + 1420257326370630309296153408120396038047712896585895855732876517443239) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_277 : Polynomial.coeff recurrence5ExceptionalProduct 277 = -((9086256218645684495676428632520038 * 10 ^ 70 + 9325889136052073163193305584810151153474083644276214296994699954774107) * 10 ^ 70 + 4486885844078207848118506673436635262767070674024058549073780197283288) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_278 : Polynomial.coeff recurrence5ExceptionalProduct 278 = ((19178698019680666916501457917015124 * 10 ^ 70 + 7747403198069473511838033077579046463723243291553440937771389024781277) * 10 ^ 70 + 7862747197964261956002100288313671005973622769129921579289416579064921) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_279 : Polynomial.coeff recurrence5ExceptionalProduct 279 = -((8712631429588842232264876464981003 * 10 ^ 70 + 7840424823663992554001590634144212545725418618073469807935751609475671) * 10 ^ 70 + 3292878930291808715366632077741511154184110242947867791502420405771377) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_280 : Polynomial.coeff recurrence5ExceptionalProduct 280 = ((1814374107448176716498709458086105 * 10 ^ 70 + 9960620766700991786808420526980487246864089055033392960559450936866679) * 10 ^ 70 + 3839424521971607025712391691638561264635649496001125785095743522428009) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_281 : Polynomial.coeff recurrence5ExceptionalProduct 281 = -((1420727049519216506028244040319447 * 10 ^ 70 + 1974169690166088159063092193634482146187878907952921580077347320996800) * 10 ^ 70 + 7401369678524299551818250689993511972344863166362265896284589665796241) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_282 : Polynomial.coeff recurrence5ExceptionalProduct 282 = ((264238080587017793136657087926545 * 10 ^ 70 + 8527214389739402814685406297168853214607984009346689042216536160866310) * 10 ^ 70 + 8080565332879350099601987423680461753707130621360427623542033150699627) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_283 : Polynomial.coeff recurrence5ExceptionalProduct 283 = -((187396781865430380915036522784752 * 10 ^ 70 + 8694269796099279325715715753967922762501861927872512207270047718798524) * 10 ^ 70 + 3055395469776053757922376975159380192084689025497550708258972850612253) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_284 : Polynomial.coeff recurrence5ExceptionalProduct 284 = ((1265174300958424566070567050849 * 10 ^ 70 + 3934568202650445164248273032780708168468656271109340612557080149544956) * 10 ^ 70 + 7840745631294707782289932386895440720333737052250611671735501209222397) / 546172134812182960667042

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_285 : Polynomial.coeff recurrence5ExceptionalProduct 285 = -((4042356987409087768854795575335 * 10 ^ 70 + 8829914648900274394471406707398620496608450757881618551659485660742663) * 10 ^ 70 + 8099954383026484255109987042199367639769917260013077172074616083095091) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_286 : Polynomial.coeff recurrence5ExceptionalProduct 286 = ((3020669092269737440060858968588 * 10 ^ 70 + 9196242713728886203247487436784238971508873732555863625120840177944349) * 10 ^ 70 + 7108299925538439259393724683935417288702008433246625247701640148064227) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_287 : Polynomial.coeff recurrence5ExceptionalProduct 287 = -((1650826091063126339054393037483 * 10 ^ 70 + 5846647937656200452374890307773721675398498745261808165511345997403197) * 10 ^ 70 + 7543735383088425478584261509081672494619665594155422833014348679624459) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_288 : Polynomial.coeff recurrence5ExceptionalProduct 288 = ((78315637929371536817357043353 * 10 ^ 70 + 6161508640748375154241689872710324319176894259723837705830671618948649) * 10 ^ 70 + 9938201047795743578052576558066529761928256661805756746258855887086911) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_289 : Polynomial.coeff recurrence5ExceptionalProduct 289 = -((34304378938891013641204909487 * 10 ^ 70 + 8634990047301255464405285429000274032761096977874670038841418216210957) * 10 ^ 70 + 8097898965773632473181029179371214777606250884409842380174074458787149) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_290 : Polynomial.coeff recurrence5ExceptionalProduct 290 = ((860097655113501502225049860 * 10 ^ 70 + 8879060412845480792978497682943252969985431217406191766168813761355539) * 10 ^ 70 + 6779676383770133171113806647170573452280315175933914973848763868875737) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_291 : Polynomial.coeff recurrence5ExceptionalProduct 291 = ((6862457961221508615095476794 * 10 ^ 70 + 6744159004449565026942120998362339398260327305933265866520568006265333) * 10 ^ 70 + 3733755281217926648621027866712357486933150282412578318277650672222971) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_292 : Polynomial.coeff recurrence5ExceptionalProduct 292 = -((877243826617315927645349419 * 10 ^ 70 + 5655170225686522989063553622296556304239328175054896806043629787705045) * 10 ^ 70 + 6228039774260006384081534878449799543685944995224123605197790755468439) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_293 : Polynomial.coeff recurrence5ExceptionalProduct 293 = ((500248092002436396642160473 * 10 ^ 70 + 923842778306722185686396129100227787893382567115116188378594523439592) * 10 ^ 70 + 5615464243379037545385792051159785390101520914088634631503863037966859) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_294 : Polynomial.coeff recurrence5ExceptionalProduct 294 = -((194309578656437639849101305 * 10 ^ 70 + 4151635088179089762383237128242489823276664199302712317838758497058499) * 10 ^ 70 + 5579235242693514301567459328379005754130763148929483288409281186102514) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_295 : Polynomial.coeff recurrence5ExceptionalProduct 295 = ((67567150342974434198237442 * 10 ^ 70 + 7444968438114098982416654593344272780316354905673290124224320113905655) * 10 ^ 70 + 4654791939176852220721763028984405354768153295580435817779891407103898) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_296 : Polynomial.coeff recurrence5ExceptionalProduct 296 = -((85520340417176762432473463 * 10 ^ 70 + 3793921755888411759519954212112331773265745519448371745674224719848311) * 10 ^ 70 + 1034170187088475825520590880830046657698767115319308070156902578338777) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_297 : Polynomial.coeff recurrence5ExceptionalProduct 297 = ((24582985857964516022130688 * 10 ^ 70 + 9267260311969221364339233276887761655876351104216462003647171002076692) * 10 ^ 70 + 7794845237542412143416011139815200888079925237415032628267673546713737) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_298 : Polynomial.coeff recurrence5ExceptionalProduct 298 = -((6268826435721986445105603 * 10 ^ 70 + 3882512650734910334821565612647094441052595736848278291599012141987012) * 10 ^ 70 + 8538399597001446793992657225218487384625974913281245472778098127281913) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_299 : Polynomial.coeff recurrence5ExceptionalProduct 299 = ((130879437229144502688510 * 10 ^ 70 + 3969339262862557865715401193253152726247702610392363019281480106078533) * 10 ^ 70 + 6254868369054076137842252051475071658466384119734285238238644662642087) / 2730860674060914803335210

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_300 : Polynomial.coeff recurrence5ExceptionalProduct 300 = -((37538639748316194002031 * 10 ^ 70 + 851497435700809152353525737618350536741843695920235898581062267309384) * 10 ^ 70 + 5931140155349001591693143026128873261661105862746882779687835321530587) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_301 : Polynomial.coeff recurrence5ExceptionalProduct 301 = -((12074773673350830485749 * 10 ^ 70 + 5245374531139319073396175150849948924150641984461114341513891228185815) * 10 ^ 70 + 3727927264208316830902219303162928019803841682009161153424495327086382) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_302 : Polynomial.coeff recurrence5ExceptionalProduct 302 = ((9674738941314203980097 * 10 ^ 70 + 9736564936828822093664784921637671867010602749484778607121436716078804) * 10 ^ 70 + 5490659161592186026397117460993767128357137964657616137848066648959773) / 5461721348121829606670420