Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0ExceptionalPart2.Coefficients316To337

Recurrence 4 lookup certificate: Scalar0Exceptional 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.recurrence4Scalar0Exceptional_coeff_316 :

Polynomial.coeff recurrence4Scalar0Exceptional 316 = -((((433798762159304600392 * 10 ^ 70 + 6334117714533754095217201373668906817883667724575682837153797415677543) * 10 ^ 70 + 7002446622518497798508101734931855614940267596741813518311435506690398) * 10 ^ 70 + 9718016451817325384477542225643392659081150652920074988209626104346345) * 10 ^ 70 + 8509007644537884981997898873007617006656332446420352495054741521361670)

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

Polynomial.coeff recurrence4Scalar0Exceptional 317 = (((247479365378230777082 * 10 ^ 70 + 5716845709151042841258035236159516062492495130992717754151242892159991) * 10 ^ 70 + 6438211546712112580424143684054558887438359208558048495546884088488342) * 10 ^ 70 + 7160413876712967090520240728038416258806203527538410776359940540458222) * 10 ^ 70 + 198137535896796519211237915266055971441763397104261681263889491180313

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

Polynomial.coeff recurrence4Scalar0Exceptional 318 = -((((138367236378942399711 * 10 ^ 70 + 5413028764315513735809721560373393575710827961841081568785366752729044) * 10 ^ 70 + 5859345202514130253651530841335607238662954646869397541135059186204257) * 10 ^ 70 + 3763856318392355865599474965522966086290812679852830712871601788968524) * 10 ^ 70 + 9904527933533992578144882611992708835346298324986479224247504997697546)

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

Polynomial.coeff recurrence4Scalar0Exceptional 319 = (((75859701209721452128 * 10 ^ 70 + 5056875306796813346330393412254355912395538461840227776886005916612305) * 10 ^ 70 + 6723330793614420427370955646073220811185228387188956505954822046018732) * 10 ^ 70 + 9042060702423386081459558778149794591940057996139937620392867560631148) * 10 ^ 70 + 8903090972697861114311406236750000235991172520319964171501247879682871

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

Polynomial.coeff recurrence4Scalar0Exceptional 320 = -((((40795703835268182371 * 10 ^ 70 + 9340050663842514900216869896451374220593773910460123592493248939029349) * 10 ^ 70 + 1768757043379541189934668524887464200225177665676079550475163533305749) * 10 ^ 70 + 2220647506071337529219889183870866423459490125878838358044408156107034) * 10 ^ 70 + 3928419483278416694907531931892975427103502105525435480967582533995679)

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

Polynomial.coeff recurrence4Scalar0Exceptional 321 = (((21523004518034986587 * 10 ^ 70 + 816515951963817663971541920932631729998286720442982259520007328266620) * 10 ^ 70 + 5278505392280527059958454148436566404448477939858847271995414380032502) * 10 ^ 70 + 340144836106027516896673362433851534733155923582780347258637373661468) * 10 ^ 70 + 6168147798591171891403514275538852087830564302195826547684495197660222

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

Polynomial.coeff recurrence4Scalar0Exceptional 322 = -((((11139423911414300696 * 10 ^ 70 + 9621544772117557417292490905641613263491233534828515969339106524189413) * 10 ^ 70 + 5593250976300245666683261060836850445991777537027983848418952903124631) * 10 ^ 70 + 8742760527474138603174561124211940298718319277607258519839201367486389) * 10 ^ 70 + 6281335290483645863829463137137097321052759537528885450678678946395340)

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

Polynomial.coeff recurrence4Scalar0Exceptional 323 = (((5654694391357435660 * 10 ^ 70 + 8773633169352598211005214714907362302027667255344030469324045720307635) * 10 ^ 70 + 5558076324469519285212147324384560035753352540356163513199176760183087) * 10 ^ 70 + 4700213128262358637299984576262974166076824448966813685236734517897964) * 10 ^ 70 + 6128145745949405818016650497423071815242134458772974522031146354263827

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

Polynomial.coeff recurrence4Scalar0Exceptional 324 = -((((2814381640588080974 * 10 ^ 70 + 7508424940708198204278880202529125952407112514166612896980209861218139) * 10 ^ 70 + 8966657972470791772268776405909924283082637257223139175088147928506047) * 10 ^ 70 + 3484509368692888280529630998748393359462888954036521378803067440249390) * 10 ^ 70 + 3236969978747674416878651967291032468096750524208479232608030089120349)

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

Polynomial.coeff recurrence4Scalar0Exceptional 325 = (((1372590114349415669 * 10 ^ 70 + 2274646982246345503274104232743202774454445415007391522092820321762561) * 10 ^ 70 + 6995354449644518413449359342890640042800617012271809907204269923794032) * 10 ^ 70 + 8508993555177914890762516620821623616402513875829731748103550672943372) * 10 ^ 70 + 4107944407174452053997406249824204896032150456854363099636291658007394

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

Polynomial.coeff recurrence4Scalar0Exceptional 326 = -((((655445351414752069 * 10 ^ 70 + 5672922730148791930310467246373327015446876851422650610411630315892057) * 10 ^ 70 + 5027851490151461902373822123104257910086575457064000618927785257514873) * 10 ^ 70 + 1918751140323947668314218850709033033148656372080937120689348221463130) * 10 ^ 70 + 8608040101154428592361798206211395417502734275106900786767634471680187)

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

