Recurrence 4 lookup certificate: Scalar2Exceptional 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.recurrence4Scalar2Exceptional_coeff_372 : Polynomial.coeff recurrence4Scalar2Exceptional 372 = -(((151262134404461584991576736302996011491460542890059538120846883612916 * 10 ^ 70 + 5078697638414433652558579338787584018302151305146966462429324615364966) * 10 ^ 70 + 363633096529021941892408049509544759738055216627738262425462717217078) * 10 ^ 70 + 8185968279442471402251386954140854752968416242789466624177950882104448)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_373 : Polynomial.coeff recurrence4Scalar2Exceptional 373 = ((58434432547249241623092728275209397534392921308070658943863957417467 * 10 ^ 70 + 3242817485553346319074155675196550753008207785456143746652600577916634) * 10 ^ 70 + 7017602304016085037545953213466475769413872289918346212738936939140716) * 10 ^ 70 + 6276096467351364258826939222857968002377183231662140144137745294353370

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_374 : Polynomial.coeff recurrence4Scalar2Exceptional 374 = -(((22039717858705707427176884549795596661283928964018409351714259768766 * 10 ^ 70 + 3498924232821707264827223958414075700045079223719394806479703277147031) * 10 ^ 70 + 2376667282025422197001527394033348643679182435762430252838701040640852) * 10 ^ 70 + 7992479144708038355290623517244620544429488610197045112799714144970397)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_375 : Polynomial.coeff recurrence4Scalar2Exceptional 375 = ((8106666028232103212518394403928549911375739068947058527237206759835 * 10 ^ 70 + 5920602406382787146551229848437289047358069366869452088747715880957024) * 10 ^ 70 + 3687607796444744542465616039226674125577423794103931145700452913590843) * 10 ^ 70 + 4332577045933332724711203779231905010228967558357356513005095640746701

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_376 : Polynomial.coeff recurrence4Scalar2Exceptional 376 = -(((2900889101857711105010822409102347570679690588852817252791166686555 * 10 ^ 70 + 1708594594281549279320573217835048110346001755110156506999249599623107) * 10 ^ 70 + 7015762789456828393250798750780177358774636105923778459005476473462493) * 10 ^ 70 + 8770041601353131772903479745208280773560439952862187773468379758204065)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_377 : Polynomial.coeff recurrence4Scalar2Exceptional 377 = ((1005469742690826664974217669741811543799042674949465046532113529338 * 10 ^ 70 + 963643432563404649002344266512526707606883697272701847692887086541819) * 10 ^ 70 + 2804652023147160917594659004338141768678407460277340179665865182415624) * 10 ^ 70 + 6808422853339248457965546145922382096888086380690475170145043073980602

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_378 : Polynomial.coeff recurrence4Scalar2Exceptional 378 = -(((334951692869969801281181548656706023584790451871344407299508842740 * 10 ^ 70 + 5698971291905886495060512819950614664684644656932023463822583180403422) * 10 ^ 70 + 3763033490562227452034538231419573492891374409396991414217896219624522) * 10 ^ 70 + 6146360131799402556248043506695521172400952768670398624544355829697737)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_379 : Polynomial.coeff recurrence4Scalar2Exceptional 379 = ((105727348760877209411410393268191567034445437187338095509249621141 * 10 ^ 70 + 5807061483171012976585529114118309555041499722917262596962449414972411) * 10 ^ 70 + 2546252388612484337361774931328473207649808775986913176135136614257446) * 10 ^ 70 + 8375048771268398874513402462338765184338439184948828222302636661517599

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_380 : Polynomial.coeff recurrence4Scalar2Exceptional 380 = -(((30728392952763784681131675382877104352247251749271458922012464259 * 10 ^ 70 + 8737419517175853714640260869232991610828655160657772103424459287596259) * 10 ^ 70 + 5972708330482204627087493713949661879464225332858953855393006183728825) * 10 ^ 70 + 6716364322267409982172502619089466421790715882056257712434251132220448)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_381 : Polynomial.coeff recurrence4Scalar2Exceptional 381 = ((7668596523963274574653699431088823851958165747656330513440200273 * 10 ^ 70 + 9233786777761262258648001652689715849210152813760682182405309351085481) * 10 ^ 70 + 5031945297477290838639558981387498376528408650452876656836147319244369) * 10 ^ 70 + 3780253525073232167478201653591260762920069997313504695727760572514475

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_382 : Polynomial.coeff recurrence4Scalar2Exceptional 382 = -(((1260600002092625920006964453827012001502225450139047013342353463 * 10 ^ 70 + 9007832894464244587500649526248527730799966281392117783540864151882270) * 10 ^ 70 + 1544694486803736373712438920067646882212251630025153348837544903191735) * 10 ^ 70 + 6101791909789693970879555875363402702099430109701406201366718094656641)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_383 : Polynomial.coeff recurrence4Scalar2Exceptional 383 = -(((185151365003776616612885805392194123835336961276400145760970161 * 10 ^ 70 + 1760763357812621469072802002146881539091368880038942296946017539266220) * 10 ^ 70 + 3188385831594384132587780825363957145156000834250063917261735251120720) * 10 ^ 70 + 3887198078758932415397955672612471778144757775880745552490301776013710)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_384 : Polynomial.coeff recurrence4Scalar2Exceptional 384 = ((329878406346372431310445236154932530498356709330438040446380161 * 10 ^ 70 + 9897404052487676087967110798268610788353040997988629186448006880600961) * 10 ^ 70 + 4384350872308674860227641796059834192445186484011854852452153895463380) * 10 ^ 70 + 1026788778897882120086254097404849221517212542923367821749405177108173

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_385 : Polynomial.coeff recurrence4Scalar2Exceptional 385 = -(((223689989204169894001618848807108788454183751541959971716590006 * 10 ^ 70 + 6167815415687774239642531242264697706875641712107904655354441297586134) * 10 ^ 70 + 732910997575551536046459313920947227331301779103880231440682002112274) * 10 ^ 70 + 2774904209732425840593017574132743283296902023077439138099903564159794)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_386 : Polynomial.coeff recurrence4Scalar2Exceptional 386 = ((120945726165492879076974869951154946065908951330436713615522972 * 10 ^ 70 + 9306911665924692615634919783992864874678087124954928835144262518093467) * 10 ^ 70 + 2296036548890886744945783088715475152018216731147322573707221870268510) * 10 ^ 70 + 5939443740050360568679045158478385596918947079252419465574261773694082

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_387 : Polynomial.coeff recurrence4Scalar2Exceptional 387 = -(((58528901039448786064170755383764590778372701486740537438717298 * 10 ^ 70 + 1024540127449233322989910033293935932906965218189468673081448724815298) * 10 ^ 70 + 8642216424045447644247812828442319415045545630008621046049761942151570) * 10 ^ 70 + 3431896881493008777205857905859686636082554256998360337065025270828622)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_388 : Polynomial.coeff recurrence4Scalar2Exceptional 388 = ((26390654936468430994296895420936147266072111035239551875472329 * 10 ^ 70 + 4755315418581980524709884425815154413778124183921305893139321127116611) * 10 ^ 70 + 92854037424452660172419142809804305250607087738407587645945939042507) * 10 ^ 70 + 2652727296446983743258962298872827004609164768665175355330706011787001

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_389 : Polynomial.coeff recurrence4Scalar2Exceptional 389 = -(((11290994987320653649236542420161149305942559773375900052486489 * 10 ^ 70 + 6905239850341490274290742709741052857108877684536698307737004382122897) * 10 ^ 70 + 1367855918876046852967745512648460382708359728363549612910565471142949) * 10 ^ 70 + 7617408432812232464731956245781395602309816346470044955962031387318626)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_390 : Polynomial.coeff recurrence4Scalar2Exceptional 390 = ((4626536040348961521587719103780547094387692469526614552851620 * 10 ^ 70 + 2543954502874210932776965929718147944993268077331704307597265446229215) * 10 ^ 70 + 3578481385465154325590587631681265112522134159312400838203756416429186) * 10 ^ 70 + 2599784855778047031622707860091440243572092039178448721763199160635592

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_391 : Polynomial.coeff recurrence4Scalar2Exceptional 391 = -(((1824603463841755346485198434060193207280858270314310748977158 * 10 ^ 70 + 8079553071644463506033340389213793811626151038763659532187247203355842) * 10 ^ 70 + 1572761179529835479273849723640068959580271938089883980334141875002160) * 10 ^ 70 + 2417226256913277063349571712213155364350862084315995287908408629918958)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_392 : Polynomial.coeff recurrence4Scalar2Exceptional 392 = ((694292167122956718061301904217055315198574368711840062427488 * 10 ^ 70 + 8149708776794052967656450329654195666132383832773931398020183561511020) * 10 ^ 70 + 2757404056547679153594115382412674217833036868799731771326898917311004) * 10 ^ 70 + 3713469836443824582592092442556815416760584518750973571911976156848869

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_393 : Polynomial.coeff recurrence4Scalar2Exceptional 393 = -(((255120325396263556826934106980579673547429970643049792431961 * 10 ^ 70 + 6129980529662507346092582977840172107532568266592554713104877999697825) * 10 ^ 70 + 7924157291561493711233629224672175051008133225079153612231354891407993) * 10 ^ 70 + 3561613341328073587850098898754493984473001386273390284637236031102797)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_394 : Polynomial.coeff recurrence4Scalar2Exceptional 394 = ((90489998240858756556432903432836921708472819654434006699180 * 10 ^ 70 + 1379860997398132311312670711771663015722092343009790345820762819815734) * 10 ^ 70 + 4745208845871442799298512337019619461344475871056956572274343771106501) * 10 ^ 70 + 9783684260017199699899278535957505284416200863118564861930013035201142

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_395 : Polynomial.coeff recurrence4Scalar2Exceptional 395 = -(((30933240522008862683531207946674196003664079357387233520321 * 10 ^ 70 + 4505976345214820219211749710449874972530412717096861046622809132852966) * 10 ^ 70 + 167026823395163877960325222288146216699844073489744086074796889155685) * 10 ^ 70 + 6013018271397966354007922959264788714260085245147901580445540460640877)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_396 : Polynomial.coeff recurrence4Scalar2Exceptional 396 = ((10161612921583645892224147471715761593143577591982166864294 * 10 ^ 70 + 3176837985575292450456348320483762258713256075542244730979022919143511) * 10 ^ 70 + 1114385376853671753264999496834468095699945624613753667345852022823770) * 10 ^ 70 + 6961967420149216284451915282720516189286797569671011239875085523319838