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_231 :
Polynomial.coeff recurrence2Scalar3Exceptional 231 = (12957158075663960194200655702434773035177256410387717411022 * 10 ^ 70 + 9655032796159165635654766297170458392788150935988452571311541631915701) * 10 ^ 70 + 2077655828254162430764270247922285350974599881089465685090124091384085
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_232 :
Polynomial.coeff recurrence2Scalar3Exceptional 232 = (2224019137007319522126086341697327339042235107858205999736 * 10 ^ 70 + 586746372493717633022541609600136316225811005366102459891736366527847) * 10 ^ 70 + 7469299044689618145485223902460947610185133016491097730680420472165299
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_233 :
Polynomial.coeff recurrence2Scalar3Exceptional 233 = -((9356815670274335496880946201465161693926779918718387413495 * 10 ^ 70 + 9765191792840187349735496804199809263599633791617992848376996131832868) * 10 ^ 70 + 7427844212445746890947444703546136030294244145451018535368465464181749)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_234 :
Polynomial.coeff recurrence2Scalar3Exceptional 234 = (11105152343626154668045888774375321300956600145965534893986 * 10 ^ 70 + 2250818916725213695628128427486505227771011797582140903556110616180129) * 10 ^ 70 + 9290150480274792020267839016193356034464011094533215390451307660279276
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_235 :
Polynomial.coeff recurrence2Scalar3Exceptional 235 = -((9860173595990458143173182506872034452476137251360596358241 * 10 ^ 70 + 188841321093815122605597055409418336979163916072609011048014260261227) * 10 ^ 70 + 9675589986441578905830508204059937434902105800394811196310216027615491)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_236 :
Polynomial.coeff recurrence2Scalar3Exceptional 236 = (7410966626328815223509944617131441708448292492839557825405 * 10 ^ 70 + 7040494963897801866620539416552227447095831880466125138056809195517200) * 10 ^ 70 + 3574285541250808888587354553367972740244451193354698490224702325990100
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_237 :
Polynomial.coeff recurrence2Scalar3Exceptional 237 = -((4878326235987292619531224938942710714070893764497675898663 * 10 ^ 70 + 7090042421035727935908720771314538001239479611175468193342196722925417) * 10 ^ 70 + 7775650309650609594788201999155011080190746432945506105245869561705373)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_238 :
Polynomial.coeff recurrence2Scalar3Exceptional 238 = (2816238961166758967911856083502705730543824223892373065097 * 10 ^ 70 + 4088058255452708664896806041171209164103600245690212958141882660265038) * 10 ^ 70 + 4774884009985873896417861684612239299719510228139492417588583834228058
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_239 :
Polynomial.coeff recurrence2Scalar3Exceptional 239 = -((1384736432242239428054842961091859187483851124289373532333 * 10 ^ 70 + 9995219006846068915691811084302865748823339062727460932420015932784035) * 10 ^ 70 + 7422780779353285188424150619493131028357776479165793169378362265502958)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_240 :
Polynomial.coeff recurrence2Scalar3Exceptional 240 = (522381708162302907850482450629921399932114228093917011016 * 10 ^ 70 + 6572738653441974839879978861153066923322199361227854136311233651540778) * 10 ^ 70 + 6538793663035042241722485710099465172604962276178322322265879985424031
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_241 :
Polynomial.coeff recurrence2Scalar3Exceptional 241 = -((79295232486217077589317082407215067683073883710740732854 * 10 ^ 70 + 2436741099732080718685593285713485544840561197482231428654241982726441) * 10 ^ 70 + 353976610064903818598285788095217796977213346793520962443956140764339)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_242 :
Polynomial.coeff recurrence2Scalar3Exceptional 242 = -((100289344383751128713864617161448814315573168443310813465 * 10 ^ 70 + 4304815453609453516655995565600580822064215843331468018710342864840807) * 10 ^ 70 + 5922954222489996351060547602861054011279211277594589230687921081108507)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_243 :
Polynomial.coeff recurrence2Scalar3Exceptional 243 = (139171282482993687715507559274493978595627818616944638940 * 10 ^ 70 + 9874812294118946048617418029431427901023825783692633545194526605344396) * 10 ^ 70 + 8140308493189715193492366102171908332898009617425225829555307397948161
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_244 :
Polynomial.coeff recurrence2Scalar3Exceptional 244 = -((117900048618193484901483453358293991809591480209934271774 * 10 ^ 70 + 2699688023177504178160525092030739429657822905456219584349275810586901) * 10 ^ 70 + 3556267283031590338154421304714362264046627457304356066026789629420845)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_245 :
Polynomial.coeff recurrence2Scalar3Exceptional 245 = (80982394731794698860555308145301562760685944398100540962 * 10 ^ 70 + 8157892269386699396849412547297378346372792753933482525895568534585158) * 10 ^ 70 + 4939115561310296072344458194992436297860881576056119723242633762721960
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_246 :
Polynomial.coeff recurrence2Scalar3Exceptional 246 = -((48233804573770303145734944093112835354328753191664593277 * 10 ^ 70 + 4410559790119041216932526715406538375906668615559081785010055730022638) * 10 ^ 70 + 1469065141314339345450891657195056003799769266464013180672253541188244)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_247 :
Polynomial.coeff recurrence2Scalar3Exceptional 247 = (25405861019127677275238671800048889634368734347941046043 * 10 ^ 70 + 8542973252132911220663606268423032099660332128221984959455739497396186) * 10 ^ 70 + 5108556031718656131782626007536855541828769899813570979700111633849359
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_248 :
Polynomial.coeff recurrence2Scalar3Exceptional 248 = -((11793042466377658825544099950917618001796188684318108329 * 10 ^ 70 + 7582001559468195832033263325682549718082408422125742863074706611619696) * 10 ^ 70 + 2744782306454290698241620425453400866619130199789593337406739672162065)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_249 :
Polynomial.coeff recurrence2Scalar3Exceptional 249 = (4682331102484454763868582250290960337968564619937820245 * 10 ^ 70 + 1167561196790125069050177233956792136657560630457051237777025769261167) * 10 ^ 70 + 1492086758212303970419727224723110795209029384255760572923792336453742
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_250 :
Polynomial.coeff recurrence2Scalar3Exceptional 250 = -((1442480701673880241765693588652322439534419879521200960 * 10 ^ 70 + 537889954576602993128111781957572000030261237740681178039739929848126) * 10 ^ 70 + 5670969460707095572314772254918662919605033939999277664807352416619746)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_251 :
Polynomial.coeff recurrence2Scalar3Exceptional 251 = (201287531205853770649235532353396230888976004895467392 * 10 ^ 70 + 9048871306540834329347061156573503581711341932789848160362316015884495) * 10 ^ 70 + 3779049286635973577598564534464908852014480642397441072187100487467491
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_252 :
Polynomial.coeff recurrence2Scalar3Exceptional 252 = (149978173085476751588289920302515041538963788334592357 * 10 ^ 70 + 996875448061073096184530191630647820842339309982172600123971770975864) * 10 ^ 70 + 2398754446758113380514128179360185592525548620855510737686976751792167
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_253 :
Polynomial.coeff recurrence2Scalar3Exceptional 253 = -((175001788676926896678071638684588452977185516001718886 * 10 ^ 70 + 3545406785781641460682957526243772679794918349073417364528547523652014) * 10 ^ 70 + 7095612946404690741978300797455941835406110496518249533589230507567131)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_254 :
Polynomial.coeff recurrence2Scalar3Exceptional 254 = (117755291597731359401463120722276571251344861881567581 * 10 ^ 70 + 6338473832289138737561577667976643371562638828660341866958756103731559) * 10 ^ 70 + 2121764129984372474811028855554007110220402904271372205686227183328099
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_255 :
Polynomial.coeff recurrence2Scalar3Exceptional 255 = -((62889207455403801776776645308637491741399850682126519 * 10 ^ 70 + 9806999769913343586224013817253981672524859239174318131792126133568920) * 10 ^ 70 + 6762271174156720806288613789788429660319697367700850684688893309587854)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_256 :
Polynomial.coeff recurrence2Scalar3Exceptional 256 = (28459680651774683243112492699947470410780718952025208 * 10 ^ 70 + 2320727832169359459251356693625858979137081063135412877224027354415126) * 10 ^ 70 + 8868926619848487547134354240487004319496491472816895027889432250787249
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_257 :
Polynomial.coeff recurrence2Scalar3Exceptional 257 = -((10981355822420863484832390005185582540112696111148474 * 10 ^ 70 + 2688509447714166877431956959878169314499527318124684133151281914323384) * 10 ^ 70 + 7927670189583712008755033469896951921555387246229229005266217741708680)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_258 :
Polynomial.coeff recurrence2Scalar3Exceptional 258 = (3467655162679000879683393917486636709355607315793633 * 10 ^ 70 + 9062487264663038974960226505975044517593166719839081824146107655200838) * 10 ^ 70 + 1201652053655212643920339767581492920297797120530413661580252412097977
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_259 :
Polynomial.coeff recurrence2Scalar3Exceptional 259 = -((753021961240643154775853298816984738277832643698946 * 10 ^ 70 + 2897830841203948010700417213316562060416675453185269327872472521146648) * 10 ^ 70 + 8566654981905775203547749387610599210171111294088290905083357048583527)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_260 :
Polynomial.coeff recurrence2Scalar3Exceptional 260 = -((13680124187573761531654813352501682809021210237681 * 10 ^ 70 + 4752631357836435802955852138602027782994889993995727854744109742869400) * 10 ^ 70 + 605996386075663686827864976116847588487018712283148742524798277610504)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_261 :
Polynomial.coeff recurrence2Scalar3Exceptional 261 = (130905704340158568957134224920511778054773199919525 * 10 ^ 70 + 8730060586301257124552333488394311695384394277561190047936440862578240) * 10 ^ 70 + 802519577640067896326014217717002140821295082929539210465573911481028
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_262 :
Polynomial.coeff recurrence2Scalar3Exceptional 262 = -((92030443608458536342994974377209726549420893154155 * 10 ^ 70 + 9208445344927608664060677690423594389360640981173805863287358164671974) * 10 ^ 70 + 6724121996936426927050653698463457196407847415024664247891973423093613)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_263 :
Polynomial.coeff recurrence2Scalar3Exceptional 263 = (45427548110480653247833547401705963309787422988877 * 10 ^ 70 + 3926118190338373163206279105435205676317513435989647055722825154940343) * 10 ^ 70 + 2667991416444846425981780377809379319513467617897739679541918598773458