Recurrence 4 lookup certificate: Scalar1First 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.recurrence4Scalar1First_coeff_251 :
Polynomial.coeff recurrence4Scalar1First 251 = -((((9357110514433624707422587213 * 10 ^ 70 + 9420132711999283005706538629586794333690492733951986909892902388593612) * 10 ^ 70 + 3062496235725942974888064391577302663962172493375427268061237920957244) * 10 ^ 70 + 7816572834186085343267221464583549882774704118876707415992556404024068) * 10 ^ 70 + 4955261205914857802767803263881538794339298671003828054598330874299875)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_252 :
Polynomial.coeff recurrence4Scalar1First 252 = (((9187650485676071438403236429 * 10 ^ 70 + 6986319819658526238198433990652492217856160552936929587365968915018636) * 10 ^ 70 + 6242221194585283412287160152323105646324213101025369387705126163564879) * 10 ^ 70 + 5830246471676424073624719049532071490440963819227884187861939061777042) * 10 ^ 70 + 2447404313208503810244538375948109951718956502205204141714651444190813
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_253 :
Polynomial.coeff recurrence4Scalar1First 253 = -((((8852422809543305695221086617 * 10 ^ 70 + 1912120193886854329827829027661180475794225808504214323126584472000001) * 10 ^ 70 + 138736057945957402212301931159469521832618491422091160751973096545920) * 10 ^ 70 + 2243297348735784284957316043234507547472709426646663650317182011256293) * 10 ^ 70 + 8223627557024815588288695992703390079014932797281736294170264626713506)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_254 :
Polynomial.coeff recurrence4Scalar1First 254 = (((8361206436111990476365752571 * 10 ^ 70 + 3416826320592960235733097552997357230651119689017008836538599144695590) * 10 ^ 70 + 2460752524766288178277074097232376566298190294887528653127688083824904) * 10 ^ 70 + 2464774642519370268809875119041405812693593321220139460482582508737915) * 10 ^ 70 + 8720711967931244862039738846696012937608850771905471693311749914770605
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_255 :
Polynomial.coeff recurrence4Scalar1First 255 = -((((7731266348164432733192318460 * 10 ^ 70 + 8417019685829994244459381601954821660360812821499482358139199055060268) * 10 ^ 70 + 5133948425307359657796821952147803520080456203125218717372889686340700) * 10 ^ 70 + 4132384496097763158946524054648890435172569365916254733433162792066255) * 10 ^ 70 + 9011464160405532245878248932204019383552125331761514181553418080696505)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_256 :
Polynomial.coeff recurrence4Scalar1First 256 = (((6986353755536327965812155346 * 10 ^ 70 + 2100641106439983343793859856264013741776112470992491039522924367661246) * 10 ^ 70 + 8557413534019030170526942129297938395223852894301970798789137268814119) * 10 ^ 70 + 5857374091242683323648767104007136029083252166540026796003179026435655) * 10 ^ 70 + 262790813930298993947681720880585040223762824365479600309096967823167
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_257 :
Polynomial.coeff recurrence4Scalar1First 257 = -((((6155222323654323006031306434 * 10 ^ 70 + 1632225317586428636212855199802853966937611752266333465407493669968061) * 10 ^ 70 + 726213619949978036368352070312614641847263888770958851474477316151828) * 10 ^ 70 + 1357670798721230569984419080409567117724771515795260389392995171374368) * 10 ^ 70 + 2045488974266302264172907565576984920578476929222368559606724125797169)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_258 :
Polynomial.coeff recurrence4Scalar1First 258 = (((5269789573771078762391109483 * 10 ^ 70 + 2994839037939907954583743301684149823527596824035635636613770295600105) * 10 ^ 70 + 5551501499347350671562282572690892618321084160622889152467351423750746) * 10 ^ 70 + 6646705157970292839782912009416905243581887900613612492722047104732776) * 10 ^ 70 + 1030923850675155389782113473706549145778605231145195339930661363672124
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_259 :
Polynomial.coeff recurrence4Scalar1First 259 = -((((4363107143174338829174718467 * 10 ^ 70 + 9101023741562363719748966603862007707488223415361895093048381117189032) * 10 ^ 70 + 4867464745919738490601746245853595421700126930522943673894354496725168) * 10 ^ 70 + 3592315920030250289571333971594003085904790984548370542486691637711023) * 10 ^ 70 + 2293310675786248395206544666222195290283100262983175542676889238054133)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_260 :
Polynomial.coeff recurrence4Scalar1First 260 = (((3467319500298069214507749049 * 10 ^ 70 + 5436948718859697579043095658130175875740607196585573120984518892562791) * 10 ^ 70 + 5261295884209340804894550203315916235484533820218847313794563420325663) * 10 ^ 70 + 9367341864643062273419801968011102823198078960636061967611836808876129) * 10 ^ 70 + 8262744798940754636048602662047703817762212279811879409031015247992666
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_261 :
Polynomial.coeff recurrence4Scalar1First 261 = -((((2611786305680769919204831531 * 10 ^ 70 + 415564696429846820960592433467340096996303003746356382511488799412961) * 10 ^ 70 + 603138891293873708093300692335941277636598041803907678839421229622359) * 10 ^ 70 + 3662205265347154337870882087970160480839079769299211893181429287255572) * 10 ^ 70 + 6505473895505702794901479843944582422857433811479583766456724751908418)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_262 :
Polynomial.coeff recurrence4Scalar1First 262 = (((1821520020206115095666278504 * 10 ^ 70 + 9257371000150656142513801539124519936069656163695733559029472901153533) * 10 ^ 70 + 5932654234069542449121923647779921640584259632611017011447204139081753) * 10 ^ 70 + 1669338488217136990942436260033483132373609539390079972803876772264021) * 10 ^ 70 + 325306879745232772730752701222403325032678354563406648052130416038857
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_263 :
Polynomial.coeff recurrence4Scalar1First 263 = -((((1116051260313818281287010172 * 10 ^ 70 + 1321666051470509084267207858166190536781665642777194287043602981711421) * 10 ^ 70 + 2217134216464280323440763384300615112403981062902170128958420782015951) * 10 ^ 70 + 9716533063439641420804877411233904228446836126837623035811524084473224) * 10 ^ 70 + 4981284421228409312679477265867132337254061435852482560520679309351401)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_264 :
Polynomial.coeff recurrence4Scalar1First 264 = (((508785367076976284112391351 * 10 ^ 70 + 522498017926497361194605872283607516225199879239242129909484759238739) * 10 ^ 70 + 6435106659538113774574387001872376745240128466095939960642671924095838) * 10 ^ 70 + 6946118142138282397107692320177799934446353085852591855021431562166211) * 10 ^ 70 + 1810747237316173687920805250598397596591609492504913077197256182661742
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_265 :
Polynomial.coeff recurrence4Scalar1First 265 = -((((6861269135811372516704554 * 10 ^ 70 + 2460093851466351207458580491500277895840448491634897285352323906760838) * 10 ^ 70 + 4649606840706665169120473829067079447109619535720677428379567687696964) * 10 ^ 70 + 6359617639385872952653773074561155874385291946493711844184900596700721) * 10 ^ 70 + 1366504930131594833107468651157427293965531584296643531363919996910615)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_266 :
Polynomial.coeff recurrence4Scalar1First 266 = -((((388525464351660302903990261 * 10 ^ 70 + 2497169189366654307163045637146984106963082230974403657237581350889925) * 10 ^ 70 + 6978912488577647129706400972501973968494858388334363715882286382215592) * 10 ^ 70 + 3459166125410813181163514907585886794663455134855854661060006405099115) * 10 ^ 70 + 623100963422829764039849328471122499980136914959267158164444351632347)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_267 :
Polynomial.coeff recurrence4Scalar1First 267 = (((681413869247931001188188406 * 10 ^ 70 + 3521385910883787892075827581120118775091513743017023263542622951562648) * 10 ^ 70 + 4165565011345047116005874400877362841362895305873909492701285287079464) * 10 ^ 70 + 3271432776383167448689186506400481407795217839452571716602304412303045) * 10 ^ 70 + 2078481826141255216675496543498747511523898535254292372669525433343308
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_268 :
Polynomial.coeff recurrence4Scalar1First 268 = -((((880089285052762548498327406 * 10 ^ 70 + 5721323614091892001281992147643172727798819399168580278035501383667835) * 10 ^ 70 + 9864342839500333502008373059929473127197585810957782332185484232731636) * 10 ^ 70 + 4131034948696264485089696314625383710285125688253039702536528458915573) * 10 ^ 70 + 5023673371600256305427454200324528627558703842998847533285724900751712)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_269 :
Polynomial.coeff recurrence4Scalar1First 269 = (((995934756608911539483043049 * 10 ^ 70 + 5858482938331764255387603132783522577290691853635115775080133591306409) * 10 ^ 70 + 4410588499505340649680711990381677884187791615913541669975557497128028) * 10 ^ 70 + 4982135973805402770407307598450494230182751857254587258125067996468433) * 10 ^ 70 + 2363622813476907059342829188128117041471273713652806489395718930335724
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_270 :
Polynomial.coeff recurrence4Scalar1First 270 = -((((1042240162360504421780972068 * 10 ^ 70 + 4541451590952513904973965625953227833265341102924306926557253511006179) * 10 ^ 70 + 5428095075878298335186081594262482109736990073933163457876071509104122) * 10 ^ 70 + 5280834749791265423791943399056715885412375223803589345043504850097948) * 10 ^ 70 + 6004196551389863749748965568752459468509308622412983085349813796586671)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_271 :
Polynomial.coeff recurrence4Scalar1First 271 = (((1033073603604794416389596141 * 10 ^ 70 + 980825120380900098589374623552970925469247543765916820908070686166738) * 10 ^ 70 + 6970081308065116996463295183807506644210319348467145558858039648011467) * 10 ^ 70 + 5190535910153258783467314975440447449824997609343672137153010788851222) * 10 ^ 70 + 5742396259333567899804107192635880247497194966111241775206959707962352
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_272 :
Polynomial.coeff recurrence4Scalar1First 272 = -((((982297180969953776431624819 * 10 ^ 70 + 5885092371724930893237041170947570976590878752869232406348405078681659) * 10 ^ 70 + 4647142271396631719815127004340508814399689002379944105817344369952261) * 10 ^ 70 + 1681933497381968897358241911269461347708663851175247329823074442977123) * 10 ^ 70 + 7139897246099462076840986971919446280029226740937256977468066142981623)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_273 :
Polynomial.coeff recurrence4Scalar1First 273 = (((902781936598908279310753157 * 10 ^ 70 + 6366846590567034883836654640278319558980109553970442194495956245745604) * 10 ^ 70 + 2994397692244323014858181795680249573462369497782819160987877808200677) * 10 ^ 70 + 5076895580867355536843592883168752929036206092845797138093180550172379) * 10 ^ 70 + 1833793841634354429726628186949349461320610938064605145889461028628726
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_274 :
Polynomial.coeff recurrence4Scalar1First 274 = -((((805848422614463248574335973 * 10 ^ 70 + 9098727309270454025739444570206183315035697704862074131766830031770000) * 10 ^ 70 + 2698143570630561853552250559386046825486710032274261464534327048326468) * 10 ^ 70 + 2336691997806779550584719776095026196518280732635360851834897195711686) * 10 ^ 70 + 7530148133879736258015849543051585267407322941671197323245300150538104)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_275 :
Polynomial.coeff recurrence4Scalar1First 275 = (((700933484978532282639874755 * 10 ^ 70 + 4324013435352635519736678363069555052231715036081776231389266108456064) * 10 ^ 70 + 7411032428321760154459165026123794015149919672547326819908966946520989) * 10 ^ 70 + 569700635280188990122329391579163975971443636360072558782423184391716) * 10 ^ 70 + 1551259300607571968915062523643883473931324849018646406693447675737037
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_276 :
Polynomial.coeff recurrence4Scalar1First 276 = -((((595462921268886877113191998 * 10 ^ 70 + 3195134819992343225067954493462113747361521647251759284326898964541446) * 10 ^ 70 + 268843609785316846547161191956116629243311547033492668361821080335843) * 10 ^ 70 + 8859259591636305190877063299969288930264370472369729295790506679226056) * 10 ^ 70 + 5627360283352185768262474875111895249238426026077322549522834469416872)