Recurrence 2 lookup certificate: Scalar2Exceptional 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.recurrence2Scalar2Exceptional_coeff_231 :
Polynomial.coeff recurrence2Scalar2Exceptional 231 = (552784354652433930758462639452792623511812871254837912058370 * 10 ^ 70 + 1789168214523650790596109913650277139459295681613639260515776684931084) * 10 ^ 70 + 3714359115867824265721642690190092804828848839502112098758254243530921
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_232 :
Polynomial.coeff recurrence2Scalar2Exceptional 232 = -((255071974749057787875794846335851851419651874466262835697339 * 10 ^ 70 + 7322418350138417884622871023440651083542204507606605343529501720403794) * 10 ^ 70 + 6648671273242396458678755592305420091979628869291789574029530405548230)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_233 :
Polynomial.coeff recurrence2Scalar2Exceptional 233 = (59940769027738858741029829327669364665898562491547124762628 * 10 ^ 70 + 6286719360696723779477548473913536190590698740736608369465353405923285) * 10 ^ 70 + 5018507381080209387982072566727902357952954355999663955040238088817977
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_234 :
Polynomial.coeff recurrence2Scalar2Exceptional 234 = (48172080324132394881379974533670616445138734952397558784026 * 10 ^ 70 + 6117599427471044726582583842916128261533191190153419384961556023871495) * 10 ^ 70 + 2211978641073636338623202685872463117642035032146709860194851036617332
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_235 :
Polynomial.coeff recurrence2Scalar2Exceptional 235 = -((92547099973373691589147220279876310228016428819755009791664 * 10 ^ 70 + 504334633951260447344631162546393589212028701690030106185659475948966) * 10 ^ 70 + 4270887353662748504310267307553595939010465034654799955170718225131775)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_236 :
Polynomial.coeff recurrence2Scalar2Exceptional 236 = (96908774113428256347971902784435289689999950265247424146496 * 10 ^ 70 + 321427782045027709775820942063928518698785449295011745988622501182238) * 10 ^ 70 + 2539564458930997561238575661511274872397475338652688648018825951451105
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_237 :
Polynomial.coeff recurrence2Scalar2Exceptional 237 = -((80907885607549477579538322409993723560318539858248129636630 * 10 ^ 70 + 5490940839220451779579590192226398589110018417173146464507004938614174) * 10 ^ 70 + 4233019525090313319621208140245185390502776567569107496706646724541931)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_238 :
Polynomial.coeff recurrence2Scalar2Exceptional 238 = (58286249624251151737649928005327798784085498838206967678546 * 10 ^ 70 + 7417797439567474787251722488481164829487332571382091511028130943279552) * 10 ^ 70 + 3706183825734044346364643557862429487360795068823479628676542596807864
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_239 :
Polynomial.coeff recurrence2Scalar2Exceptional 239 = -((37033218825409129308022656800080610895206292440342427861194 * 10 ^ 70 + 2850958101098534464982900169353876178393071673967429290952972127065370) * 10 ^ 70 + 9069221730923753966802302543663500701997514566470071611263519170290882)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_240 :
Polynomial.coeff recurrence2Scalar2Exceptional 240 = (20646998479583013102913986568572637471456368004543632137957 * 10 ^ 70 + 539614276415827291702214193518255030687289336060159413726213415300445) * 10 ^ 70 + 2127215773803181242584263075047025811052961838098031147867339731317312
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_241 :
Polynomial.coeff recurrence2Scalar2Exceptional 241 = -((9726968134542566688291388911214216618424908426373285623737 * 10 ^ 70 + 5678573057359115564557339433339735247298820015487708626139011372691702) * 10 ^ 70 + 8076527228509190654233740757846208115935700230445744441942591898327446)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_242 :
Polynomial.coeff recurrence2Scalar2Exceptional 242 = (3387570508148279669288185617988517319916318410679615504453 * 10 ^ 70 + 5016111989482037404473674526602130288529855199461707312061068477623240) * 10 ^ 70 + 6530982971684188716548666138411882190793532424924629454921137370008204
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_243 :
Polynomial.coeff recurrence2Scalar2Exceptional 243 = -((262556764480850674601222247784986584053271341296069031433 * 10 ^ 70 + 998469841873870988810139550973855730277291815653994231171125491484439) * 10 ^ 70 + 1195188244312844721906749237895480959226317444552609873355567915738600)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_244 :
Polynomial.coeff recurrence2Scalar2Exceptional 244 = -((922027620892773007062752228113157266527151206126989379001 * 10 ^ 70 + 3148170515431847498963436519913744515660322094078003800601744796687372) * 10 ^ 70 + 9152918257236227496550406790157167457221889458488125317981129031292546)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_245 :
Polynomial.coeff recurrence2Scalar2Exceptional 245 = (1112592968074157590592761230785738515851455450779462013441 * 10 ^ 70 + 4845472915607052504198148559709231107577792143610084658909120522393509) * 10 ^ 70 + 2406518665870501433700418626367785042313338744671292319372239298484472
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_246 :
Polynomial.coeff recurrence2Scalar2Exceptional 246 = -((902799503093460215738974146078111345941554075770598192941 * 10 ^ 70 + 7848959102647492643791807181478381935112006358017433382001058896240689) * 10 ^ 70 + 5524381611220608644332867261862362395281652325875631558933972286625638)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_247 :
Polynomial.coeff recurrence2Scalar2Exceptional 247 = (606997675219658726159965070950330329601033833684171361552 * 10 ^ 70 + 7675008738607761191617650650005598583676214282282643105613306679027768) * 10 ^ 70 + 8909863529205191084923619096448886057869240863212256626753659797418879
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_248 :
Polynomial.coeff recurrence2Scalar2Exceptional 248 = -((357576612684157814128300308694140009640407453434346090759 * 10 ^ 70 + 530976936629382619378789939742919596444068449364789420745266063396491) * 10 ^ 70 + 3432390092914289116665262510527202773921918812936373373385326864682704)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_249 :
Polynomial.coeff recurrence2Scalar2Exceptional 249 = (187783982550808580357376402207504543778840977514584373421 * 10 ^ 70 + 9894708763685939562071537365152103281071933453689875708150984094809430) * 10 ^ 70 + 7820759296837218847044361012654909173122182436872422559354490398324921
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_250 :
Polynomial.coeff recurrence2Scalar2Exceptional 250 = -((87721344982238806803539833461890859750422554182984702850 * 10 ^ 70 + 7746206731899960961074694584223010443311304970793332907581038040265472) * 10 ^ 70 + 1115722054498075961335952137079858018841071929932166521366385246794812)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_251 :
Polynomial.coeff recurrence2Scalar2Exceptional 251 = (35600899156879374306013508614270004087594279384467994486 * 10 ^ 70 + 7269720649327267285921399582255963980677909539159274078932123605806294) * 10 ^ 70 + 7499390398777044625980906396141665445040816313845538914882060896672790
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_252 :
Polynomial.coeff recurrence2Scalar2Exceptional 252 = -((11667389910389588388164698094005833221663086848228247934 * 10 ^ 70 + 8562947312505831661366248750523889351334288210211840707498870059554753) * 10 ^ 70 + 8820899631329482020480150409871354037141058934823222833488025855085655)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_253 :
Polynomial.coeff recurrence2Scalar2Exceptional 253 = (2251419739677074361652430267098069213496429062976793303 * 10 ^ 70 + 9374012384112140906884223471147661643654397597324323748629207936948319) * 10 ^ 70 + 6418760064277338433650776551319047103514888280876641027685488667121888
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_254 :
Polynomial.coeff recurrence2Scalar2Exceptional 254 = (637475222517754442734037680351242887594194060832424385 * 10 ^ 70 + 9275159463864750228894929294710736767480626009796937017527269468467076) * 10 ^ 70 + 1985089715160115113747153008630862788894987655443971212159176885860101
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_255 :
Polynomial.coeff recurrence2Scalar2Exceptional 255 = -((1053748487683121107516166222506554858600843189999809375 * 10 ^ 70 + 363781281327575927015391725147888070285807459602377650299734247942431) * 10 ^ 70 + 9328658895072812841788236513990196913834846379169199234135307356624864)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Exceptional_coeff_256 :
Polynomial.coeff recurrence2Scalar2Exceptional 256 = (773694993611066968160092571536070611860599244168379038 * 10 ^ 70 + 6179619812359607619011289519771242040105021955994858418656414955668518) * 10 ^ 70 + 3723720434043746312845423996974010670322938555291039053321087423440600