Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar3ExceptionalPart0.Coefficients200To230

Recurrence 2 lookup certificate: Scalar3Exceptional 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.recurrence2Scalar3Exceptional_coeff_200 :

Polynomial.coeff recurrence2Scalar3Exceptional 200 = -((17739344263302481876101992579904989603105428945923440367693 * 10 ^ 70 + 3452629089549792869222739479166755955842530091233396051868023794743344) * 10 ^ 70 + 7974252070141015736840054817252087446866993775557920492318761829417599)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_201 :

Polynomial.coeff recurrence2Scalar3Exceptional 201 = (41799180150505857147452316550132217017693035460584069275329 * 10 ^ 70 + 2069562984132180387694397480749309877586589165387857659853970980094602) * 10 ^ 70 + 5422835084869697304749114855763048389125286028856663735803259472539099

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_202 :

Polynomial.coeff recurrence2Scalar3Exceptional 202 = -((76198830639460294363353376700091525071519301557087986851141 * 10 ^ 70 + 9401246609497558554742233123486959055670453299004424642590168937001156) * 10 ^ 70 + 8556822322022288670884026679739340987562644154454216929378430157817699)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_203 :

Polynomial.coeff recurrence2Scalar3Exceptional 203 = (119692024854759281429646037532373745936764929335893532079843 * 10 ^ 70 + 1393651455359890346471926334237031172190088340042368734479519017809743) * 10 ^ 70 + 4898248050013241025127823524395321187518027665613430882263780599274143

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_204 :

Polynomial.coeff recurrence2Scalar3Exceptional 204 = -((168045747222649796386028001975470199540783952382542006060336 * 10 ^ 70 + 8732888445117408144082930173331627868084965606200830054341376402912917) * 10 ^ 70 + 9266693208385568045947185472179385090751011319482586315056104209974628)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_205 :

Polynomial.coeff recurrence2Scalar3Exceptional 205 = (213748758183979505456574652784459982395284501789477027077389 * 10 ^ 70 + 3922489874628473342443604736517394073933460391297288718793273912322122) * 10 ^ 70 + 2630308201563569420936470613501058952008332372155529843367055437228430

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_206 :

Polynomial.coeff recurrence2Scalar3Exceptional 206 = -((246581637234929928263764004163010253894443779081160352770954 * 10 ^ 70 + 7727472885924093650717083297011262472080253270921433090415614008989140) * 10 ^ 70 + 458920377102168824266686779941246685260168606462279643624451573142127)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_207 :

Polynomial.coeff recurrence2Scalar3Exceptional 207 = (255209842571688976273715062567353211541475032533927666027955 * 10 ^ 70 + 2824532316545625910832721209079629193479943614132286037771044375757497) * 10 ^ 70 + 9799026258514228433572869137096854631216048066046037145864771257609923

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_208 :

Polynomial.coeff recurrence2Scalar3Exceptional 208 = -((229663286235698364425887167889585690132983319672182946889104 * 10 ^ 70 + 3451228043951142429607018469674428335051053005643710285199341091775361) * 10 ^ 70 + 4833008124019630989441076916659758568183562348062080005034575986708133)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_209 :

Polynomial.coeff recurrence2Scalar3Exceptional 209 = (164217655687470098066083054292299285999831194146026567076833 * 10 ^ 70 + 2486409326936162542556284685041407077464059808695232872202271101292860) * 10 ^ 70 + 7334339958813011390833027264466482350940173841825748097705635196721545

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_210 :

Polynomial.coeff recurrence2Scalar3Exceptional 210 = -((59915715959615373757097909636540895497385984363683489569841 * 10 ^ 70 + 7513317037547417884419414968262921845547900286351097828815966743192809) * 10 ^ 70 + 8922421418972755946135473854508417040462696459317172494070386066566288)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_211 :

Polynomial.coeff recurrence2Scalar3Exceptional 211 = -((74112008914907090092709216540216185910388359994494396488283 * 10 ^ 70 + 8327198796751904506182608203593455869012432779172305266237714935432953) * 10 ^ 70 + 6822027112170303520355411552837082317022385252764824439273890618920764)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_212 :

Polynomial.coeff recurrence2Scalar3Exceptional 212 = (221170089156471697686008246075442844791371516043688415458212 * 10 ^ 70 + 7539379106391733563308706540877817820458798011011152059415421612538860) * 10 ^ 70 + 4368086375325264589592453450646688532480466368534235842651427137014932

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_213 :

Polynomial.coeff recurrence2Scalar3Exceptional 213 = -((359548333123157843562308555239134167377277018434188247579329 * 10 ^ 70 + 5368265899509507793097757637676266029070764447907229991869518469638305) * 10 ^ 70 + 726570332295603923794245067621032673677664501791452220481895686096305)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_214 :

Polynomial.coeff recurrence2Scalar3Exceptional 214 = (466683383181800184326333316592854885492470644361518073466700 * 10 ^ 70 + 7360447318855835943238797887038893904545862534201584676364030617637189) * 10 ^ 70 + 6808677795243535716619078025817896990189940068171094826687359759094038

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_215 :

