Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1SecondPart3.Coefficients458To484

Recurrence 4 lookup certificate: Scalar1Second 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.recurrence4Scalar1Second_coeff_458 :

Polynomial.coeff recurrence4Scalar1Second 458 = ((4581517873298164113874 * 10 ^ 70 + 3654619866315196054315305167362879655163774313039767525678574000162866) * 10 ^ 70 + 7793732534481366174787485374143383206965391804975088236270616528446765) * 10 ^ 70 + 9565188165698255832392843002126324297025103457869220362445811069767734

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_459 :

Polynomial.coeff recurrence4Scalar1Second 459 = -(((432545713237268264038 * 10 ^ 70 + 8846847383545043158314531717237670604040683283187253076760867334503966) * 10 ^ 70 + 7759074360307310239302396066988505246950798521853110995787266795126920) * 10 ^ 70 + 9615757288492762735224653406365133445664728087775286139862216666053780)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_460 :

Polynomial.coeff recurrence4Scalar1Second 460 = ((22443323120204317865 * 10 ^ 70 + 3410013717827997558040240449012850502408665595925033691079906513684455) * 10 ^ 70 + 9879769897596063960971265068941528870495051051033936329265196706051764) * 10 ^ 70 + 5863874211423848697719182350082369667480227280376537632349668590464934

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_461 :

Polynomial.coeff recurrence4Scalar1Second 461 = ((1441682357280730711 * 10 ^ 70 + 7688935328864764646372857677043268790646886320081746303706829069519092) * 10 ^ 70 + 5816161145829036261988579491668766092995711439859503463447578285203052) * 10 ^ 70 + 1580809211267604623742053321043055142517248016412371198442522584422255

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_462 :

Polynomial.coeff recurrence4Scalar1Second 462 = -(((567366559815404638 * 10 ^ 70 + 3261158906198887007625323168279180881978545160286549861873064038554336) * 10 ^ 70 + 8049939538697724238016677278199678556985975507013169691689038757453629) * 10 ^ 70 + 4771197055534286551354133645942513283037355945709723437668507480616942)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_463 :

Polynomial.coeff recurrence4Scalar1Second 463 = ((89179515549669399 * 10 ^ 70 + 7471784165632587326571919730928104607072599481613929598540289102395417) * 10 ^ 70 + 5942249338509635669001259192721322721278112145171820906418575639484553) * 10 ^ 70 + 3931590795946166258741877072175368917592270907646814717031078362560172

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_464 :

Polynomial.coeff recurrence4Scalar1Second 464 = -(((9907765037948716 * 10 ^ 70 + 528331407780142528559935351341604566726421023888569266638041836039070) * 10 ^ 70 + 6161227906461529936786617607001145986491832256710782263917737369692219) * 10 ^ 70 + 1400946975851710891801267059874373967190164737504083867793826527482905)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_465 :

Polynomial.coeff recurrence4Scalar1Second 465 = ((834084604090698 * 10 ^ 70 + 4757120470080650318328627491419764688272087199017530241065670679710034) * 10 ^ 70 + 5800528569266408155580402076027335265561428326700697449699062808096724) * 10 ^ 70 + 9655272990557246582812968166791290138733346581062508579414353615605788

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_466 :

Polynomial.coeff recurrence4Scalar1Second 466 = -(((50577622808750 * 10 ^ 70 + 8289160975793817982762427796455460714827102124705169139209567338548238) * 10 ^ 70 + 1910367270746024379175830177549909578263732080692448314418240426318694) * 10 ^ 70 + 2915005629145143496218221166227528812547068356611210199051499147385423)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_467 :

Polynomial.coeff recurrence4Scalar1Second 467 = ((1544924451846 * 10 ^ 70 + 760937211628028985112324312099525638728627377387159413466915222569805) * 10 ^ 70 + 5721224172453197980800945255747555198182358634755437228896430504041336) * 10 ^ 70 + 8721462947220158694961971591651759696296982263263126932028319830509718

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_468 :

Polynomial.coeff recurrence4Scalar1Second 468 = ((91019881947 * 10 ^ 70 + 7958435466353293113454652865396365160656867327501740681984914246977184) * 10 ^ 70 + 7245939958660163815258265318294981439440865712330621993441941767775796) * 10 ^ 70 + 8974825150961522288963795549524251788212015110402846082993047946576950

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_469 :

Polynomial.coeff recurrence4Scalar1Second 469 = -(((18343279733 * 10 ^ 70 + 8746310490134331309021774639725432994067528057697815354321558827791967) * 10 ^ 70 + 911514547680088673779882532148798455654741735932245737813387346592695) * 10 ^ 70 + 1465464435858418106382321023353567487619838472030834427374078397022875)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_470 :

Polynomial.coeff recurrence4Scalar1Second 470 = ((1585475709 * 10 ^ 70 + 7645206472878005895511997967913024982324003528615983030743807059241751) * 10 ^ 70 + 7260196797527650494185715626368187276243934355755832372218279003223610) * 10 ^ 70 + 9997363018593189682439833267690145781072010975318815468367461822952505

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_471 :

