Recurrence 2 lookup certificate: Scalar1Shift 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.recurrence2Scalar1Shift_coeff_302 :
Polynomial.coeff recurrence2Scalar1Shift 302 = (11768614193698311528134403182438696648358821370790966 * 10 ^ 70 + 4770417993940612768324519981365764337527632920939574380700894415198094) * 10 ^ 70 + 6106765592307693956030765044488659624065805667657992066274386234585626
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_303 :
Polynomial.coeff recurrence2Scalar1Shift 303 = (465107340803703962570563186731469919100574370406288 * 10 ^ 70 + 2805079594533635465507429060330563706477462558424602603436048115114193) * 10 ^ 70 + 6344323988483337900545811990086698458323777873783562830369135983768533
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_304 :
Polynomial.coeff recurrence2Scalar1Shift 304 = -((668042274050664535972283290080237798786147296656085 * 10 ^ 70 + 5747514629319695963330959843330630666092025102960386594543959600756446) * 10 ^ 70 + 1525709074749550721670437304598977122325687262542087434409054231354008)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_305 :
Polynomial.coeff recurrence2Scalar1Shift 305 = (229485106711896216183207230144105176496357581387539 * 10 ^ 70 + 1713264333560305676488027034235463898650141253482771221258244268882433) * 10 ^ 70 + 7763367800475283362755847009203923826554690129789069672081546376463812
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_306 :
Polynomial.coeff recurrence2Scalar1Shift 306 = -((57831479255666939235005363757725957567855487078439 * 10 ^ 70 + 2253738984155829449509733300577851303607790742297620581205692427551402) * 10 ^ 70 + 9957260764275471689303067790060909130189504914786708838890368610288565)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_307 :
Polynomial.coeff recurrence2Scalar1Shift 307 = (12186347333044047729412995292842714970865600445245 * 10 ^ 70 + 9490268038839200078288661343960865541509757291236841389776114320501032) * 10 ^ 70 + 7039871288385634902408644249949946070512386144314412815855707232465487
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_308 :
Polynomial.coeff recurrence2Scalar1Shift 308 = -((2231013517870218208436648741647452838816585225910 * 10 ^ 70 + 9693553401855903926995899555681157624773765208192601553816860316308801) * 10 ^ 70 + 3071916941543320843894425994327188385912127043354919460002713991808227)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_309 :
Polynomial.coeff recurrence2Scalar1Shift 309 = (357875636814139279111330973776649441186752110910 * 10 ^ 70 + 3636048190404150051902073441047475668533926645954519623137957404841847) * 10 ^ 70 + 5139699151394950019287615750819412905619226035780215506900743732754594
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_310 :
Polynomial.coeff recurrence2Scalar1Shift 310 = -((49708368549198023253243552112830073223183831162 * 10 ^ 70 + 3551646349111922686402490372547626837156462731793072749629810889039100) * 10 ^ 70 + 3588218813418715662511716037019667926488466722705003809306621005875646)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_311 :
Polynomial.coeff recurrence2Scalar1Shift 311 = (5719958320353379572832362104056911457819354838 * 10 ^ 70 + 4170865509269368021097514658327691885472177826510492976469460849199957) * 10 ^ 70 + 7732074637414897178819147535692099993599521975255988157742928911003889
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_312 :
Polynomial.coeff recurrence2Scalar1Shift 312 = -((467954262427806790775108091483839505744843276 * 10 ^ 70 + 3351182241226921170997561062270667730126265309335730083668499039967528) * 10 ^ 70 + 1540010383055051807720765087094718648846744198223739454606978364590683)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_313 :
Polynomial.coeff recurrence2Scalar1Shift 313 = (3693387992360813562468793253713422383847100 * 10 ^ 70 + 4521323087889814335394713440466227636635130635133380292762054584920183) * 10 ^ 70 + 2879089806502897534865617704442804819568882812679751863520847331085467
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_314 :
Polynomial.coeff recurrence2Scalar1Shift 314 = (8623399172883070306665617037414461484170725 * 10 ^ 70 + 3129780912644575180342862174242501127043710344714122948051323673622796) * 10 ^ 70 + 7486675361560932254887022068716983398123946702530766289775558445956070
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_315 :
Polynomial.coeff recurrence2Scalar1Shift 315 = -((2296511777754335313980700361492590470566869 * 10 ^ 70 + 4916696286587129413519275637971607454087150835614796147308408220964156) * 10 ^ 70 + 5138520141784576847983709003572974872373928835461813804752165056717550)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_316 :
Polynomial.coeff recurrence2Scalar1Shift 316 = (417484896367157600536149970914955346791181 * 10 ^ 70 + 5380350995584689758395284819927467122111806047640406658522759763259156) * 10 ^ 70 + 6312790417505149927176933567052948787880578461040821112519873162762848
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_317 :
Polynomial.coeff recurrence2Scalar1Shift 317 = -((61790203652997031733362963593319708936715 * 10 ^ 70 + 7993563452780448004024636930913552891978010111078595211139029794082893) * 10 ^ 70 + 2365796985286768374694028628104342605024753083626785155084292175976270)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_318 :
Polynomial.coeff recurrence2Scalar1Shift 318 = (7746139565487694409938008089488164996520 * 10 ^ 70 + 9732553142790287899644664038217209223962512259654522921611730702202785) * 10 ^ 70 + 1699019923358098310954982860790090213000551823730050050840526964632703
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_319 :
Polynomial.coeff recurrence2Scalar1Shift 319 = -((815378370273035771260446925960952896613 * 10 ^ 70 + 3151649160160215437204987729895423662315872889805709387805732376842980) * 10 ^ 70 + 3285592021720524836294243417290243678879255955273567731526153245642184)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_320 :
Polynomial.coeff recurrence2Scalar1Shift 320 = (67443192159925559473018396579858869656 * 10 ^ 70 + 9810031142701004266396408077090874414326583585329014136550025228773937) * 10 ^ 70 + 7600625895470180462893483761029284293678519130383704283675846279284098
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_321 :
Polynomial.coeff recurrence2Scalar1Shift 321 = -((3270316914798826100324063961242514315 * 10 ^ 70 + 3173373569650814152721186581118148536423199172343026983122596174686367) * 10 ^ 70 + 9085222449157167965460270125835755791221241027046800971115200935543909)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_322 :
Polynomial.coeff recurrence2Scalar1Shift 322 = -((176637564910902261462747712165350681 * 10 ^ 70 + 4855004513400743469843763011357015152232273780875110906941846799665894) * 10 ^ 70 + 4600883418067725492740117822072652627620170679811055344635767350628498)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_323 :
Polynomial.coeff recurrence2Scalar1Shift 323 = (70192419085263582624498532813299296 * 10 ^ 70 + 528892017648337205903534069317617194026104757504218875843172054515437) * 10 ^ 70 + 445056065765345912660845778357863651986318790253273043123696338487011
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_324 :
Polynomial.coeff recurrence2Scalar1Shift 324 = -((10668373544098375899839625656439698 * 10 ^ 70 + 3748578686582470020943038909080209360642546689468407585036620560098500) * 10 ^ 70 + 3791681502553438878559826421605416307911448776914140447122160382825099)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_325 :
Polynomial.coeff recurrence2Scalar1Shift 325 = (1124099440754796484211895843248484 * 10 ^ 70 + 3145186923045093450162397495592325732149798060046500916171498726540627) * 10 ^ 70 + 7183036627962256754544872362612981890058105267918308992307286637901659
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_326 :
Polynomial.coeff recurrence2Scalar1Shift 326 = -((84807941045910271828643130188580 * 10 ^ 70 + 6997442848196178181194613000994634333625124719026651588895714691748090) * 10 ^ 70 + 8654366146087414680142429314820698877044804079178897266465875325459574)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_327 :
Polynomial.coeff recurrence2Scalar1Shift 327 = (3652235426064342630889491040344 * 10 ^ 70 + 6254768468980151458278721301710405161803118140889917651202415076262731) * 10 ^ 70 + 9114670958428618101421933453764961453656089057681590712536241284525992
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_328 :
Polynomial.coeff recurrence2Scalar1Shift 328 = (107245001096026958790168525312 * 10 ^ 70 + 4033352335774025712832240464065391861125830842629161429604675751143094) * 10 ^ 70 + 5546390617823753811840913670370310144861620372282709974051991357035249
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_329 :
Polynomial.coeff recurrence2Scalar1Shift 329 = -((38340820613786692340555054653 * 10 ^ 70 + 1822740587308531354607225122318769030726035419902126112772787125702947) * 10 ^ 70 + 4335885006247583375290560301992945360731280949166144750939430727661747)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_330 :
Polynomial.coeff recurrence2Scalar1Shift 330 = (4077576829086977074039337868 * 10 ^ 70 + 5940482206411529704506613902918031342858757107208225460955932481717767) * 10 ^ 70 + 1907824327997637541973312154413123860976466765111962960125676469878513
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_331 :
Polynomial.coeff recurrence2Scalar1Shift 331 = -((261715132600132464168060674 * 10 ^ 70 + 4151548966727466985025715864836136592878315845281721893913216372027634) * 10 ^ 70 + 4798334553046371915007964221379997093851842435760915139148964765494961)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_332 :
Polynomial.coeff recurrence2Scalar1Shift 332 = (8285367335533400125936941 * 10 ^ 70 + 1533578037788334904835009525186835867828054175521245178543472032100657) * 10 ^ 70 + 952205097361456256133662578375177235353658164284754727234564537265021
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_333 :
Polynomial.coeff recurrence2Scalar1Shift 333 = (307374615118008732208087 * 10 ^ 70 + 4372991205223182088101881331844023804279528277374360078665480328573982) * 10 ^ 70 + 9300541454639394191895087756420622117603173794583348389729596987263808
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_334 :
Polynomial.coeff recurrence2Scalar1Shift 334 = -((60482698547547812167595 * 10 ^ 70 + 785284221051345267275573694944245001251911635112581898037496494698212) * 10 ^ 70 + 1557300439577039334387977420256405648145108558876361664047900375664748)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_335 :
Polynomial.coeff recurrence2Scalar1Shift 335 = (4171151555955676068130 * 10 ^ 70 + 5779484007426587195035775599101868922406275293492772392467707840452325) * 10 ^ 70 + 4616945133163877179288857908369423881873509440449584648958503633012950
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_336 :
Polynomial.coeff recurrence2Scalar1Shift 336 = -((153957333692994430399 * 10 ^ 70 + 9676745134332467131472618892428528941226844581074537043148201209740633) * 10 ^ 70 + 1446262837112486530603910948738987046412120254687224609974819723766745)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_337 :
Polynomial.coeff recurrence2Scalar1Shift 337 = (769262980239311452 * 10 ^ 70 + 6670431708365824834546522091183700736199014641367371851870390422001410) * 10 ^ 70 + 7989267505623692037406308975457754363275001526536423383595102616148194
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_338 :
Polynomial.coeff recurrence2Scalar1Shift 338 = (269048024432136180 * 10 ^ 70 + 6583082660232948139462695234429341518043758627240192882926951579102682) * 10 ^ 70 + 6985897427098523241715196548465838024978181782076635131530461820164302