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_485 : Polynomial.coeff recurrence4Scalar1First 485 = (1972339663927866737605700270737996706289734166773571040 * 10 ^ 70 + 7441237727456753488584435153992849406395933449089465995541091694425369) * 10 ^ 70 + 8191272826085369452760292328545116035530504668279621566579650235412799

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_486 : Polynomial.coeff recurrence4Scalar1First 486 = (6116730521157699241962726464081025395313241970716344 * 10 ^ 70 + 1380963709523931386407910904855836950945172172175496761804897806021562) * 10 ^ 70 + 1039838676398830753397615803318320605232601997062904127441000195653097

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_487 : Polynomial.coeff recurrence4Scalar1First 487 = -((74648090932077347353263753864833245709248293104249 * 10 ^ 70 + 6576722286580108023576817125411503525848590422123583849366601609915960) * 10 ^ 70 + 8384450081969754806502709479764596001436371663463968914365435306373618)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_488 : Polynomial.coeff recurrence4Scalar1First 488 = -((339186021775847190861139694017958971968887438604 * 10 ^ 70 + 6139956025663920525971554393110091145678015254756696528326141524395508) * 10 ^ 70 + 1015276928984203431723370644458172977932351107427333238642909499029449)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_489 : Polynomial.coeff recurrence4Scalar1First 489 = (1232530091055216136077249860747126090406097399 * 10 ^ 70 + 3059518758004075414674490120195176815526103905813540399414028159374438) * 10 ^ 70 + 8343796897954486759119787895257680868756527970904822041451633848520742

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_490 : Polynomial.coeff recurrence4Scalar1First 490 = (7526124239358483796856268347382848283365740 * 10 ^ 70 + 8054345538169604571634557221321238005660153360147357220966666696118537) * 10 ^ 70 + 7126156916716859073453133213501095328376111803953648037514277455286518

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_491 : Polynomial.coeff recurrence4Scalar1First 491 = -((9312190052053424212586533715395067321455 * 10 ^ 70 + 7995809174577019192275481238950303169296101861530076184249339365101968) * 10 ^ 70 + 7793388981916622203304667223701557712195187170546309034223255199648127)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_492 : Polynomial.coeff recurrence4Scalar1First 492 = -((81536586444739608178053319965601833224 * 10 ^ 70 + 3363586451380916348146503841139944016616395126512275041466259170764934) * 10 ^ 70 + 1828485571491685981343824807054481375254622381431793403942827219627406)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_493 : Polynomial.coeff recurrence4Scalar1First 493 = (42467609532802624975544424386539137 * 10 ^ 70 + 6101704001284299665339319760306209932844299739375997660039582470903992) * 10 ^ 70 + 3438253238152746194610539939453653348668719302981521561659335562193818

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_494 : Polynomial.coeff recurrence4Scalar1First 494 = (490810692449436746794488338981596 * 10 ^ 70 + 2492477523389816807277515003689744430725304468636020534881247752764615) * 10 ^ 70 + 2322174316644426123543975176112026210624582287561861273962149196770062

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_495 : Polynomial.coeff recurrence4Scalar1First 495 = -((210097027913814188838807220613 * 10 ^ 70 + 840473736124601249973586663604480651128551179649532635407127042023259) * 10 ^ 70 + 9739748607811914372380651790389901051880282629597113635641916003459856)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_496 : Polynomial.coeff recurrence4Scalar1First 496 = -((1642172443042872222668543852 * 10 ^ 70 + 9037417640025370136667214888040987054407916365344370239264547941478712) * 10 ^ 70 + 5928044549193440995381480775627326645990648327491370346907184824326443)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_497 : Polynomial.coeff recurrence4Scalar1First 497 = (1008497370059499659711662 * 10 ^ 70 + 3676708471849466564292967881348637453070266263160376135612080697500600) * 10 ^ 70 + 2658840564901637275524884732067381204845850078614750164734704123594228

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_498 : Polynomial.coeff recurrence4Scalar1First 498 = (2544942759587124200259 * 10 ^ 70 + 2346188935835411478316915752449305401831361591637033140320656322287736) * 10 ^ 70 + 9841788622251137119611954794919155212095118397128158994391423535073337

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_499 : Polynomial.coeff recurrence4Scalar1First 499 = -((2226143944909891390 * 10 ^ 70 + 9835121376077371204266789095475373946368531243131046493017575471397725) * 10 ^ 70 + 5156155595573248780810428045991922936496191733714313063662357838195479)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_500 : Polynomial.coeff recurrence4Scalar1First 500 = -((945097891307393 * 10 ^ 70 + 4682845961491778028504175512787514419124240180440771506096860628266110) * 10 ^ 70 + 1492392031003527309671190307246878191022875214254828547286751702904123)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_501 : Polynomial.coeff recurrence4Scalar1First 501 = (1180937056767 * 10 ^ 70 + 1673237875357378323544708086603741009779417305850960408830990918322263) * 10 ^ 70 + 8832923049849030556904813858899408362808586811767339575576884580072377

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_502 : Polynomial.coeff recurrence4Scalar1First 502 = -((115282679 * 10 ^ 70 + 3132037069055099157111363858862768609496498545148931800517812141412679) * 10 ^ 70 + 212708086825054015190823615790272034400361985005940435701368659363382)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_503 : Polynomial.coeff recurrence4Scalar1First 503 = -((95784 * 10 ^ 70 + 7051279528726760760701577470682221342369726174083271247623349401785487) * 10 ^ 70 + 2373935467374019213757725834598087182271605729535360340421467025169037)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_504 : Polynomial.coeff recurrence4Scalar1First 504 = (17 * 10 ^ 70 + 1432416920070436566929847924499860641182379648291476220965161296186630) * 10 ^ 70 + 494804242371929568006463141020811377612354686409038889734322041482735

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_505 : Polynomial.coeff recurrence4Scalar1First 505 = 3210542217947617211629707595273107072249483294653354853480542839735 * 10 ^ 70 + 9469660170781244095820924612961028802431063684617787521823127394230495

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_506 : Polynomial.coeff recurrence4Scalar1First 506 = -(1590329813036954421921444186742491627397130701811589226779313682 * 10 ^ 70 + 5923245748844080217507673083911685369154251669696572418678451075909769)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_507 : Polynomial.coeff recurrence4Scalar1First 507 = 44917810696009707609319006854678105930269483758512676000761 * 10 ^ 70 + 7357273229078575866667622182882415175585991549867038059019172437909960

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_508 : Polynomial.coeff recurrence4Scalar1First 508 = 780703593417263659911223146443448232981528409591408128 * 10 ^ 70 + 9857614745312238910434906780923508811921870089215904497962479278599674

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_509 : Polynomial.coeff recurrence4Scalar1First 509 = -(29150508356483022930565045869325200584398564614598 * 10 ^ 70 + 960616034432173973688958591864501792297153353224219935340974091172560)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_510 : Polynomial.coeff recurrence4Scalar1First 510 = 103017743661360131232578851696511847305370894 * 10 ^ 70 + 6797074169192186865706376482645903159289366802910811244660784014754088

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_511 : Polynomial.coeff recurrence4Scalar1First 511 = 605206929389022692376173192279101523284 * 10 ^ 70 + 3768782281772964258988716477801130602553785652613462389782044679436313

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_512 : Polynomial.coeff recurrence4Scalar1First 512 = -(2387564210795561767331640168739011 * 10 ^ 70 + 1055656557510652155564391597591862663130937896343765201276236665781971)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_513 : Polynomial.coeff recurrence4Scalar1First 513 = 722923329923565252946204848 * 10 ^ 70 + 1485352938550773357973813673894293528915621928611917809580688545632809

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_514 : Polynomial.coeff recurrence4Scalar1First 514 = 639227295447097744006 * 10 ^ 70 + 6949833568875890757490842621048178695602214816757076895539676784710869