Polynomial.coeff recurrence4Scalar0Exceptional 327 = (((306118518928448420 * 10 ^ 70 + 7669049524745767512251514961438112495126139127043873347390523096674350) * 10 ^ 70 + 6781833642894190998255608663110781451622168920308891930192668682955752) * 10 ^ 70 + 8672575096537917365813262434234146772606791803038547656713982073756192) * 10 ^ 70 + 4610753287838445793736733169212715698624586054827018578617666752594839

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

Polynomial.coeff recurrence4Scalar0Exceptional 328 = -((((139616004840130988 * 10 ^ 70 + 6899159918836410668321909354167421127617917124194604619769164299053548) * 10 ^ 70 + 3375172726549048901439050749854316953463654920849484741175804337020754) * 10 ^ 70 + 9750790826812212056891385032668641789546797941363497435644883135842734) * 10 ^ 70 + 265949395052726950127887764007101375939812435111586989584188961205419)

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

Polynomial.coeff recurrence4Scalar0Exceptional 329 = (((62049687364935925 * 10 ^ 70 + 4776149408739934292272680188197904372384990273717947533689046647521109) * 10 ^ 70 + 5849905514121633450536643723792326103338024131829687429827348530198857) * 10 ^ 70 + 9015873084503795679907379127900344405358405370944997239139017456011790) * 10 ^ 70 + 8462946991396148838747947063725318486663571945830951402958203990753372

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

Polynomial.coeff recurrence4Scalar0Exceptional 330 = -((((26789028181771436 * 10 ^ 70 + 6404714850550137876200570340381723502796260827360462785703115953712504) * 10 ^ 70 + 7682884625042279324708980892013106539273482904536658321775087249946517) * 10 ^ 70 + 9817632691897397562886029470307569922508379261450867293660195381631391) * 10 ^ 70 + 2057935782784202286441831463375669931226333787444616156704646357735945)

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

Polynomial.coeff recurrence4Scalar0Exceptional 331 = (((11183328842133886 * 10 ^ 70 + 497559387675523257713612481325721247777424411175705136737057957718934) * 10 ^ 70 + 8473732115815166353196877876240469913797444201835329780815434320281999) * 10 ^ 70 + 1120629822829861085476020224916491285612485005983623231455866437861682) * 10 ^ 70 + 5212545007052664719563491413565663916360243477526749276773215053884490

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

Polynomial.coeff recurrence4Scalar0Exceptional 332 = -((((4481208055887998 * 10 ^ 70 + 3422665763500063039710090497520494668632175253324832012873203067300752) * 10 ^ 70 + 3641370478079110163660599982599964554619560012961270283915260376213692) * 10 ^ 70 + 5368983233251122553073931575796686924793966320722281248167524767212191) * 10 ^ 70 + 5826758415640317159569194669937419367449309196237157865095391413210330)

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

Polynomial.coeff recurrence4Scalar0Exceptional 333 = (((1702152577690804 * 10 ^ 70 + 6008478144677673983813564173674915267336848005972894210237341425112841) * 10 ^ 70 + 4424005345437590844275034777140858794758383241950963136153630448846265) * 10 ^ 70 + 2860402851662091170104844549920483505486932406451360773514391205446603) * 10 ^ 70 + 4252058582105882498769864585554583345873398501681514335765163660196489

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

Polynomial.coeff recurrence4Scalar0Exceptional 334 = -((((598471945740846 * 10 ^ 70 + 6828290377808724493052214007325316966381502286723137925282469075015843) * 10 ^ 70 + 5944040599194870712787574458376448035568426258821369570294671382268291) * 10 ^ 70 + 1314298665596159573422579063149759737730905512077350675486552721002548) * 10 ^ 70 + 962391176085916400029797832089622794767156166250123344546573429361011)

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

Polynomial.coeff recurrence4Scalar0Exceptional 335 = (((184489772772104 * 10 ^ 70 + 4094341626857258493826212250103821641855934863689556618878855666167176) * 10 ^ 70 + 4341514844573594573271738420327474184538010117143139988105133084179627) * 10 ^ 70 + 3009947488311972576590752408576529459784794283218698304488352912388893) * 10 ^ 70 + 9077625317809910743982297970318730339532315799712633638932070903937859

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

Polynomial.coeff recurrence4Scalar0Exceptional 336 = -((((41789034947383 * 10 ^ 70 + 9599878693586031651513224888097066562798590242424653144469799380748786) * 10 ^ 70 + 8797460117203554603697627096393177163940713877781493668104535009634105) * 10 ^ 70 + 548381341593462613921166057641437781089256288774770876051746528285173) * 10 ^ 70 + 808133122168603469928204298196944614625462237141071729340294437198722)

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

Polynomial.coeff recurrence4Scalar0Exceptional 337 = -((((548535417451 * 10 ^ 70 + 2897356711471464891227807940955339420138447841279210149909070729054924) * 10 ^ 70 + 4365246232401716766167251984413452841364868122321499623709912428767316) * 10 ^ 70 + 7205100960412726588329446054009155002187870784025551549839220501267902) * 10 ^ 70 + 1608509018893827637724650837710310814609549326969894958299823881536092)