Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupLeadingSquarePart1

Recurrence 2 lookup certificate: LeadingSquare coefficient convolution #

This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_224 :
Polynomial.coeff recurrence2LeadingSquare 224 = 561809761417290135585358064070334009503682424858883366562967118721 * 10 ^ 70 + 1267377411830800253673091633820916822465455485082650459395233447406406
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_225 :
Polynomial.coeff recurrence2LeadingSquare 225 = -(58621623113470959536612563423384900819108175116212178194759299991 * 10 ^ 70 + 3197270855949458407654059225323685398018341953685335948671800447565622)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_226 :
Polynomial.coeff recurrence2LeadingSquare 226 = 5654646791334891163180811991514835722586150645529370525005555025 * 10 ^ 70 + 2491592221681213210366656829801459736634745809782604066972868749535703
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_227 :
Polynomial.coeff recurrence2LeadingSquare 227 = -(502207919304935493863026772744868723576554329361824668685097198 * 10 ^ 70 + 822628446767478857412598553183753164533565300883454632656896928795302)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_228 :
Polynomial.coeff recurrence2LeadingSquare 228 = 40883739372899976403995774669750458666500107055294971252843718 * 10 ^ 70 + 664152813445048736941894973947984780808800372330968267677582210847135
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_229 :
Polynomial.coeff recurrence2LeadingSquare 229 = -(3035582872312280507228906623488125720153601986813114188170157 * 10 ^ 70 + 3958663405679618182530702662017700522250678284193957694181787567129962)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_230 :
Polynomial.coeff recurrence2LeadingSquare 230 = 204424673581056177391562605993804808697109917032794883958632 * 10 ^ 70 + 3758243883643324923171703834851926241130962816797219578946957694898028
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_231 :
Polynomial.coeff recurrence2LeadingSquare 231 = -(12407761274524548054352292238204188663599817398960623863107 * 10 ^ 70 + 3025200631630691693146437794988718298630907170333069859018963093026134)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_232 :
Polynomial.coeff recurrence2LeadingSquare 232 = 673949085123631859268691057639288307199633637829206666572 * 10 ^ 70 + 6766371887717385774749830915345929390722328417180227789644426962474733
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_233 :
Polynomial.coeff recurrence2LeadingSquare 233 = -(32493634160801342122221232307759319455763996340018635774 * 10 ^ 70 + 8470577107644099678023432405205586602852606796341490454120780639539430)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_234 :
Polynomial.coeff recurrence2LeadingSquare 234 = 1377613349505456866723128077963437619444679401495324239 * 10 ^ 70 + 3446104712093439741472727877315406591206950008178631536995663760485137
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_235 :
Polynomial.coeff recurrence2LeadingSquare 235 = -(50797767058235850070711144865158715419542093118985747 * 10 ^ 70 + 9852866194208145312475868768133488072083669622620587881257886429645868)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_236 :
Polynomial.coeff recurrence2LeadingSquare 236 = 1607939379379968372478556430804934177003922969514504 * 10 ^ 70 + 5514152136087890738958755552199277499913799747722077762257412080548610
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_237 :
Polynomial.coeff recurrence2LeadingSquare 237 = -(42998253372772890541051360049826234760646013855082 * 10 ^ 70 + 7632709854350945714703022698913843338005919241534085204893813772233260)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_238 :
Polynomial.coeff recurrence2LeadingSquare 238 = 951737838638004543567181235992893153489967863312 * 10 ^ 70 + 588330584551406139297989269195952025204045562199404816492024931085286
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_239 :
Polynomial.coeff recurrence2LeadingSquare 239 = -(16957553185211324559971225701742983204324775162 * 10 ^ 70 + 8509603758573789201180414536420787025003982038878748953570464949274184)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_240 :
Polynomial.coeff recurrence2LeadingSquare 240 = 233073908422455085885065242601835263197905841 * 10 ^ 70 + 5557421957841954438792747917135043257204218186215064161969879921821024
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_241 :
Polynomial.coeff recurrence2LeadingSquare 241 = -(2282135561078593235068932087932267857111489 * 10 ^ 70 + 2913425173114419360017600604440949819545123610837435414138138203325562)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_242 :
Polynomial.coeff recurrence2LeadingSquare 242 = 12699925842094552641005027792615968774784 * 10 ^ 70 + 5087779474356342071759153966331467126075117820082403826268289462191408
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_243 :
Polynomial.coeff recurrence2LeadingSquare 243 = 13235890497248962405078804334327787549 * 10 ^ 70 + 717196278864211425241316528067562875156847300900824522712498960513128
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_244 :
Polynomial.coeff recurrence2LeadingSquare 244 = -(888769690578224965769577527148145705 * 10 ^ 70 + 6311908186118668759169709388210241262529946510078530934931949249777165)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_245 :
Polynomial.coeff recurrence2LeadingSquare 245 = 6591183252195620445529857283924621 * 10 ^ 70 + 8578087086772039376704652641030212680884041868381979789802844040734890
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_246 :
Polynomial.coeff recurrence2LeadingSquare 246 = -(9521708187634297077491647703786 * 10 ^ 70 + 5773407055877061872535422247793287096207382579842969357394317568201231)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_247 :
Polynomial.coeff recurrence2LeadingSquare 247 = -(152199368632941720907287026288 * 10 ^ 70 + 9470528690200840531886874799841826828362247016558448088545204199023660)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_248 :
Polynomial.coeff recurrence2LeadingSquare 248 = 951179927042320541491367718 * 10 ^ 70 + 7099706315522876211007602325259702763961639317047489799315109691621596
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_249 :
Polynomial.coeff recurrence2LeadingSquare 249 = -(913805482927709469001513 * 10 ^ 70 + 1501946789877945668389565758428867107594273305538065689946904345952682)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_250 :
Polynomial.coeff recurrence2LeadingSquare 250 = -(11043535116429383580879 * 10 ^ 70 + 7211188543246020734587759503637895002172724101780653086701682714544867)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_251 :
Polynomial.coeff recurrence2LeadingSquare 251 = 46241981649816768616 * 10 ^ 70 + 6666445979314224947688883614767358061767643910388377365494886630608028
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_252 :
Polynomial.coeff recurrence2LeadingSquare 252 = -(39179208295356993 * 10 ^ 70 + 955145394499404501391588489566709785373118435050329670701696836374851)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_253 :
Polynomial.coeff recurrence2LeadingSquare 253 = -(205358698960284 * 10 ^ 70 + 4886539382272811185449248981975309840420720554500193118218364382619158)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_254 :
Polynomial.coeff recurrence2LeadingSquare 254 = 762979121991 * 10 ^ 70 + 2376339231357296252793618506141108963497373477934851059795916552708738
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_255 :
Polynomial.coeff recurrence2LeadingSquare 255 = -(1252542529 * 10 ^ 70 + 2855645366157441560821791846063742747170387688567707668819919351475680)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_256 :
Polynomial.coeff recurrence2LeadingSquare 256 = 1190390 * 10 ^ 70 + 5668669804374762879023083911000695840052534576183597927143988184916627
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_257 :
Polynomial.coeff recurrence2LeadingSquare 257 = -(686 * 10 ^ 70 + 7129352649463879045477947982222711245069047553500365887609327273800266)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_258 :
Polynomial.coeff recurrence2LeadingSquare 258 = 2385711292812592668185321574152758713260339832977141265159278262127015
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_259 :
Polynomial.coeff recurrence2LeadingSquare 259 = -481872277519030416031028333064414110199545218781126383778227319502
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_260 :
Polynomial.coeff recurrence2LeadingSquare 260 = 53841771322926348327685386648171838138229482693893494721410789
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_261 :
Polynomial.coeff recurrence2LeadingSquare 261 = -3092793674963169611298319377989159470325820478404925031202
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_262 :
Polynomial.coeff recurrence2LeadingSquare 262 = 85062553733218251738974939428507320800293573276860431
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_263 :
Polynomial.coeff recurrence2LeadingSquare 263 = -971429686168595293080674931260101722348428922526
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_264 :
Polynomial.coeff recurrence2LeadingSquare 264 = 4339432442551415782594727081480877152045890
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_265 :
Polynomial.coeff recurrence2LeadingSquare 265 = -5221574427476610763264270701221703918
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_266 :
Polynomial.coeff recurrence2LeadingSquare 266 = 1895399483217394147509375939816
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_267 :
Polynomial.coeff recurrence2LeadingSquare 267 = -25231363388779055119656
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2LeadingSquare_coeff_268 :
Polynomial.coeff recurrence2LeadingSquare 268 = 85566736552441