Recurrence 4 lookup certificate: B3A4 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.recurrence4B3A4_coeff_307 : Polynomial.coeff recurrence4B3A4 307 = (2426150 * 10 ^ 70 + 6302112143286515028942816882357035215921028103043677995314360221264289) * 10 ^ 70 + 4403362117991416744051079447002960450902893725893499772632914231074887

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_308 : Polynomial.coeff recurrence4B3A4 308 = -((161409 * 10 ^ 70 + 8666487565620689879171321454274732084034074835266381079252136032380649) * 10 ^ 70 + 4564792210850415379122028729963216568416126001159972443684324762616856)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_309 : Polynomial.coeff recurrence4B3A4 309 = (5805 * 10 ^ 70 + 9890530821062925985161891203397126946492056162150549582492245655971898) * 10 ^ 70 + 7200619788445216502007167131823593314053877979516157877351092446639808

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_310 : Polynomial.coeff recurrence4B3A4 310 = (49 * 10 ^ 70 + 6973347303390780696737018907444647324074857031671227363739939148022225) * 10 ^ 70 + 5437141191897960068900028626671746039277281446479730371499316659006157

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_311 : Polynomial.coeff recurrence4B3A4 311 = -((19 * 10 ^ 70 + 881074132447707955981692828734785654434466147240669288697312333122562) * 10 ^ 70 + 8067076638587157565882662795815097271599741887814045511668872320517353)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_312 : Polynomial.coeff recurrence4B3A4 312 = (1 * 10 ^ 70 + 100082882441755146073581235670500227462990175396389360075222900911401) * 10 ^ 70 + 8907061893286144718448214223432177738708339004266821077007422467111141

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_313 : Polynomial.coeff recurrence4B3A4 313 = -(151180559054390631935768272158739620829297957561744860174430844020064 * 10 ^ 70 + 694487704844839130235695270160464652678412335688242537158463776706674)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_314 : Polynomial.coeff recurrence4B3A4 314 = -(7629277740819337564623533282902789238343906276038338762000163755286 * 10 ^ 70 + 5453845105643900191776991276675536713531895755344796334986467761267122)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_315 : Polynomial.coeff recurrence4B3A4 315 = 329738798763536250116249985873351911115034226430064093281965802098 * 10 ^ 70 + 9687018519657757032110114857589159710626658050181156762553306072974975

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_316 : Polynomial.coeff recurrence4B3A4 316 = 706627098538555179323563847416251733192052216569140121193241091 * 10 ^ 70 + 5246839822640564717642988521740600983355052355183501666580839185841863

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_317 : Polynomial.coeff recurrence4B3A4 317 = -(166411573156517844664884976114985206234480818880420283008594635 * 10 ^ 70 + 3688044856837901086397231251217552506585855865094007782962420857269292)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_318 : Polynomial.coeff recurrence4B3A4 318 = -(697234139504619110568223943311327535980760783486300703666081 * 10 ^ 70 + 8743338623122932711902926926851482215410429868594286539402752593890429)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_319 : Polynomial.coeff recurrence4B3A4 319 = 25348154732708195135096719468081189457721950349007423912743 * 10 ^ 70 + 2220947253791680026456346793800503744595546391475109792504925051770870

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_320 : Polynomial.coeff recurrence4B3A4 320 = 239205521392227763092018275537064152769979578384911544989 * 10 ^ 70 + 1198213118851018124909578862508830729741876925736607909805979452884634

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_321 : Polynomial.coeff recurrence4B3A4 321 = -(2324099666444241757148387128176363760905753234367882 * 10 ^ 70 + 2102940585628268676622366011059510069511751526792742163237353781937826)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_322 : Polynomial.coeff recurrence4B3A4 322 = -(7377186380597392882336396305965986785207103985965293 * 10 ^ 70 + 2168297745347805090010917857591144024684560300882285795940915723909780)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_323 : Polynomial.coeff recurrence4B3A4 323 = -(23157349412720647199961812249699212666555361226805 * 10 ^ 70 + 7582707831071136158879688216642700111195294053886606796125772338949148)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_324 : Polynomial.coeff recurrence4B3A4 324 = 37215880863582041008400949859368698140755343983 * 10 ^ 70 + 5081198725246236253843920819360166543438367259256059854516856372395516

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_325 : Polynomial.coeff recurrence4B3A4 325 = 240457175124432748223982525243957413606356836 * 10 ^ 70 + 2085706051900174120621716121735160927691861644725847409965817492074968

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_326 : Polynomial.coeff recurrence4B3A4 326 = 26233067116942477577060757573858847124160 * 10 ^ 70 + 8371478537121960162561097271400731091578713136279133608852314322851779

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_327 : Polynomial.coeff recurrence4B3A4 327 = -(910425048878492487207338451629469407381 * 10 ^ 70 + 9278994800481357450288242596257661759336509942568622253604514362609863)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_328 : Polynomial.coeff recurrence4B3A4 328 = -(428355539847926311572658624395038248 * 10 ^ 70 + 361083897205547582034902650387982302479720663516850258198644457878043)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_329 : Polynomial.coeff recurrence4B3A4 329 = 1342527882549121917151999130204344 * 10 ^ 70 + 5878083444395964082269965986408980615886633678590049724652198955484427

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_330 : Polynomial.coeff recurrence4B3A4 330 = 600607385899269656305003742482 * 10 ^ 70 + 3373205723775023733237817417675921298755014442203298006804841135273279

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_331 : Polynomial.coeff recurrence4B3A4 331 = -(433046799005802435781488911 * 10 ^ 70 + 9004577671544857594964810268490189745337640304069759533087791243955209)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_332 : Polynomial.coeff recurrence4B3A4 332 = -(118688360847302617950182 * 10 ^ 70 + 2377836523527105353798187862201597897932247198952480195533069026983398)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_333 : Polynomial.coeff recurrence4B3A4 333 = 15083837867884666381 * 10 ^ 70 + 8355544097756873469628750295126057073679552296990065450414149968432239

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_334 : Polynomial.coeff recurrence4B3A4 334 = 1937018098315750 * 10 ^ 70 + 6912004504424788689234805386985231853146692642409340501069117308364897

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_335 : Polynomial.coeff recurrence4B3A4 335 = -(37234255610 * 10 ^ 70 + 7214639938930088712137988031203787055631346063421151059647160868476309)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_336 : Polynomial.coeff recurrence4B3A4 336 = -(1769622 * 10 ^ 70 + 443168808919257720113164189418356213691776949453438172088986284742262)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_337 : Polynomial.coeff recurrence4B3A4 337 = 4 * 10 ^ 70 + 340688137721530789091017979358661860009364964993702298318398011262667

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_338 : Polynomial.coeff recurrence4B3A4 338 = 504017678327847682915086885677927800554808002053473611490763774507

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_339 : Polynomial.coeff recurrence4B3A4 339 = -100762257592350468113657032443957682948882773522607516144985

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_340 : Polynomial.coeff recurrence4B3A4 340 = -164307136086778267567799254222819600906248373976475560

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_341 : Polynomial.coeff recurrence4B3A4 341 = 2235913438855190091535226669145218491828049229

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_342 : Polynomial.coeff recurrence4B3A4 342 = 68130461165797460872098471860624747870