Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar3ShiftPart1.Coefficients266To299

Recurrence 2 lookup certificate: Scalar3Shift 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.recurrence2Scalar3Shift_coeff_266 :

Polynomial.coeff recurrence2Scalar3Shift 266 = (3505339372462333578743221398221915899774424955446695345439438557086 * 10 ^ 70 + 2287663813650478725402951423861817997043824860279743838332104528763404) * 10 ^ 70 + 5679483295191567061231971977190123921293338090340136680661869927984690

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

Polynomial.coeff recurrence2Scalar3Shift 267 = -((1459307117436888036509478271413065576551376368744125075919786811573 * 10 ^ 70 + 4395618544489239181168992970576831314204425148608551049605502101029152) * 10 ^ 70 + 494828631779175338841997842405734564157485423831954069903827913093713)

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

Polynomial.coeff recurrence2Scalar3Shift 268 = (552278004072104579299780511196293996171784831573133653741505037019 * 10 ^ 70 + 3598099215781005482575296436946440396405118059855638111209470009519846) * 10 ^ 70 + 4147573774758095289666147567088848726442994366088063396329799529225833

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

Polynomial.coeff recurrence2Scalar3Shift 269 = -((181911175864383803302729650273254782614436619085328080891076105096 * 10 ^ 70 + 7623734409547428715777611045497416115188898120742001197788565528092578) * 10 ^ 70 + 766560530445795008967822842947865347110520314091042842343967000920616)

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

Polynomial.coeff recurrence2Scalar3Shift 270 = (45951459109897340177647976607415507818507900395587883792675508796 * 10 ^ 70 + 6785701832824707155544563554939960795264944378831022397284767722501003) * 10 ^ 70 + 9492505406020085200875389935734792252210688483856966505272718645132741

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

Polynomial.coeff recurrence2Scalar3Shift 271 = -((3571716050517223792554121611708622160500147256256463743996850952 * 10 ^ 70 + 1403206535394374819810343690832428724055574571365277343424189358389992) * 10 ^ 70 + 5145139347165870014698690809184991870070171852566894608767034467345773)

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

Polynomial.coeff recurrence2Scalar3Shift 272 = -((5682390380080016414472184816352086704264959799184902040064058883 * 10 ^ 70 + 6667068557797608531478121240506362543346123293144283832961517015284496) * 10 ^ 70 + 5195840324207505265218743362862355683772263261502536692591867808904000)

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

Polynomial.coeff recurrence2Scalar3Shift 273 = (5314765944633047436276232672208491324595086473252079073806908415 * 10 ^ 70 + 6457174436198877830364711807688005219631848778244125845756006275459896) * 10 ^ 70 + 3547679795220191474044540409259267050286289985965643714535459709135183

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

Polynomial.coeff recurrence2Scalar3Shift 274 = -((3286269797971797284075338352197413124651400150830953344827152255 * 10 ^ 70 + 916855522386920265344755756298209792235336671949598520153349238860702) * 10 ^ 70 + 5557861410060228194888428892173417226927020420266838099965022813515897)

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

Polynomial.coeff recurrence2Scalar3Shift 275 = (1701250794730564997813335618317532239125456617194593585222156627 * 10 ^ 70 + 9088591896896761483248261770242822702438489973698015528278629981939336) * 10 ^ 70 + 1475875027904445745774125746489919587107063082414275737699641999634251

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

Polynomial.coeff recurrence2Scalar3Shift 276 = -((785948971418392467623657474688541718714566376632100602381789848 * 10 ^ 70 + 4697739746850757865744518398069215514943070255260839554680947675111889) * 10 ^ 70 + 7801016909133435472136306717847236738279539961091096169775785365604030)

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

Polynomial.coeff recurrence2Scalar3Shift 277 = (332362068553419959843977611969051368413570631507887589539989541 * 10 ^ 70 + 357658568534158485734900139240713639608737918527348497497328800783580) * 10 ^ 70 + 9228361842837895021706928914151796417442461440305438761867261398872485

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

Polynomial.coeff recurrence2Scalar3Shift 278 = -((130106301592050450384948583059391378881279737951844802144025673 * 10 ^ 70 + 5443955950927806915584792348599357127321655219300180558277830379052347) * 10 ^ 70 + 9473379346596196004843908736295354169809085129298421124666094229123336)

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

Polynomial.coeff recurrence2Scalar3Shift 279 = (47339231231202666032397754823226129881442078246978221347725075 * 10 ^ 70 + 2183153221539783582875034896099702807520056063050258485569183810906837) * 10 ^ 70 + 8671684137827171227382065909155409295764225802006008913928922580722423

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

Polynomial.coeff recurrence2Scalar3Shift 280 = -((15994220256212456773328539073117412736245596157154215171517368 * 10 ^ 70 + 2205822019136035250975778329307653938666297385317721655618523072214412) * 10 ^ 70 + 2752499433131088199592297160023184014034919853118307051010485138504533)

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

Polynomial.coeff recurrence2Scalar3Shift 281 = (4987166493356664970667303446753175801078031062559467757192338 * 10 ^ 70 + 132873122940358483311227030812780494702541012431181524771007654068027) * 10 ^ 70 + 1729701178143529518741055446358570629403249961815437471634693581448900

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

Polynomial.coeff recurrence2Scalar3Shift 282 = -((1415248148793833299453068269705187339345692650544806288154514 * 10 ^ 70 + 4464407172151439605311566843709119753161391310732572828736039468526006) * 10 ^ 70 + 3946482369676806145031793771886383423904068044218418353502631624453959)

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

