Recurrence 4 lookup certificate: Scalar2Exceptional coefficient convolution

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_116 : Polynomial.coeff recurrence4Scalar2Exceptional 116 = -(((183346514575472565182275113544458480 * 10 ^ 70 + 1313554325606584246480454390480103723637336157165304283908315218518699) * 10 ^ 70 + 5043419205974208003488984387731376511564125633982087936142157615402415) * 10 ^ 70 + 2616811818090019150794911038212011084589454742329036791166015000232052)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_117 : Polynomial.coeff recurrence4Scalar2Exceptional 117 = ((1528224159845085773549791211644897586 * 10 ^ 70 + 2685863783218331483056400702191588003904448371471993583830452565671432) * 10 ^ 70 + 8560701160217782783894922805473369695301496309976603577221150226490843) * 10 ^ 70 + 1445156487764116454335245166494863465838418352423354997795967106225442

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_118 : Polynomial.coeff recurrence4Scalar2Exceptional 118 = -(((11499449592048197101391599294885052096 * 10 ^ 70 + 9438330741569356807283182308561035972924184313069392689481815648630799) * 10 ^ 70 + 9533660525869676701469054365891325505048077103408022293096705044147692) * 10 ^ 70 + 9478438355716949639587181878562646322993724645192886123187387002421725)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_119 : Polynomial.coeff recurrence4Scalar2Exceptional 119 = ((78935050597835869839248332923844299387 * 10 ^ 70 + 4861786192789788687071708173718220487526251454485392508441323139774857) * 10 ^ 70 + 1960351363899636484364636036950740293701818535566063004091663122148749) * 10 ^ 70 + 424008138163570590483744907453121622912949995033436201978458948465917

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_120 : Polynomial.coeff recurrence4Scalar2Exceptional 120 = -(((492326720372576766866288832766522904772 * 10 ^ 70 + 8673227785414358764616798481723847718047429872042551513853417895964093) * 10 ^ 70 + 9999286409225197395564403538800770511944134214198993091033470704898088) * 10 ^ 70 + 5898210848998511334741773920677133588651612653857501980671847978296215)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_121 : Polynomial.coeff recurrence4Scalar2Exceptional 121 = ((2731583380078680837741404553192637006468 * 10 ^ 70 + 6126628465647184332414916228072625962757480131284761003064183722134576) * 10 ^ 70 + 7624538475514224720865271630785100129205237351966757760099532723139662) * 10 ^ 70 + 8366435911933270529495595902051715896248265694994265958334482299413540

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_122 : Polynomial.coeff recurrence4Scalar2Exceptional 122 = -(((12691889947756002256856949135989912356986 * 10 ^ 70 + 8434954438109070618768005746875522776400330683176994208651296628443305) * 10 ^ 70 + 3103139590171136367855982546499460625310526259139625867025809340080908) * 10 ^ 70 + 8960471031560830858655916366943663852376364536769282483052509095254588)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_123 : Polynomial.coeff recurrence4Scalar2Exceptional 123 = ((39381254357532165299450989517402909968297 * 10 ^ 70 + 6043061155333342482129802432823396197130638272192940274121229478179737) * 10 ^ 70 + 5822281983760262820492199774324136183077923680099297697788335224935466) * 10 ^ 70 + 477791865737463033525819420024936976837020126381729106164073402060361

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_124 : Polynomial.coeff recurrence4Scalar2Exceptional 124 = ((61177122351785499414718863808914915128511 * 10 ^ 70 + 7979081608015293442249569388111472212135034206974084284474101153637540) * 10 ^ 70 + 6584547490548172305101144660459037770751567951664967017729763635260026) * 10 ^ 70 + 5677061722604659381948821593527775300371095311144280833518476527442479

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_125 : Polynomial.coeff recurrence4Scalar2Exceptional 125 = -(((2465991108514156010234356248698495463471980 * 10 ^ 70 + 9284797976577762791667765529266205763642299805515515195004107457997015) * 10 ^ 70 + 3448600252633666450820064574840362010849510407787463699831187591113474) * 10 ^ 70 + 2835802311856057980314138662491501489027825057547696259636801978432592)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_126 : Polynomial.coeff recurrence4Scalar2Exceptional 126 = ((27958618972115298414492877990373609753722378 * 10 ^ 70 + 4306396753039046914376403352591610822077617557939478519474163170062813) * 10 ^ 70 + 5253839195785367027800861755220743693399212083660967531719800625045177) * 10 ^ 70 + 6904621679136151101041724122311076977097054807336490809242999310098367

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_127 : Polynomial.coeff recurrence4Scalar2Exceptional 127 = -(((240569764488697440646937076159524413820224093 * 10 ^ 70 + 5977289262936371898124223040278454046187479279578589553871374205999829) * 10 ^ 70 + 3160720048185136928359606290666916716364181234544762284603936177244287) * 10 ^ 70 + 3442775704069636744582935076127858964354123740134500499619239607375000)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_128 : Polynomial.coeff recurrence4Scalar2Exceptional 128 = ((1784018229405321890999275335649641400740331909 * 10 ^ 70 + 9564965374785000774591836084994684298418702398620494226774504910492522) * 10 ^ 70 + 829303639607144323290668163500947583493512468013171273549386958955239) * 10 ^ 70 + 6782995826674377637175308385915148697765193715892194043209300173465349

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_129 : Polynomial.coeff recurrence4Scalar2Exceptional 129 = -(((11858419375935660260466005247572765578619754284 * 10 ^ 70 + 7570488071007672793661880095431851159896998057690422569275354968000486) * 10 ^ 70 + 5846449985636091468041731591799444825975333986096210458340991773122967) * 10 ^ 70 + 461200191868749656200946613979749332141813184265911646732359147784613)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_130 : Polynomial.coeff recurrence4Scalar2Exceptional 130 = ((71459860490427004708781222113706132041186598740 * 10 ^ 70 + 7728363664444889054295785150754517045203380582608699036027178795927823) * 10 ^ 70 + 1583500843905333868556141904116003077970352531266920463124611509043690) * 10 ^ 70 + 9926760801987831449105208336512584510265954425403670492834159544937230

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_131 : Polynomial.coeff recurrence4Scalar2Exceptional 131 = -(((388184744812426264652274790377321122389353776858 * 10 ^ 70 + 3344985593805900322772130742922788088914100036839350243361165992425516) * 10 ^ 70 + 5146562744711012952351520237394433793851702961133996516979033991214590) * 10 ^ 70 + 9987887533213461202295962846462853807964480407637248015183719028110855)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_132 : Polynomial.coeff recurrence4Scalar2Exceptional 132 = ((1848237967274368580339500460262037807931803099192 * 10 ^ 70 + 676980503353624138730980684414367747161258499077936971145231708908229) * 10 ^ 70 + 904767632956453302023701377284552560503767265470094248647031352151658) * 10 ^ 70 + 2291780851582821416054703516238786917704232208260603424773945399852339

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_133 : Polynomial.coeff recurrence4Scalar2Exceptional 133 = -(((7073272815945886766639795655883757950245820555843 * 10 ^ 70 + 5459890787058805202460207218363153618366458395038493162272544822885737) * 10 ^ 70 + 735980424749569592667454216116821447982083961094125016937803597123198) * 10 ^ 70 + 7804463955956006290194909300568255454867315868050712459371367852767055)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_134 : Polynomial.coeff recurrence4Scalar2Exceptional 134 = ((14207070660475576161470744456201050576710933526728 * 10 ^ 70 + 9196450068745333582497051630961883902949882639679701158112796317667748) * 10 ^ 70 + 5400294914465932910712169719135703985811076521809991019342942895972945) * 10 ^ 70 + 7127728594735603131672608965134917439746636416868211817801420670440152

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_135 : Polynomial.coeff recurrence4Scalar2Exceptional 135 = ((90132913206884898016700751781190773892207495617760 * 10 ^ 70 + 618820978673256019212804252723187860149615100788267939725588029682514) * 10 ^ 70 + 8820182978376511778587306172847190618824476499825547618888689887323530) * 10 ^ 70 + 4517683549577114740478731469486762191731857572483077867869933395869760

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_136 : Polynomial.coeff recurrence4Scalar2Exceptional 136 = -(((1515133553290292639151509361150693070896144689089754 * 10 ^ 70 + 9669227813633769273872227328681162803570415941637713841102445884425256) * 10 ^ 70 + 2911139551537359030614217898638772393673785427627796875447745579693441) * 10 ^ 70 + 7925823971356441621895331528471849680357759791822554107107820046945954)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_137 : Polynomial.coeff recurrence4Scalar2Exceptional 137 = ((13878708166953875157380384211850821962910579058522091 * 10 ^ 70 + 4699372806364147060074932195945671833696761027427091177174639889118336) * 10 ^ 70 + 2556775881410955672583167760018421236071869085168011695133218807900109) * 10 ^ 70 + 8037763418531787167581286054464538976948761392256137930856093371456491

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_138 : Polynomial.coeff recurrence4Scalar2Exceptional 138 = -(((103117443693573760948817730057310879177040281773787906 * 10 ^ 70 + 2000147070788391971993721707056305224783007892055073254508752426272678) * 10 ^ 70 + 9705639939536092253852856429281118593860133353958149207099784151026090) * 10 ^ 70 + 7809482630659511837194542297280245120374928541752564689691232094414020)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_139 : Polynomial.coeff recurrence4Scalar2Exceptional 139 = ((676921950681576377946335627898939438464644361227482784 * 10 ^ 70 + 591368351717812121294564790466300656490283902530654426965358794844841) * 10 ^ 70 + 6817174729355661830699196615773951610335605549317686513456686218853310) * 10 ^ 70 + 1173244006280704644387838396785461220761594384992638101052048780931123

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_140 : Polynomial.coeff recurrence4Scalar2Exceptional 140 = -(((4047748545511214493025726596598404970078464922554957176 * 10 ^ 70 + 5852249888170662913093076348321074673656745375303084009399326440258317) * 10 ^ 70 + 7463708151835366376530725077980104206397300382537605600086549148822904) * 10 ^ 70 + 7814247454841469657005501878801194212732892320451296354636383309789678)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_141 : Polynomial.coeff recurrence4Scalar2Exceptional 141 = ((22287305727084643390943555395391811940911674152195681129 * 10 ^ 70 + 781980150721911663569357009651722393276643905477900858916607220574622) * 10 ^ 70 + 4055873336409290186500385624667285256713275349990767923033642178443528) * 10 ^ 70 + 4887239031997675764172895234174007481939051185196883577164662442173883

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_142 : Polynomial.coeff recurrence4Scalar2Exceptional 142 = -(((112897789936671604837641738048293418899551170469689035634 * 10 ^ 70 + 4660685991416420534288295835389029107927230580805095044106301913601332) * 10 ^ 70 + 5407974448661923291795884737473452838620596135932167737905565070221805) * 10 ^ 70 + 184764042811195780202321441649603152188334219380286295657293111292865)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_143 : Polynomial.coeff recurrence4Scalar2Exceptional 143 = ((518996633386194798597242997247492891839083680072907702402 * 10 ^ 70 + 5924182927033162434030987199743468078751461904744541759074830291850062) * 10 ^ 70 + 6466695267389412882905802322597811676407060178567810948636538553014198) * 10 ^ 70 + 5713015910029872715851485059858539531923770706270814211380391334654823

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_144 : Polynomial.coeff recurrence4Scalar2Exceptional 144 = -(((2083259298505801494878142426032788712483730934386380958413 * 10 ^ 70 + 1890329827059605974861805890972997987131536709205958410460877750395480) * 10 ^ 70 + 4925365359814849123900737863407651385387640072720288494283657492049555) * 10 ^ 70 + 7610029892141844063390406074801573719082955763078045243113825570416360)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_145 : Polynomial.coeff recurrence4Scalar2Exceptional 145 = ((6478358606083984888257366023134838887075803881248684105890 * 10 ^ 70 + 7142274347859859569846184455065778691927950985202192776385060499479757) * 10 ^ 70 + 5347318155857898749160434086952946909978269184871851027211788789224176) * 10 ^ 70 + 7030763335601854169265763725510554340468098685567442046093807593748126

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_146 : Polynomial.coeff recurrence4Scalar2Exceptional 146 = -(((6747578478385700664127052554634912825535734728835797126381 * 10 ^ 70 + 8721769838196656398650172564428579740696839916967132903093562794996185) * 10 ^ 70 + 3734952677165647101441656681559244589621009735103723517168955861872132) * 10 ^ 70 + 4291577035724409219813960288376511692288966979701360178836611756891794)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_147 : Polynomial.coeff recurrence4Scalar2Exceptional 147 = -(((116315406285393116183291992709843482216570701301613303092456 * 10 ^ 70 + 9789515346664552254086450464090523197612208037292135251555007062894881) * 10 ^ 70 + 7998451942644544690944604296191783362587383195407937881661598584849694) * 10 ^ 70 + 1047859902968006762040908593372264299961051677328531385030708732621423)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_148 : Polynomial.coeff recurrence4Scalar2Exceptional 148 = ((1389523958021577752941530435538793587762147963023760872355388 * 10 ^ 70 + 700521926597204142057680328954592842818549527536528880807554553240553) * 10 ^ 70 + 5545143229118201431782671091159911644113115355569344349552207816747810) * 10 ^ 70 + 8237016550558129738449859871118983269485218334704923319379360356843208

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_149 : Polynomial.coeff recurrence4Scalar2Exceptional 149 = -(((10988958344962339193905069122369451123045712303630431261888275 * 10 ^ 70 + 9082360245691237714694094179884812325646955189269406517303336251429330) * 10 ^ 70 + 9221289280793648462276800587723416825952117314536844154602056586843122) * 10 ^ 70 + 6188404311158078427861328687943303989435832630357484130869652308195868)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_150 : Polynomial.coeff recurrence4Scalar2Exceptional 150 = ((73741124866369259767984670313142164348065851152819547091499808 * 10 ^ 70 + 5938182496828883246608865031984899188638450434250956504835574745120929) * 10 ^ 70 + 4583340036572473776968334807034928105551078803805330771167006501503814) * 10 ^ 70 + 8114276572091036730158672527895847525542326484678514798686663539926431

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_151 : Polynomial.coeff recurrence4Scalar2Exceptional 151 = -(((449387784397366632329993577020984504349341726302244843543751964 * 10 ^ 70 + 2744929295415266345123588291432857731872994105505189732517669559243281) * 10 ^ 70 + 7732469644968194524100821897430016334042325401623569056806050799558036) * 10 ^ 70 + 740207189228383841407744674399889960810557138647075426545893307438570)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_152 : Polynomial.coeff recurrence4Scalar2Exceptional 152 = ((2559897981839109983351657731943732789108866502364173583501599998 * 10 ^ 70 + 7965964571022941878191810086314360082143244729027621460093060408265976) * 10 ^ 70 + 279524666824748389439651864968363834754279125483821455446679324641424) * 10 ^ 70 + 3400470444199969520145510481360807577457376750096552061800555164964327

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_153 : Polynomial.coeff recurrence4Scalar2Exceptional 153 = -(((13838318765829643552605204552511118872863938375366222452956835418 * 10 ^ 70 + 6745621959533012946858037039347893202705023487088061368623264917120127) * 10 ^ 70 + 8587425061421776195966468267053328739935050855759634128770685470371383) * 10 ^ 70 + 7025553898764889282883472444110447078413637145184778990826787340997923)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_154 : Polynomial.coeff recurrence4Scalar2Exceptional 154 = ((71633645528026717335025515383320099107631216886085172580429771823 * 10 ^ 70 + 4545248941834817683505092489310212132999557166383286056746149009681816) * 10 ^ 70 + 9365990145493125635220478722918245423759000720357775898271103086278104) * 10 ^ 70 + 1835183883673271244083659535578312819351129154959852931367341937805439

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_155 : Polynomial.coeff recurrence4Scalar2Exceptional 155 = -(((357164229850054765672853955116428287127656758541297711166335093200 * 10 ^ 70 + 169491335147984621130929092682915106662589919081165878202457051155976) * 10 ^ 70 + 8551352659414932637840586367302976930521379519536222110411079604915172) * 10 ^ 70 + 9221630346762235830922082218727254982262455161604363189446846728444938)