Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar1ExceptionalPart1.Coefficients285To313

Recurrence 2 lookup certificate: Scalar1Exceptional 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.recurrence2Scalar1Exceptional_coeff_285 :

Polynomial.coeff recurrence2Scalar1Exceptional 285 = (264381696217789808725462257865561024161718771 * 10 ^ 70 + 6990558774924532232046420345344100648961610766519524681683937179378210) * 10 ^ 70 + 7627963298958559808149563674984451640812900304511528882080527008987124

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

Polynomial.coeff recurrence2Scalar1Exceptional 286 = -((68891738754539153175440797933048759593985667 * 10 ^ 70 + 7942424326188458868569911528376969141695737805485320022548747031693192) * 10 ^ 70 + 2011624054184195250738502835289065577626451792429109787806205154005169)

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

Polynomial.coeff recurrence2Scalar1Exceptional 287 = (3994606795530035877976419491298121002467647 * 10 ^ 70 + 180387094519094072760341941642081278493362037338413447653653722552478) * 10 ^ 70 + 3563365169072904353729024295019505052052370558348200288664274911066654

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

Polynomial.coeff recurrence2Scalar1Exceptional 288 = (8366370115124385521414567530414624374794334 * 10 ^ 70 + 164483034275546004645482126920573625196278103153541016199206339783790) * 10 ^ 70 + 5183220299150361281257285220515150334366459371317483672117193390315498

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

Polynomial.coeff recurrence2Scalar1Exceptional 289 = -((6174842452186898289576171005465350334138352 * 10 ^ 70 + 8553026604692359164556564441298856334070610207996520908644707929546329) * 10 ^ 70 + 6295572592859576648884655564696372427243186223005549798529727998058171)

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

Polynomial.coeff recurrence2Scalar1Exceptional 290 = (2754504325976807125597760010495151671547722 * 10 ^ 70 + 1938208191090459997166670267568289763729407588431206577282540517498224) * 10 ^ 70 + 4556808732765363664976675104288347712618482366532114967982043109210777

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

Polynomial.coeff recurrence2Scalar1Exceptional 291 = -((859541206400782755832743699998611377563490 * 10 ^ 70 + 3886016859893953968273448580493631512267121529604112308254599278974558) * 10 ^ 70 + 4355668073382284063894758916292149993750356451378514448002615702180258)

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

Polynomial.coeff recurrence2Scalar1Exceptional 292 = (154466756816596563819233395879523487529675 * 10 ^ 70 + 1158879580923077197585929355740331207807899483245642323851124675519342) * 10 ^ 70 + 6887875092695467137914654967394336046740787849734839552083904926654024

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

Polynomial.coeff recurrence2Scalar1Exceptional 293 = (18161391615661832015249023781292103350869 * 10 ^ 70 + 2085163857461930101434736392568715175125991377496310591448766471279576) * 10 ^ 70 + 745404934841110412197469382868991529066558350355174919621994108767465

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

Polynomial.coeff recurrence2Scalar1Exceptional 294 = -((28959878502880858292874247816359799531683 * 10 ^ 70 + 8609601331699810975026519046968663473328806568016580587793957909341252) * 10 ^ 70 + 1091382912339805883484075780301095928445189810181058131744144125079112)

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

Polynomial.coeff recurrence2Scalar1Exceptional 295 = (13871601630974152103489570788171439652145 * 10 ^ 70 + 1037266334681077277402943021350362346196281466529687556396716776693177) * 10 ^ 70 + 478108382003141128072534580139324064388771824911030875279714190070756

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

Polynomial.coeff recurrence2Scalar1Exceptional 296 = -((4234880325668558390033248014144605559491 * 10 ^ 70 + 2224941587717922109938839297747442796563094851543039436617197044999597) * 10 ^ 70 + 5300917777170299059241003061563696751825671127184119064627115448089315)

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

Polynomial.coeff recurrence2Scalar1Exceptional 297 = (743352595236625407263001437640267113663 * 10 ^ 70 + 3388416637614922975550197980927249887630541070114172641642493667662697) * 10 ^ 70 + 9483780018911810237924101364303519058769796408990229439845614757583091

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

Polynomial.coeff recurrence2Scalar1Exceptional 298 = (48051460689405947099412894577533237509 * 10 ^ 70 + 8205796122424546909252974610382740165019023721656816956419863037332737) * 10 ^ 70 + 8797206449753812932337330648442258434095450549985499828366440708639497

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