Polynomial.coeff recurrence2Scalar3Shift 283 = (354681302057736508026121144546970136965626243378440999240810 * 10 ^ 70 + 4606411271391924332248764648849310673172347144553437599754904156377794) * 10 ^ 70 + 7128162561454530920622424845121678389900666495745655129108775003053003

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

Polynomial.coeff recurrence2Scalar3Shift 284 = -((72745021253562085893749787969797045986961463263783722854071 * 10 ^ 70 + 305112533820771228216651526137974518204426011811876159842442459971457) * 10 ^ 70 + 4809751066758116394849014201205669099140115916067624269545425569009591)

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

Polynomial.coeff recurrence2Scalar3Shift 285 = (8958758865263356365487773097672553304214935250300494963735 * 10 ^ 70 + 2840161669889361932056650854522540411805588247031801893269073942799933) * 10 ^ 70 + 3939280268449561528953876643790573414886903237036536023726073115451001

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

Polynomial.coeff recurrence2Scalar3Shift 286 = (1506809491816607468863047584109784426716470349979090405007 * 10 ^ 70 + 7662780260454374378083552551727774257050480769874773627148908337088030) * 10 ^ 70 + 3658390286326817172190474268973191057822286472233763888177129498855557

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

Polynomial.coeff recurrence2Scalar3Shift 287 = -((1635017140476793296061844032144318022650388001551253163087 * 10 ^ 70 + 8009602327962869745470455632321633853551040429401652116999927885874346) * 10 ^ 70 + 4691930746062299648398664626239395048477944499371635110023254737776441)

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

Polynomial.coeff recurrence2Scalar3Shift 288 = (772933188309064531665444687581252069394429553878111741048 * 10 ^ 70 + 8516300612447828041903069595720435399419397571017328178935746324244020) * 10 ^ 70 + 9179525360208139738618468436508472612163252495578718563929102063667013

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

Polynomial.coeff recurrence2Scalar3Shift 289 = -((284068338514117184363889432760921170042243547435692167864 * 10 ^ 70 + 5132111379801217408479133051489362246854400297466943334182019122273591) * 10 ^ 70 + 3124199620685667593998769645440326367641404836837629927944436407244794)

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

Polynomial.coeff recurrence2Scalar3Shift 290 = (89807497003879435256649045682054559030560995527208469612 * 10 ^ 70 + 4121548432047628396883970185085370415203586707161893805669153799657510) * 10 ^ 70 + 4560608052337100305839679506922235430787906542370014266174520311457531

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

Polynomial.coeff recurrence2Scalar3Shift 291 = -((25240018187811963325296028999183600634032227604610820628 * 10 ^ 70 + 3140749187443658515160150553087031216313704580108114204831861642926900) * 10 ^ 70 + 333644650254472282375001056074362939457574151547979336182102562422807)

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

Polynomial.coeff recurrence2Scalar3Shift 292 = (6368444382621510494352939273350881146996789417325484658 * 10 ^ 70 + 6777934224181886765128447295168681190776588479861356025072417538289433) * 10 ^ 70 + 3811126854808458966213966272536505935222921847035140022532256545438295

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

Polynomial.coeff recurrence2Scalar3Shift 293 = -((1437249165000131132368464910378248571877606191760524243 * 10 ^ 70 + 8872244906862878410727544334500160154123515392572061808526513176846736) * 10 ^ 70 + 1605229984336266042116995483019215581995604628105463290448749647166481)

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

Polynomial.coeff recurrence2Scalar3Shift 294 = (284655752157619235908334997096608047343575193839640025 * 10 ^ 70 + 4820318854605200394084749324898925990589877814888465567530614827150474) * 10 ^ 70 + 7341655504340841710032406515919965520386816320457425029278057164779748

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

Polynomial.coeff recurrence2Scalar3Shift 295 = -((47018228335198997470682102849301328700180419932147450 * 10 ^ 70 + 8493070961305980589665293066804281274522941184378687852205372635126816) * 10 ^ 70 + 9805679538134488842192602048892886832872475650075314405257511130831328)

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

Polynomial.coeff recurrence2Scalar3Shift 296 = (5472876286869920591916675397156778264701250672310253 * 10 ^ 70 + 8273045606274921927469591055266735387006994488056421540517363127986821) * 10 ^ 70 + 1313163438784190065027448868225664696899465190392435857449660499567905

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

Polynomial.coeff recurrence2Scalar3Shift 297 = -((5595510924450127957217287274425747541780246905258 * 10 ^ 70 + 6317529346834917510015717425625525012242191586038171274370653068070752) * 10 ^ 70 + 5281953007583094180852153409389826949188523044566409138939781841901560)

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

Polynomial.coeff recurrence2Scalar3Shift 298 = -((239953614802551106702405134845032913621982985325463 * 10 ^ 70 + 3376663499586926647354008636346207587165939243300709553806116595178788) * 10 ^ 70 + 6048328459413340204147664753953881888040598729757946527597482866281851)

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

Polynomial.coeff recurrence2Scalar3Shift 299 = (91031807695649233122014570432927561621745593832438 * 10 ^ 70 + 4373662020931014897475328311506803271186745047917910026997060938264616) * 10 ^ 70 + 5827314859130264031626777271148621388224832953743579971629520499560156