Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupA6Low

Recurrence 2 lookup certificate: A6 source coefficients, low half #

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.recurrence2A6_coeff_0 :
Polynomial.coeff remainder2Coefficient6 0 = -606
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_1 :
Polynomial.coeff remainder2Coefficient6 1 = -264384
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_2 :
Polynomial.coeff remainder2Coefficient6 2 = 656868640
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_3 :
Polynomial.coeff remainder2Coefficient6 3 = -43610885488
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_4 :
Polynomial.coeff remainder2Coefficient6 4 = -7907413645917
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_5 :
Polynomial.coeff remainder2Coefficient6 5 = 237849108519302
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_6 :
Polynomial.coeff remainder2Coefficient6 6 = 17822290888370542
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_7 :
Polynomial.coeff remainder2Coefficient6 7 = -60757622243990768
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_8 :
Polynomial.coeff remainder2Coefficient6 8 = -15092317899760440692
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_9 :
Polynomial.coeff remainder2Coefficient6 9 = -122739733042983787952
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_10 :
Polynomial.coeff remainder2Coefficient6 10 = 3980510503323414556252
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_11 :
Polynomial.coeff remainder2Coefficient6 11 = 80975272851461060031324
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_12 :
Polynomial.coeff remainder2Coefficient6 12 = -339731311869300366432704
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_13 :
Polynomial.coeff remainder2Coefficient6 13 = -14893034520022581397395970
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_14 :
Polynomial.coeff remainder2Coefficient6 14 = -61507058526884679075023217
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_15 :
Polynomial.coeff remainder2Coefficient6 15 = 1557412099701861736209197599
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_16 :
Polynomial.coeff remainder2Coefficient6 16 = 11931824111968927302483079140
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_17 :
Polynomial.coeff remainder2Coefficient6 17 = -74615194376512967677074331502
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_18 :
Polynomial.coeff remainder2Coefficient6 18 = -1147978231603713844269051911554
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_19 :
Polynomial.coeff remainder2Coefficient6 19 = 1703605390132880923263815628087
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_20 :
Polynomial.coeff remainder2Coefficient6 20 = 65342815875548638995525416873715
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_21 :
Polynomial.coeff remainder2Coefficient6 21 = 46764779696712004097218540893258
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_22 :
Polynomial.coeff remainder2Coefficient6 22 = -2756851892830333293894575180613507
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_23 :
Polynomial.coeff remainder2Coefficient6 23 = -4973479925282740496115957637429406
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_24 :
Polynomial.coeff remainder2Coefficient6 24 = 90957482947576568207820968873219052
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_25 :
Polynomial.coeff remainder2Coefficient6 25 = 210316203154359032521086649236863646
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_26 :
Polynomial.coeff remainder2Coefficient6 26 = -2519572862830697884162971473184893653
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_27 :
Polynomial.coeff remainder2Coefficient6 27 = -5716537617376765869030209898778114261
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_28 :
Polynomial.coeff remainder2Coefficient6 28 = 60367025213541084292114337935339630656
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_29 :
Polynomial.coeff remainder2Coefficient6 29 = 106109478758528122081569249927892450975
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_30 :
Polynomial.coeff remainder2Coefficient6 30 = -1258161069668623656362952421948325399372
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_31 :
Polynomial.coeff remainder2Coefficient6 31 = -1140152263465682044046210616394825658004
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_32 :
Polynomial.coeff remainder2Coefficient6 32 = 22303221764783494685504179773267006285479
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_33 :
Polynomial.coeff remainder2Coefficient6 33 = -3068732178837805852846609862113546712980
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_34 :
Polynomial.coeff remainder2Coefficient6 34 = -321295042349681723632820191220560028096900
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_35 :
Polynomial.coeff remainder2Coefficient6 35 = 424684769546239265370557834075128561258657
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_36 :
Polynomial.coeff remainder2Coefficient6 36 = 3467010735621713056201496621093019705005373
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_37 :
Polynomial.coeff remainder2Coefficient6 37 = -9820907169482207987595217407352126266374824
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_38 :
Polynomial.coeff remainder2Coefficient6 38 = -22643107225379856272866206550665913259766049
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_39 :
Polynomial.coeff remainder2Coefficient6 39 = 134638847786245837888592364557673177253229780
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_40 :
Polynomial.coeff remainder2Coefficient6 40 = -14699805210117737208311297643153352365036420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_41 :
Polynomial.coeff remainder2Coefficient6 41 = -1140838767007516959294651878397634074067432175
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_42 :
Polynomial.coeff remainder2Coefficient6 42 = 2198291250583775650210278270666734838628936545
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_43 :
Polynomial.coeff remainder2Coefficient6 43 = 4377108880256740642198220811140850983490192676
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_44 :
Polynomial.coeff remainder2Coefficient6 44 = -23751755542444203265532361883311010910235695327
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_45 :
Polynomial.coeff remainder2Coefficient6 45 = 19324817302042652217758620587384065055762449306
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_46 :
Polynomial.coeff remainder2Coefficient6 46 = 101615939163603552285300697518056435893445132998
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A6_coeff_47 :
Polynomial.coeff remainder2Coefficient6 47 = -317667961885729755212373371552547149669387921084