Polynomial.coeff recurrence4Scalar1Second 471 = -(((88426205 * 10 ^ 70 + 4968395513310987935922468989234602434515188314208698862354687581812259) * 10 ^ 70 + 2997593137551502713008340347608044106642980438683787606818514929118399) * 10 ^ 70 + 3614398183005879834738514946863348574140808180259418404003158390067578)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_472 :

Polynomial.coeff recurrence4Scalar1Second 472 = ((2949587 * 10 ^ 70 + 2984655671956189616080283372341283159972745116942579896765990049284942) * 10 ^ 70 + 2394425976300166117202826951547767595278237595301183029194983760600329) * 10 ^ 70 + 1856101929255838676224826293681861678253799064553991939772454120177080

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_473 :

Polynomial.coeff recurrence4Scalar1Second 473 = -(((8480 * 10 ^ 70 + 4062256670430238107098051059099171466903496733416305706613481137990626) * 10 ^ 70 + 1588336253993018278164959393985064325341257677613975849739983794460146) * 10 ^ 70 + 6085154919660733345219046821530688881279347556210853002551342126947590)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_474 :

Polynomial.coeff recurrence4Scalar1Second 474 = -(((5383 * 10 ^ 70 + 5507487619176533618821196324957796522047594029694554317496660138912428) * 10 ^ 70 + 2119363272602500518536250337703561326989474854462064712212840323482748) * 10 ^ 70 + 2642594222784148618331405653534334067477561070534166863525150186252902)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_475 :

Polynomial.coeff recurrence4Scalar1Second 475 = ((324 * 10 ^ 70 + 6189776805208155305956146002345574056460404811393284207769810334298913) * 10 ^ 70 + 306619364623560185365244456249008507454500100917087119709892187581885) * 10 ^ 70 + 7053321562663506432088148135834741247317110982927380942025990315967698

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_476 :

Polynomial.coeff recurrence4Scalar1Second 476 = -(((8 * 10 ^ 70 + 7989105693678167274757480431326829754256556362813718342227019117872850) * 10 ^ 70 + 3350077518165092530489711854410633375920371215862553015877263021699183) * 10 ^ 70 + 1911758053260743213431722195960731353029175831623332895880489907383616)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_477 :

Polynomial.coeff recurrence4Scalar1Second 477 = (196466627747958759453827042799814559471602787184527290150702577242808 * 10 ^ 70 + 435886928946116580823412936563408396900906050478620190649060463634711) * 10 ^ 70 + 4224652764726604138745262623916300687753525086652514619849067592594823

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_478 :

Polynomial.coeff recurrence4Scalar1Second 478 = (64040068575171941540421377164470683039991094327871264648431700590749 * 10 ^ 70 + 6828526587496148958938928345668830455038361092006658459664011538270048) * 10 ^ 70 + 3019141021246222130850136006522531923018735588102414122947628212621733

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_479 :

Polynomial.coeff recurrence4Scalar1Second 479 = -((1693585157580120967959775794019236823882557577610219235013823675059 * 10 ^ 70 + 1987761532862521165001718274672105536641002298218225500993352394649733) * 10 ^ 70 + 4010124984722708573917236082626030441872620983450668829900021919065097)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_480 :

Polynomial.coeff recurrence4Scalar1Second 480 = (428476796876125402629712499761083863137262312457274023074506165 * 10 ^ 70 + 5821861131635910850149819542949354326263362240117688414786375518010477) * 10 ^ 70 + 324400998211935663345885798760241452897384428430418236613182853900282

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_481 :

Polynomial.coeff recurrence4Scalar1Second 481 = (571620929562550029966431625721047329796733360869817049113254062 * 10 ^ 70 + 6366549521343627158179798987345895001937364733753782231369976149994968) * 10 ^ 70 + 5891765091670282535978187420286377623916784896195974935214465791173872

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_482 :

Polynomial.coeff recurrence4Scalar1Second 482 = -((3737142562596350340282869761772721630562141053681895513326655 * 10 ^ 70 + 1990628007641376920732567489993912548162034724799772267010230400454695) * 10 ^ 70 + 3221948328984620313037461278607904447002614288350536323513535891927386)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_483 :

Polynomial.coeff recurrence4Scalar1Second 483 = -((91310160464374603435474983446296302341011409367853177217294 * 10 ^ 70 + 7593641876362595139483609991298344515917770323429099078824620213580538) * 10 ^ 70 + 4280273193814692449245729147072212814023759519922465361581510025906391)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_484 :

Polynomial.coeff recurrence4Scalar1Second 484 = (503607785877125461216791671980561889662996031852569481867 * 10 ^ 70 + 7811584684576150408454181957290438767188406229998696564912333482524741) * 10 ^ 70 + 7769049816666811792696168116900941160111916767247598012619684706889308