Polynomial.coeff recurrence2Scalar3Exceptional 215 = -((523971004995992399095604694131774817366843956324396262990771 * 10 ^ 70 + 2175876860762876011103745232823658616202452845515692963869895908677409) * 10 ^ 70 + 5278557839756443779721868708060458619744287482028855814097498266548704)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_216 :

Polynomial.coeff recurrence2Scalar3Exceptional 216 = (520978204666960227937185631597102060486794165222277165150493 * 10 ^ 70 + 5586954872955775148029387805909312386129398776580696526679003287297294) * 10 ^ 70 + 8441495847291570807709001987139660215275333658448606504768768854780854

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_217 :

Polynomial.coeff recurrence2Scalar3Exceptional 217 = -((457894210175147712265618382312858423374955610751812115233748 * 10 ^ 70 + 1974936612080649337179961181104826656425266562848365052150935093324728) * 10 ^ 70 + 6500449097187963991014773565084989184443641781498944988787863552044714)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_218 :

Polynomial.coeff recurrence2Scalar3Exceptional 218 = (345523216019557139403095342036612031931585675196323843548433 * 10 ^ 70 + 1568033860375670877534219648422673815795796215114671328385928564865445) * 10 ^ 70 + 6824421205680851435251391924390197437358380890646338736089916725576699

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_219 :

Polynomial.coeff recurrence2Scalar3Exceptional 219 = -((202816543663389117619187974434832947541942017936930924992252 * 10 ^ 70 + 1578511847167037353412234283268423255658992676699088150170281519028358) * 10 ^ 70 + 9448455387775530453738697859994051822587824383495599195455422800999446)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_220 :

Polynomial.coeff recurrence2Scalar3Exceptional 220 = (52637671670336499603086911308574198317421195066237373244741 * 10 ^ 70 + 7404315534651701270304804458317835784298268989358434379534331301899471) * 10 ^ 70 + 5342815168666230239585800165424363309182942798961546822011514721820955

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_221 :

Polynomial.coeff recurrence2Scalar3Exceptional 221 = (83079610923425619958498849137266477135154513290100541866637 * 10 ^ 70 + 8352572530674401455927142130187965184066424269547422401160326491062077) * 10 ^ 70 + 4136576058828984786680961807001403106313307690856484170948177119032861

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_222 :

Polynomial.coeff recurrence2Scalar3Exceptional 222 = -((187525638151693752737066411887817267743576107635879043032389 * 10 ^ 70 + 480133808508785209386260580298480867834919337425798392773236058796222) * 10 ^ 70 + 431565686142681541017104937549218799485998923416645632707573333401555)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_223 :

Polynomial.coeff recurrence2Scalar3Exceptional 223 = (251593644523806699083824908075098917012868786300158552961222 * 10 ^ 70 + 5488659697592386241186479366851833004323951099984288607807969341324774) * 10 ^ 70 + 2202303629649977789280771313367139841120748533394161418633532661198332

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_224 :

Polynomial.coeff recurrence2Scalar3Exceptional 224 = -((274417252416547657588583026521429788000231978544343519787245 * 10 ^ 70 + 8863739313339972533662935404580690345015909480444495729506430572416619) * 10 ^ 70 + 6560531845267719335366977959521617732529043164775757467451827476233802)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_225 :

Polynomial.coeff recurrence2Scalar3Exceptional 225 = (262041563359073820627922855995159685922976658469641906122366 * 10 ^ 70 + 7618216992499928539236993072406853081136312116435505465282363201495019) * 10 ^ 70 + 8626289128621339084529105489562295915816248107949028510611530766241332

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_226 :

Polynomial.coeff recurrence2Scalar3Exceptional 226 = -((224866591482521728419009149609052460702954941718979441731492 * 10 ^ 70 + 3512156370867284466733640753798651136449237677301169476761494896148280) * 10 ^ 70 + 4276656843277165879097017242088321217041243223538991631476309136469968)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_227 :

Polynomial.coeff recurrence2Scalar3Exceptional 227 = (174706870481393565243174417628596333079862373807557337270140 * 10 ^ 70 + 1758157812551011995651136890081194903068837604526763120117753349469333) * 10 ^ 70 + 8651738313908036914931955802650087230752246353017226337544734975929911

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_228 :

Polynomial.coeff recurrence2Scalar3Exceptional 228 = -((122239908774802774839680859046823942865002692116544799744582 * 10 ^ 70 + 7573663118926790893891944146011956672315784846496097752642686838316537) * 10 ^ 70 + 7822555196847609276613142932894169500187920367075046786721461556619628)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_229 :

Polynomial.coeff recurrence2Scalar3Exceptional 229 = (75344170560495310454362332011174240894247793969509521885077 * 10 ^ 70 + 5790217610632971683413037739521023967062178328226473047956193872077652) * 10 ^ 70 + 2612054774671161321210824130371685844276051080359771169286864723755408

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_230 :

Polynomial.coeff recurrence2Scalar3Exceptional 230 = -((38479156045962330790302298562844005376065001943684022781914 * 10 ^ 70 + 5085714564534939108182996894032604346575301153046687556245970040957890) * 10 ^ 70 + 9106873855920912684147237316440567022502647834623171084255852347111591)