Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupA4SquarePart1.Coefficients319To356

Recurrence 4 lookup certificate: A4Square coefficient convolution #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_319 :
Polynomial.coeff recurrence4A4Square 319 = 6879651957795406699976510832241735001566260664798167803421520854403 * 10 ^ 70 + 6755758607973274499951611465998900881878731182517666066841864170246982
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_320 :
Polynomial.coeff recurrence4A4Square 320 = -(1257619790909101578225125267737285745220331705219208690634265748231 * 10 ^ 70 + 8955291507061866872370908324922494700575014894033598611280061145499406)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_321 :
Polynomial.coeff recurrence4A4Square 321 = 43093688845195770101826873793510832190684740060022232964566605267 * 10 ^ 70 + 1336624924118391473282581344612719571946692935534167434403121244439310
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_322 :
Polynomial.coeff recurrence4A4Square 322 = 2070542378997992651063561879071458474900703722082548867819056129 * 10 ^ 70 + 3035107164629534317399366510192017368819220210022712655709347152503140
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_323 :
Polynomial.coeff recurrence4A4Square 323 = -(188528004253068622754226673132190771963010535249132852311131787 * 10 ^ 70 + 6117495724695797464183215322085140981318881275461415137457789904848090)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_324 :
Polynomial.coeff recurrence4A4Square 324 = -(294282209461227529541356883740355613760463413093657242441943 * 10 ^ 70 + 2505205535395393955702383338255867464319680073549258799221015557447053)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_325 :
Polynomial.coeff recurrence4A4Square 325 = 387459991758440756964227748700515339477852461946315865323018 * 10 ^ 70 + 7795581671587384477151271753039012305073671087496586340841121534377198
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_326 :
Polynomial.coeff recurrence4A4Square 326 = -(1622099580446484303211332274153952765699595652422329019029 * 10 ^ 70 + 1651997914843532681746125682307742590705127428486541287166017442807877)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_327 :
Polynomial.coeff recurrence4A4Square 327 = -(582367602522785410427371681812622465169440013364389584255 * 10 ^ 70 + 1705836699972071455456790253068250103825719056038841920499999643909290)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_328 :
Polynomial.coeff recurrence4A4Square 328 = -(5222435568130091972784452359487927391850341312580541986 * 10 ^ 70 + 8837627283997237100844458352313435720050885477564169612467266025684704)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_329 :
Polynomial.coeff recurrence4A4Square 329 = 514319422458267499276625972545810867513676390243094557 * 10 ^ 70 + 988188505378428598858164005381085095665241038359223914611692715789508
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_330 :
Polynomial.coeff recurrence4A4Square 330 = 19981540052068574745668843061227113339000697637228144 * 10 ^ 70 + 9954605277978992533872659248499959282069883241051720270753751415174055
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_331 :
Polynomial.coeff recurrence4A4Square 331 = 365964004912955106747576484725887963583923522135672 * 10 ^ 70 + 6351018308034691681083054424963318390136401442928649838977885865931266
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_332 :
Polynomial.coeff recurrence4A4Square 332 = 4135499660108401371702405968273675477107181696746 * 10 ^ 70 + 9352743612518361837932044567071682761865818296273779896436449610732726
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_333 :
Polynomial.coeff recurrence4A4Square 333 = 31011430833655776944198952579161357127672736915 * 10 ^ 70 + 1108301906702951224022436980634738492543346832272801136221677640863510
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_334 :
Polynomial.coeff recurrence4A4Square 334 = 155884162685842677808667336959691517559004952 * 10 ^ 70 + 7098626749034659390388446399978288422959462121337871826288553343472530
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_335 :
Polynomial.coeff recurrence4A4Square 335 = 498735895326936922651666867774927824988637 * 10 ^ 70 + 6909101454246856907063380220761105499588746500240178053694603934728614
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_336 :
Polynomial.coeff recurrence4A4Square 336 = 788422191402604240471919215696905149419 * 10 ^ 70 + 1964720620882930844723072421587861464813671498597170387242395354888632
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_337 :
Polynomial.coeff recurrence4A4Square 337 = -(713197692892228556255485419926848706 * 10 ^ 70 + 9304319078146167847296676488297726596136315398230956650043767285787342)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_338 :
Polynomial.coeff recurrence4A4Square 338 = -(6597078588303681490384788537951714 * 10 ^ 70 + 1561141312029677125454368453577217449159168961830509056385891328383362)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_339 :
Polynomial.coeff recurrence4A4Square 339 = -(13870585199136708050228178391108 * 10 ^ 70 + 3357640084507328667026464295002777761307829931983888115692153854641910)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_340 :
Polynomial.coeff recurrence4A4Square 340 = -(8841789082681546770235451228 * 10 ^ 70 + 7968194793544480289873177822745798998221347372224465960387362181727028)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_341 :
Polynomial.coeff recurrence4A4Square 341 = 17057135479476206256634696 * 10 ^ 70 + 1017222792145342949002754567156161117275414137041804849700262135547220
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_342 :
Polynomial.coeff recurrence4A4Square 342 = 44592042870203709611942 * 10 ^ 70 + 3511932960808022206290932812189882647088051191860661292981576646655999
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_343 :
Polynomial.coeff recurrence4A4Square 343 = 46478067118278524275 * 10 ^ 70 + 8408250256520402828523525550669930281037760203882056647468301010344308
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_344 :
Polynomial.coeff recurrence4A4Square 344 = 26815579655532077 * 10 ^ 70 + 7246795778406707859482058756966909352451749872423681619003560223635325
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_345 :
Polynomial.coeff recurrence4A4Square 345 = 8994751079290 * 10 ^ 70 + 9676088662409391965397422361705638564494022782934929096940758026374270
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_346 :
Polynomial.coeff recurrence4A4Square 346 = 1744366891 * 10 ^ 70 + 3088183840292621173402735344186274387874458499970562653214501564693674
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_347 :
Polynomial.coeff recurrence4A4Square 347 = 189655 * 10 ^ 70 + 5541206303811756361868383890594524590284187969400259529138816582695862
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_348 :
Polynomial.coeff recurrence4A4Square 348 = 11 * 10 ^ 70 + 1118152040355336922123889324615966148225058072231422799739216906330957
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_349 :
Polynomial.coeff recurrence4A4Square 349 = 3294187829126525658111999044906005665122417868950220234815569550036
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_350 :
Polynomial.coeff recurrence4A4Square 350 = 46761195054975912432022141342913210693235416615085836269304792
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_351 :
Polynomial.coeff recurrence4A4Square 351 = 282228363208519389703829178132802097983214024899202160594
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_352 :
Polynomial.coeff recurrence4A4Square 352 = 688588957607202701068994497847406833908335977217771
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_353 :
Polynomial.coeff recurrence4A4Square 353 = 510094750000584395586589881327884907544173790
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_354 :
Polynomial.coeff recurrence4A4Square 354 = 121790380541980693795330736786246777411
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_355 :
Polynomial.coeff recurrence4A4Square 355 = 3261532994918344993998095763390
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_356 :
Polynomial.coeff recurrence4A4Square 356 = 23215239933528791584969