Recurrence 4 lookup certificate: Scalar0Exceptional 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.recurrence4Scalar0Exceptional_coeff_74 :
Polynomial.coeff recurrence4Scalar0Exceptional 74 = (405204554204169743737263309349606827256694291334622046984371 * 10 ^ 70 + 5215844235902207773368946641431006715795364071290144464181802162875384) * 10 ^ 70 + 2215448018198927764156514469846700959068790612247262995885009098318425
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_75 :
Polynomial.coeff recurrence4Scalar0Exceptional 75 = -((9432935662313614019035721919410545651279849026654361087786420 * 10 ^ 70 + 3366865941747471045749024105224935820119996422440907923044985836926568) * 10 ^ 70 + 3325433954624746727541600224178570132301437802911292572471311684640569)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_76 :
Polynomial.coeff recurrence4Scalar0Exceptional 76 = (212130284673053924663427272551830532463549957757963797071454735 * 10 ^ 70 + 9252845257173806445539313067880862239549892494538560302265286060390626) * 10 ^ 70 + 7397420758848436045744399389527715694514737541601093807472796140888211
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_77 :
Polynomial.coeff recurrence4Scalar0Exceptional 77 = -((4610013120870488436566814875599416708853077248448451181870519639 * 10 ^ 70 + 2422009524075026971274929150393538310665071934393110087869280916661568) * 10 ^ 70 + 1476965544923806789744845376242790957550475281370358637087038359536915)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_78 :
Polynomial.coeff recurrence4Scalar0Exceptional 78 = (96849879236899181380831385389296606994785096059336310145920729811 * 10 ^ 70 + 9521897975011486413573789532501069553333160236592249915057376599204736) * 10 ^ 70 + 7770085344482570576971365826146514125896218097437632295877216252714787
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_79 :
Polynomial.coeff recurrence4Scalar0Exceptional 79 = -((1967616656153485874728920987866130491869060370208244566584389578925 * 10 ^ 70 + 7748216144788349606782610331570203065342775299920644763086871763044885) * 10 ^ 70 + 7625057696493482521739911687784466787490547894709000277127187090224476)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_80 :
Polynomial.coeff recurrence4Scalar0Exceptional 80 = (38669332611927934537202811088931894592266264206819527923180336663485 * 10 ^ 70 + 6223560029458379792713502558410174027587243419533918536180679290028192) * 10 ^ 70 + 3953563540934243300042456027851479898434122053482223085202804141696068
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_81 :
Polynomial.coeff recurrence4Scalar0Exceptional 81 = -((735378776984603477060225367470583534458945090309641771631133726954648 * 10 ^ 70 + 356605930414601687451041850302701042162468636093491890318894048550890) * 10 ^ 70 + 8185046335344577479018789131017531353597307468315986852620735604111256)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_82 :
Polynomial.coeff recurrence4Scalar0Exceptional 82 = ((1 * 10 ^ 70 + 3536307263594965893477809174490980976754265450736500279567945553418672) * 10 ^ 70 + 4389027919848663167573947522069923561045750651759731303035760893452130) * 10 ^ 70 + 8437032498430596456425382015215177733476896626219987148193306163187014
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_83 :
Polynomial.coeff recurrence4Scalar0Exceptional 83 = -(((24 * 10 ^ 70 + 1242219115969500515001054272428742902646905284179114294206075167855923) * 10 ^ 70 + 8147505107129651909088850644500127658576287416518973475585828275586106) * 10 ^ 70 + 9905025877270437828777313146024611134875993895409279057765523121936018)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_84 :
Polynomial.coeff recurrence4Scalar0Exceptional 84 = ((416 * 10 ^ 70 + 3727704131541538608131814196223466660631496878586673010441409791545904) * 10 ^ 70 + 1694519605617182085187712494729726147070582806486864620993351038399167) * 10 ^ 70 + 8608486299112154835011591106397370948502512028438969656289704820234455
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_85 :
Polynomial.coeff recurrence4Scalar0Exceptional 85 = -(((6961 * 10 ^ 70 + 3168881799959264884877177433386500290203659217099271829462673171826427) * 10 ^ 70 + 2093440955577691540651321335275753206335230064152803874794591903136800) * 10 ^ 70 + 4574049415038506995911783208179519732577622788067721857889448440405340)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_86 :
Polynomial.coeff recurrence4Scalar0Exceptional 86 = ((112765 * 10 ^ 70 + 6055090280336262157088035206282240914650059840335530891014649049073119) * 10 ^ 70 + 6279400634252318135703328908511837922681529444196558658154552772563119) * 10 ^ 70 + 7166000288377332299226165565700195145516100550527581571563119535330703
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_87 :
Polynomial.coeff recurrence4Scalar0Exceptional 87 = -(((1770213 * 10 ^ 70 + 3161947243527126430636690760590288102815255477853759196419070641985235) * 10 ^ 70 + 3877398509296563667836092701180880555149134997689712039651088106301782) * 10 ^ 70 + 5449918561297660266590206525589829437723565829505953193920850252782397)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_88 :
Polynomial.coeff recurrence4Scalar0Exceptional 88 = ((26934978 * 10 ^ 70 + 2386524976420147020760559352616430788069356453416539187818175627354666) * 10 ^ 70 + 4893762331703429100262660023861036670436294965193812418002005428690326) * 10 ^ 70 + 859665843240246453272511807755953663522857348593634722292054148588235
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_89 :
Polynomial.coeff recurrence4Scalar0Exceptional 89 = -(((397299728 * 10 ^ 70 + 3677170128860503635320953500638313114714858997806259563541985315640884) * 10 ^ 70 + 2812420720639550665607718187460785953930628548727507522671421357612555) * 10 ^ 70 + 8756586910966363869351497033007373023929082467278719926770403801864128)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_90 :
Polynomial.coeff recurrence4Scalar0Exceptional 90 = ((5681831403 * 10 ^ 70 + 7299184380684803455319915747143421359087270636330096337897254851344128) * 10 ^ 70 + 1308046449354605939391451482443775475334553979679904693015391203127998) * 10 ^ 70 + 1256825596045694229392467091548893649874821761761476468503132291735330
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_91 :
Polynomial.coeff recurrence4Scalar0Exceptional 91 = -(((78790327383 * 10 ^ 70 + 6088603922644461226631683964202766569407667765413420572121127667838606) * 10 ^ 70 + 1047427632650473847383542486981042920251358292727635252625434696647332) * 10 ^ 70 + 4937798376078658394238861470176950193243478347297760186322058379433132)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_92 :
Polynomial.coeff recurrence4Scalar0Exceptional 92 = ((1059509703603 * 10 ^ 70 + 8823839970425373440611908096473720481669628231325177886900789324148446) * 10 ^ 70 + 6958489043299946445548728454815256207804511110718963338613906408843625) * 10 ^ 70 + 6625554186685698484983103881793601267383660130453749664785918813705865
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_93 :
Polynomial.coeff recurrence4Scalar0Exceptional 93 = -(((13816650056361 * 10 ^ 70 + 8475785929040728001892145828595337106139999721104879161435318045803002) * 10 ^ 70 + 8143690042589107310202462100166178741019260639084287177137683650776883) * 10 ^ 70 + 6941372245316781233322896863799810151341708815742968210780529251595100)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_94 :
Polynomial.coeff recurrence4Scalar0Exceptional 94 = ((174730219304198 * 10 ^ 70 + 5318175276874235816677783225718939773915871787513521583965877298203009) * 10 ^ 70 + 247098058594507938653828660623263672190524173066710762284380704354771) * 10 ^ 70 + 2342226459921431109059018076041487643148837156033197494519440145728053
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_95 :
Polynomial.coeff recurrence4Scalar0Exceptional 95 = -(((2142807948716539 * 10 ^ 70 + 4987917658789487813171011416563218868504117679983011803985016674470906) * 10 ^ 70 + 5450245548138692473119849914962254322530385281650562212139966003888330) * 10 ^ 70 + 5435927280131862879558922072765906015783510022465237290424010041766756)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_96 :
Polynomial.coeff recurrence4Scalar0Exceptional 96 = ((25480543210882048 * 10 ^ 70 + 9844565635753006916660873467685634883842589664438801187333431900381648) * 10 ^ 70 + 7327602255907894400880604392501143531801580507282767795032198248536139) * 10 ^ 70 + 8088815523378779545336678798687455817243025075736128063695556711266013
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_97 :
Polynomial.coeff recurrence4Scalar0Exceptional 97 = -(((293750285538612148 * 10 ^ 70 + 1275243402554544345428553577347131315884336019491515359126047866600862) * 10 ^ 70 + 6510924290348581423481629653661064746662914103943143278112880831692195) * 10 ^ 70 + 720862932896095321951272756399800824014718568238443918548188737970594)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_98 :
Polynomial.coeff recurrence4Scalar0Exceptional 98 = ((3282423729833663093 * 10 ^ 70 + 6817553583411474489366491298136933918057261346446418424527842427935005) * 10 ^ 70 + 9025713864895426727557765351610834291363220939134289223207306926097185) * 10 ^ 70 + 7470980432274350220162032988800500278145749466922769976670097291017460
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_99 :
Polynomial.coeff recurrence4Scalar0Exceptional 99 = -(((35540382744495244696 * 10 ^ 70 + 6562119442606343348137528411768238170024089908586771896861825396274282) * 10 ^ 70 + 8673613107809808056936709638505374649164728831353729425955063535227634) * 10 ^ 70 + 2086150186955854649054281148656092546845088063792041287796127893395764)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_100 :
Polynomial.coeff recurrence4Scalar0Exceptional 100 = ((372715892401984242075 * 10 ^ 70 + 8429261952142882906118956581339186667371668741574650957651557313011000) * 10 ^ 70 + 7794612402182099051400189034907611249203003645640410426745533557114726) * 10 ^ 70 + 4880095863481798298967450683613472811661711331027766789834986769084619
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_101 :
Polynomial.coeff recurrence4Scalar0Exceptional 101 = -(((3783729179481727841307 * 10 ^ 70 + 2559954668079188906434934362088808993312773745825685239525149825226251) * 10 ^ 70 + 6797466998794423631219343614742042493135518341594253027828531730562655) * 10 ^ 70 + 602725882124197207354831406802893083516639746592159088740544983761759)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_102 :
Polynomial.coeff recurrence4Scalar0Exceptional 102 = ((37156124862885503376308 * 10 ^ 70 + 8796664271934157767711666528156920706896884029276891076939420552325452) * 10 ^ 70 + 8439555287915180931765371216910566245175283283018240692003439400197866) * 10 ^ 70 + 3160288606626936631860806538538784022214659110500985380917517513865012
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_103 :
Polynomial.coeff recurrence4Scalar0Exceptional 103 = -(((352607150493247252920850 * 10 ^ 70 + 1447091214618415214952289050023998172965156114725066795876584150693197) * 10 ^ 70 + 93046615360404156899910454185776488694633920522062331881040655682147) * 10 ^ 70 + 5090841885494725549710455126560359274243824314371606150835289339842230)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_104 :
Polynomial.coeff recurrence4Scalar0Exceptional 104 = ((3229607952634835812903987 * 10 ^ 70 + 5851798557713312222060654296964791503639579216822535550514705381016087) * 10 ^ 70 + 9481862520894264857867090368037430877430668570260131919552529893794378) * 10 ^ 70 + 4102115400868155176870425251011678691074439913273868839300431491888118