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_123 : Polynomial.coeff recurrence5ExceptionalProduct 123 = -((837574785147661405263031789398476136 * 10 ^ 70 + 7871221400170272532735766013850495522190627924551617492919067261912994) * 10 ^ 70 + 83622991254618633219531202249356601779188595473272164933720674682607) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_124 : Polynomial.coeff recurrence5ExceptionalProduct 124 = ((66832006643177995615329031785043307 * 10 ^ 70 + 9057369831201862384991483827831323594744487032563070345225637215226234) * 10 ^ 70 + 7060092065612296949263242315817421572800984173454999123749491567207451) / 369035226224447946396650

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_125 : Polynomial.coeff recurrence5ExceptionalProduct 125 = ((11569281872160970249074640380197256036 * 10 ^ 70 + 5250689080062210076138501720907840762797425709559111648063300510481879) * 10 ^ 70 + 6277320230795794584052620286648363982113301928845564248793103172395951) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_126 : Polynomial.coeff recurrence5ExceptionalProduct 126 = -((66113966084409414706645115570493125746 * 10 ^ 70 + 5310628932270509486468870687849288911284387553639589196347331942220838) * 10 ^ 70 + 9140689176279358848921660035877263588512961688197980802169400796636098) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_127 : Polynomial.coeff recurrence5ExceptionalProduct 127 = ((79976535847962217535631029418136766034 * 10 ^ 70 + 4454513310558720413700602429516394970113417388594834852388395879685823) * 10 ^ 70 + 7114706857277466430624931269061107253743036017892317480691764148525912) / 1365430337030457401667605

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_128 : Polynomial.coeff recurrence5ExceptionalProduct 128 = -((7530911538172489904206935976039853405672 * 10 ^ 70 + 2482492280967607680963986508677357984100902219514938792285431114737814) * 10 ^ 70 + 5308580638790529626584026031977277328256150673702879658238212276974417) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_129 : Polynomial.coeff recurrence5ExceptionalProduct 129 = ((29657981183012655845902605774414929439597 * 10 ^ 70 + 7703203117886272404447030986628603749020334580667123892782113374556243) * 10 ^ 70 + 2100905185559417350181572149685743904911447967919729918616402277444783) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_130 : Polynomial.coeff recurrence5ExceptionalProduct 130 = -((48790639132606723550109159710903270068128 * 10 ^ 70 + 6473619201541655898052439524186608257723122340949829808162869804663321) * 10 ^ 70 + 1580271075102520104778719843745198064001013739223943182278862830831787) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_131 : Polynomial.coeff recurrence5ExceptionalProduct 131 = ((247079584262608396533202491246174147327715 * 10 ^ 70 + 4797723442799236107923222379909373282634909414668273382156537065742220) * 10 ^ 70 + 1137347358746685523979024412090785645229819570478493072828728583011343) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_132 : Polynomial.coeff recurrence5ExceptionalProduct 132 = -((285859196888028176280722107662587893320351 * 10 ^ 70 + 994790426632764272146296363484070233271591402168919982233364337927668) * 10 ^ 70 + 9046728799856996977276322677091059167812773307365655911083747605773797) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_133 : Polynomial.coeff recurrence5ExceptionalProduct 133 = -((86083539636181585269624466669041399788593 * 10 ^ 70 + 3407505827479760974142831521793488370099105854754379994318147230992965) * 10 ^ 70 + 803159795598463402257676270066452192107362843274856484145969664055406) / 1365430337030457401667605

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_134 : Polynomial.coeff recurrence5ExceptionalProduct 134 = ((8480015418893767224474518794749540747099181 * 10 ^ 70 + 7146073865681141527978156809201256538701649844930633844694013248819831) * 10 ^ 70 + 5776755509860203617235483828155309165618943636005660343980037886684069) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_135 : Polynomial.coeff recurrence5ExceptionalProduct 135 = -((49077015700621991632613698067503718627940525 * 10 ^ 70 + 4145786091507004373510140029802183452879647999431952299049481477899232) * 10 ^ 70 + 4298221732077436504363791918121823131135597990995728614411999969538251) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_136 : Polynomial.coeff recurrence5ExceptionalProduct 136 = ((465808660722656360029775121506090304906136260 * 10 ^ 70 + 3092239154202711855487984944588993756212474325877562679838686877893491) * 10 ^ 70 + 6753682675292017337267533082631138172903947463933754754740967330538021) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_137 : Polynomial.coeff recurrence5ExceptionalProduct 137 = -((1966575449816242274907135403999408503431724449 * 10 ^ 70 + 5561991734786797645041496553622764682930218107808263781393474021886183) * 10 ^ 70 + 9310904270427184030808068645880787021329642480469537863680927430162177) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_138 : Polynomial.coeff recurrence5ExceptionalProduct 138 = ((381917838545865109085927230092444165515085340 * 10 ^ 70 + 3536586494786214957045339866143367085522051402626812251220475381332021) * 10 ^ 70 + 6035242141721271826128286820816150321606737542016275829680593455154683) / 1365430337030457401667605

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_139 : Polynomial.coeff recurrence5ExceptionalProduct 139 = -((27775610450808985680933142528192320067874154343 * 10 ^ 70 + 846627741181542551193861100424151411352459162123135041812371234753166) * 10 ^ 70 + 737109005783703007468379419919984215932615745880791203052024725769057) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_140 : Polynomial.coeff recurrence5ExceptionalProduct 140 = ((95550663312350749396894892018960348734657763493 * 10 ^ 70 + 2610364353979684375424811844966766487542629678295841960399832412376661) * 10 ^ 70 + 9053358002697729854185087951831185201832120956056772402155173089749831) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_141 : Polynomial.coeff recurrence5ExceptionalProduct 141 = -((15654793858973566606671736650877807332941217739 * 10 ^ 70 + 1937026385180917309156351266393936412124174397293847999673668136296453) * 10 ^ 70 + 8293746195930952795718258944030280967723391311013391841392400731810208) / 1365430337030457401667605

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_142 : Polynomial.coeff recurrence5ExceptionalProduct 142 = ((981902882969343212982511942582990813362966026380 * 10 ^ 70 + 6409099335636986530156975498255583272809359799792890591664382069684541) * 10 ^ 70 + 8461890139816887714630427905265950571346207868113051459474036530284297) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_143 : Polynomial.coeff recurrence5ExceptionalProduct 143 = -((2957532144241128813374444776434196097360708409874 * 10 ^ 70 + 3454159480093984234290103231338760894380727067552811290061482427081604) * 10 ^ 70 + 2176271800501678826568089373544396174609904422871345054961704938316081) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_144 : Polynomial.coeff recurrence5ExceptionalProduct 144 = ((4289336560904017709841966701098241661756374234998 * 10 ^ 70 + 2830007048933907171023649385897451029378682424436675138314652982046684) * 10 ^ 70 + 9638345619935304873320411796625844344190214941052247050357551901521629) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_145 : Polynomial.coeff recurrence5ExceptionalProduct 145 = -((24013246373869666584886511047669951409948574202976 * 10 ^ 70 + 1124435473263279826029363336518048449587649297876000349642308681013002) * 10 ^ 70 + 6304650429779415563507911805275564073971206049460275308898240695422137) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_146 : Polynomial.coeff recurrence5ExceptionalProduct 146 = ((32488028901496188918503711184129336046760013355878 * 10 ^ 70 + 6113350552543419580261800556816371299834293193226545069697633926789480) * 10 ^ 70 + 7240025424732193363221633298149689462385043979019217933381859221645981) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_147 : Polynomial.coeff recurrence5ExceptionalProduct 147 = -((170187181856000828102700468691101639677308966304486 * 10 ^ 70 + 6943307308548274734675082332441865903733905166756574923649791694577520) * 10 ^ 70 + 3025742714132661291441478967290459583624850422537650201239630982042207) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_148 : Polynomial.coeff recurrence5ExceptionalProduct 148 = ((86397250759807533330010774781866108759105785289651 * 10 ^ 70 + 3012773119529750208765260030328303774956701970983722507243914682136146) * 10 ^ 70 + 5896403806471893039570517575165270893338959682646984919807977072545747) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_149 : Polynomial.coeff recurrence5ExceptionalProduct 149 = -((531829858233000555767488479693471527096202704940910 * 10 ^ 70 + 1557637305402009827111247018445952573537199668095147798035632607663032) * 10 ^ 70 + 6745932095812783984354533959295585783302676061342397401608156840824573) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_150 : Polynomial.coeff recurrence5ExceptionalProduct 150 = ((1271314094870406785703014884980446210075450798498465 * 10 ^ 70 + 1452566256816856966813644814622470961735556575612233574073363133317855) * 10 ^ 70 + 3221031012018817731450248004093596523028551401964463860765286772521119) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_151 : Polynomial.coeff recurrence5ExceptionalProduct 151 = -((590496567161083581213945415583347794393424955674515 * 10 ^ 70 + 9489282224970825405745702647783931893593373256951613574886989061067525) * 10 ^ 70 + 6586128830177392879331504741515149163354297974502550490190671942383823) / 2730860674060914803335210

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_152 : Polynomial.coeff recurrence5ExceptionalProduct 152 = ((13331269350963618133042095639988490488726862360257544 * 10 ^ 70 + 3230630840236042487058644465585396874593488904346535106499509293306469) * 10 ^ 70 + 6223364324297440895706930978905643883984909905485432403277625930982247) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_153 : Polynomial.coeff recurrence5ExceptionalProduct 153 = -((29273553989177639554023555945432168707758399125888199 * 10 ^ 70 + 3608298811257476244192891153353739892672688672799321556792110113743476) * 10 ^ 70 + 2275673410093483175538767768420134597591270918032947803169536096042599) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_154 : Polynomial.coeff recurrence5ExceptionalProduct 154 = ((31275167814788014580976036870819660388659276254301607 * 10 ^ 70 + 3734822147528516156247726918521209084863396572081573538903710155895768) * 10 ^ 70 + 1314457624787848517403103934220939747461803924482660500096006994996541) / 13654303370304574016676050

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_155 : Polynomial.coeff recurrence5ExceptionalProduct 155 = -((26021886381007161971912421920719628677380488040493819 * 10 ^ 70 + 9671454449162094057641224791486888026933976188628488415908034379172193) * 10 ^ 70 + 9422787836998431023052843470791894502746728439234991344967002353686829) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_156 : Polynomial.coeff recurrence5ExceptionalProduct 156 = ((263551220152590582955654840306262363185024284111930520 * 10 ^ 70 + 3414174481811693660705097460806973920784149609739427699573140053656245) * 10 ^ 70 + 3885663671200402973828426908637073996466922390478991739914629088838923) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_157 : Polynomial.coeff recurrence5ExceptionalProduct 157 = -((130008143596845764586613432659428537934378179326731221 * 10 ^ 70 + 6936041492206329809627699774746231527159854153624567445007574533315601) * 10 ^ 70 + 8458327447753503671675205029098935588825829238437306389930386810112699) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_158 : Polynomial.coeff recurrence5ExceptionalProduct 158 = ((249953625286963303816522452238756266366964335596603792 * 10 ^ 70 + 9414761667173478450922796005022202311978064916187170631163051493138921) * 10 ^ 70 + 3512892435617225937798298639775751360280592019182475091543377504424231) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_159 : Polynomial.coeff recurrence5ExceptionalProduct 159 = -((93669726664990706078736464811072429340698983090274241 * 10 ^ 70 + 2349898943949204016484272913724280558266287877849019824615632507715353) * 10 ^ 70 + 1329571543807622471734441537179484175384346934801437376584926757614314) / 1365430337030457401667605

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_160 : Polynomial.coeff recurrence5ExceptionalProduct 160 = ((3421702018302135017726869831973993251527016255176290371 * 10 ^ 70 + 4405498655970203875545660946851897038744571748371425689771997754574327) * 10 ^ 70 + 5467400406614858839462006243161715848624629463006291944411066185170189) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_161 : Polynomial.coeff recurrence5ExceptionalProduct 161 = -((6092925588623668215809833737908151987709316575101700711 * 10 ^ 70 + 6663908807713847218666055480051108126311304090181517373786227881301921) * 10 ^ 70 + 5776839311315031019825692096863970398495102672070015214797062214684619) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_162 : Polynomial.coeff recurrence5ExceptionalProduct 162 = ((528936978471590355456607642682313259014121901957567399 * 10 ^ 70 + 8081279859861567803144421962568143570146040150922347134003742107792867) * 10 ^ 70 + 926424785657090792893540688263835288925954114708827015153436720028163) / 1365430337030457401667605

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_163 : Polynomial.coeff recurrence5ExceptionalProduct 163 = -((3582087539951390765220471575976362691323674691831614641 * 10 ^ 70 + 1103735648839344050401598353388157243536703337166511699714569510031713) * 10 ^ 70 + 6539303250367014205154959884007798613776343685571611386006077469086747) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_164 : Polynomial.coeff recurrence5ExceptionalProduct 164 = ((29571189855600637133272731220489457383486717901184378253 * 10 ^ 70 + 6683733224294922716677040133630438677455257599106183257270703661979819) * 10 ^ 70 + 4630576075366876430830125153290240492984368600995087597077625350778351) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_165 : Polynomial.coeff recurrence5ExceptionalProduct 165 = -((11903476194977292952606220402648144376239480363407297222 * 10 ^ 70 + 2169564486558637711386148240320573570448187347084081772883844987950409) * 10 ^ 70 + 210040078877537449997022453012865014055759660183747491678804788090402) / 6827151685152287008338025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_166 : Polynomial.coeff recurrence5ExceptionalProduct 166 = ((74765056459692902610445509585314424797517591930095676675 * 10 ^ 70 + 9449285321223221790491850621210163458458283270640895043133792070980318) * 10 ^ 70 + 3617753461917709845179029689897612317636330039511626380359611069139459) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_167 : Polynomial.coeff recurrence5ExceptionalProduct 167 = -((114484146960830040761784590000426160700253847519769218151 * 10 ^ 70 + 4755306136721839280514529348801130060136375876962639416195216991797788) * 10 ^ 70 + 5293245284709706064781511161950952971832110282338807686914072648392631) / 27308606740609148033352100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_168 : Polynomial.coeff recurrence5ExceptionalProduct 168 = ((34187629675770153988611781184366101330116821268212279848 * 10 ^ 70 + 949314139829272036745755517793697649456722110134836871964770294651292) * 10 ^ 70 + 4081874409615631018825044724771861613023063061858107954420650238340919) / 5461721348121829606670420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5ExceptionalProduct_coeff_169 : Polynomial.coeff recurrence5ExceptionalProduct 169 = -((124421700690908936450540684770825479311801455865947302352 * 10 ^ 70 + 7186724168617404898587527209074533445191790018097577361610468077480183) * 10 ^ 70 + 4700654839719789857874899743883843212990306916685047678945951941267027) / 13654303370304574016676050