Polynomial.coeff recurrence2Scalar1Exceptional 299 = -((93278510016636752061220170822643211732 * 10 ^ 70 + 6311251110036688585343856827687439911819030905909380642045557897659354) * 10 ^ 70 + 8164061270107603076835653240418028926162584473964641424575969778581080)

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

Polynomial.coeff recurrence2Scalar1Exceptional 300 = (39253161189637614086217806276988123266 * 10 ^ 70 + 408270699502067987729963203792851667983918249449073908030182827169138) * 10 ^ 70 + 6475227315898479205668382728842898465124665011913303806150442696506090

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

Polynomial.coeff recurrence2Scalar1Exceptional 301 = -((9753005405841125352304567359634688319 * 10 ^ 70 + 1647867036681559659506509496568216556485402914607545966207790974358910) * 10 ^ 70 + 3213069352378136657569625911270120321249106757494072670610605094281147)

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

Polynomial.coeff recurrence2Scalar1Exceptional 302 = (1064288595106627699166068375022215358 * 10 ^ 70 + 6292272129373870465404162960458370456097380350814763866125977071557441) * 10 ^ 70 + 5237004787444526087233990391223794994888906298680916383288355372202020

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

Polynomial.coeff recurrence2Scalar1Exceptional 303 = (304792375595836714136147445143908030 * 10 ^ 70 + 7140308040245043818221786044951556285104639662255512439557973654618440) * 10 ^ 70 + 2347321040876942675307010405402629352858152954111753758121783942119916

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

Polynomial.coeff recurrence2Scalar1Exceptional 304 = -((201501287588238129681052254173567365 * 10 ^ 70 + 4110962006257435872661740761991486186165956114359740131703918974590354) * 10 ^ 70 + 6925186147708071711628388407209538245265271867250429432401808414319789)

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

Polynomial.coeff recurrence2Scalar1Exceptional 305 = (57434839704781723234920165317805279 * 10 ^ 70 + 1293194246502091230133552013422970197105859917234256522435578836444592) * 10 ^ 70 + 7378186341397400389171480473319263491925834075472592441861296144098637

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

Polynomial.coeff recurrence2Scalar1Exceptional 306 = -((8250946857127590080018261229264595 * 10 ^ 70 + 1831673862454414770958450289497648040447478180141457976159714139930311) * 10 ^ 70 + 132633663371721540865316275492020946554773912791214159442363362650079)

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

Polynomial.coeff recurrence2Scalar1Exceptional 307 = -((629142439359668862723439553544759 * 10 ^ 70 + 8988343593011121275087357445974586468925125698473646923073816516278911) * 10 ^ 70 + 8696843841354671447427757913285668203406073835106259744137986326599808)

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

Polynomial.coeff recurrence2Scalar1Exceptional 308 = (712564262206706573897266075607150 * 10 ^ 70 + 8120944177274601909030877178601022799677861667916585143555992205068420) * 10 ^ 70 + 3400840350992598983823643991829758774005841413915360796908406959078810

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

Polynomial.coeff recurrence2Scalar1Exceptional 309 = -((202722884530526532366382129678198 * 10 ^ 70 + 277545034132458955026700402407405690866733755594353313384870143623874) * 10 ^ 70 + 237229387139698829064796000088137709574040313509979494472828506813314)

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

Polynomial.coeff recurrence2Scalar1Exceptional 310 = (26725448256019702070527679504444 * 10 ^ 70 + 7389604617183682767869869713078871670564177938355695149067639850484506) * 10 ^ 70 + 5698965260492380364317577850590948221082759913179848311048044351587650

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

Polynomial.coeff recurrence2Scalar1Exceptional 311 = (2131547907481481704761403154427 * 10 ^ 70 + 2701861064046013521667012069895944721199799017187566763641160169743352) * 10 ^ 70 + 9537871875642346318280091725243825070804638934609584486956286047516472

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

Polynomial.coeff recurrence2Scalar1Exceptional 312 = -((1926457916866307726732692172339 * 10 ^ 70 + 2288736884838084419559336710990591523441056730761361019832911199463607) * 10 ^ 70 + 8156322122109581297247354269209323937116021512824223605954413600911525)

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

Polynomial.coeff recurrence2Scalar1Exceptional 313 = (446989394028780227505629565380 * 10 ^ 70 + 8705558357201707348175460655551534295977494164809442157675237026282722) * 10 ^ 70 + 3075896781313641679314126077871898630822400573102489767626258783928840