Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar3ShiftPart1.Coefficients336To375

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.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_336 :
Polynomial.coeff recurrence2Scalar3Shift 336 = -((13247371014 * 10 ^ 70 + 8308539211999096722388485415962410364185872180514673753624826899695535) * 10 ^ 70 + 6985533458148373575856872063142775546233871476752823882682530067146651)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_337 :
Polynomial.coeff recurrence2Scalar3Shift 337 = -((171251846 * 10 ^ 70 + 58707341757629495054623911498632908092134146569117089231304209554615) * 10 ^ 70 + 5941924208081933784775686390960777820656383733673613220073438625220822)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_338 :
Polynomial.coeff recurrence2Scalar3Shift 338 = (7729130 * 10 ^ 70 + 6832879553047241271067340599446401415965589416913378221228515693782507) * 10 ^ 70 + 8909107385958603360722874737238722685752069121743241937981853313274324
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_339 :
Polynomial.coeff recurrence2Scalar3Shift 339 = -((79467 * 10 ^ 70 + 2281802734705075892003668072950578076954424970453013313294235048488450) * 10 ^ 70 + 4395690913695422220199081335852946141454146000772407873609878294132236)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_340 :
Polynomial.coeff recurrence2Scalar3Shift 340 = -((466 * 10 ^ 70 + 4192822789109021217301851965792944087098548800274137403540648157776335) * 10 ^ 70 + 4563027060934648235009782246294518642705732782008959115108461183101211)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_341 :
Polynomial.coeff recurrence2Scalar3Shift 341 = (15 * 10 ^ 70 + 7644598980336030532757602447541890761383613873306135639365217265448312) * 10 ^ 70 + 6799391734214307022192141413059846821452046111464051111281872643190236
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_342 :
Polynomial.coeff recurrence2Scalar3Shift 342 = -(627626893075892454386287886836668899936096622397991275063461847421196 * 10 ^ 70 + 6454577332777221710015989226024063462470695218096869255278376080024819)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_343 :
Polynomial.coeff recurrence2Scalar3Shift 343 = -(9930499660016114127638051725177304927415096746931535857697046224674 * 10 ^ 70 + 1356677144963770492598277625363244658674582967419888403805748315475559)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_344 :
Polynomial.coeff recurrence2Scalar3Shift 344 = 81826728700567318714040865446037735878136832542297240542638701158 * 10 ^ 70 + 2807471221351396070560066258490280574202332770110168739958257966099845
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_345 :
Polynomial.coeff recurrence2Scalar3Shift 345 = 257301846929008225471371544164409318792275984656306618155901664 * 10 ^ 70 + 4550066869923006596881721199338682053527518167638310547766548320008541
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_346 :
Polynomial.coeff recurrence2Scalar3Shift 346 = -(3889692393618105503261552997279898198386528612155066406722597 * 10 ^ 70 + 7693397951904969470419032676373995610746940461330205348873839513556655)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_347 :
Polynomial.coeff recurrence2Scalar3Shift 347 = -(740989285024878836121972638973176078254135445440231290242 * 10 ^ 70 + 2861482076530659104164346878315813765031244056657751622108704315531316)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_348 :
Polynomial.coeff recurrence2Scalar3Shift 348 = 96543156598210164959306376260356299965513643544875411100 * 10 ^ 70 + 7479247137229142884484108844962851190008129305776677889612155423853661
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_349 :
Polynomial.coeff recurrence2Scalar3Shift 349 = -(117329047297662773853458320093103492519261978741542481 * 10 ^ 70 + 2124895726658445545673840365825765160183476775091250050414022597989514)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_350 :
Polynomial.coeff recurrence2Scalar3Shift 350 = -(1308762101161586506729729642070179299513105417560564 * 10 ^ 70 + 9139033331594766144437161435722703992529313876594439203128841186741489)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_351 :
Polynomial.coeff recurrence2Scalar3Shift 351 = 2969055682104249693033070283909213065285837969325 * 10 ^ 70 + 3375776272007091730558483455437939107102155080623410248278471689598223
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_352 :
Polynomial.coeff recurrence2Scalar3Shift 352 = 8621666411570524824476412825759622122946989636 * 10 ^ 70 + 5420877912349702067347227654019087734004423696389500428236972240822044
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_353 :
Polynomial.coeff recurrence2Scalar3Shift 353 = -(31943216475720628569317190242591194848812386 * 10 ^ 70 + 2196373438556348006578685190548429672736651147459732028848500123264736)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_354 :
Polynomial.coeff recurrence2Scalar3Shift 354 = -(9619462725666532684998940447891910282728 * 10 ^ 70 + 199653221911724033690506931440753315703795116908561669089088199855243)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_355 :
Polynomial.coeff recurrence2Scalar3Shift 355 = 149364870373557463259330379543222616751 * 10 ^ 70 + 7723818465477456647383307972384702245162566833831079936615132711976765
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_356 :
Polynomial.coeff recurrence2Scalar3Shift 356 = -(154717701436839856146371287802271709 * 10 ^ 70 + 1536783776051650527281760246654030936687451148034203772965148089412056)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_357 :
Polynomial.coeff recurrence2Scalar3Shift 357 = -(153945028770103129077717567469866 * 10 ^ 70 + 2100203697508895887441526848438226328432919045287365977274681632426877)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_358 :
Polynomial.coeff recurrence2Scalar3Shift 358 = 417990921122235296519761732630 * 10 ^ 70 + 884748575913449004617692563562344812670556925242444438558294642939863
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_359 :
Polynomial.coeff recurrence2Scalar3Shift 359 = -(284474063529363702207430955 * 10 ^ 70 + 3290641655238165460358128517580832771568586381193365621498594407387534)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_360 :
Polynomial.coeff recurrence2Scalar3Shift 360 = 20142920343341738292875 * 10 ^ 70 + 991048049413455595692938797710041707775497587375658806592795169062073
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_361 :
Polynomial.coeff recurrence2Scalar3Shift 361 = 59883243616274239521 * 10 ^ 70 + 6586506244118301054368294398929001493128977325780572736350802801938219
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_362 :
Polynomial.coeff recurrence2Scalar3Shift 362 = -(26999596876736381 * 10 ^ 70 + 6330668664512368831426845672176168766310745696891890530854996402178125)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_363 :
Polynomial.coeff recurrence2Scalar3Shift 363 = 4182527216633 * 10 ^ 70 + 9586209700382871870430823030626200207211332330611846469443862095902286
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_364 :
Polynomial.coeff recurrence2Scalar3Shift 364 = -(140237945 * 10 ^ 70 + 1849784473461775035477856139875735881958807820661374535752697602049867)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_365 :
Polynomial.coeff recurrence2Scalar3Shift 365 = -(19222 * 10 ^ 70 + 4723116937040079734726739575414717689070899626466290896544913650486945)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_366 :
Polynomial.coeff recurrence2Scalar3Shift 366 = 1 * 10 ^ 70 + 5171791846473585029461913609637339901287956700507924355201482925353965
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_367 :
Polynomial.coeff recurrence2Scalar3Shift 367 = -326748467231985099277039007699553112269302401102927411775581648598
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_368 :
Polynomial.coeff recurrence2Scalar3Shift 368 = 1866921889427777477585165710501847736200764144627540842918583
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_369 :
Polynomial.coeff recurrence2Scalar3Shift 369 = 1992955521863482669546903058786574235939405405654698452
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_370 :
Polynomial.coeff recurrence2Scalar3Shift 370 = -22194740933985694963963876171341280510094357767775
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_371 :
Polynomial.coeff recurrence2Scalar3Shift 371 = 18495588673549012232517070907111886696608400
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_372 :
Polynomial.coeff recurrence2Scalar3Shift 372 = -2428415422479462826016467479132468682
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_373 :
Polynomial.coeff recurrence2Scalar3Shift 373 = 14109381873722360030037538062
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_374 :
Polynomial.coeff recurrence2Scalar3Shift 374 = 14623435900183798807
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_375 :
Polynomial.coeff recurrence2Scalar3Shift 375 = -22256050974