Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupA5Low

Recurrence 2 lookup certificate: A5 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.recurrence2A5_coeff_0 :
Polynomial.coeff remainder2Coefficient5 0 = -8
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_1 :
Polynomial.coeff remainder2Coefficient5 1 = -4584
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_2 :
Polynomial.coeff remainder2Coefficient5 2 = 58202904
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_3 :
Polynomial.coeff remainder2Coefficient5 3 = -13173586573
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_4 :
Polynomial.coeff remainder2Coefficient5 4 = -826150121927
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_5 :
Polynomial.coeff remainder2Coefficient5 5 = 152811697040613
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_6 :
Polynomial.coeff remainder2Coefficient5 6 = 1321979052167081
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_7 :
Polynomial.coeff remainder2Coefficient5 7 = -239337682022022144
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_8 :
Polynomial.coeff remainder2Coefficient5 8 = -4010384813694609235
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_9 :
Polynomial.coeff remainder2Coefficient5 9 = 140981990055572131702
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_10 :
Polynomial.coeff remainder2Coefficient5 10 = 2708132833691499223520
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_11 :
Polynomial.coeff remainder2Coefficient5 11 = -11117019750973116692969
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_12 :
Polynomial.coeff remainder2Coefficient5 12 = -1038032059894976781868696
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_13 :
Polynomial.coeff remainder2Coefficient5 13 = -1516553408964565706773563
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_14 :
Polynomial.coeff remainder2Coefficient5 14 = 113435219738758599710588858
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_15 :
Polynomial.coeff remainder2Coefficient5 15 = 1281528474945542949359844633
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_16 :
Polynomial.coeff remainder2Coefficient5 16 = -10949556985199660678063311825
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_17 :
Polynomial.coeff remainder2Coefficient5 17 = -125392070547471792509348429414
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_18 :
Polynomial.coeff remainder2Coefficient5 18 = 215558598921243747288171008522
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_19 :
Polynomial.coeff remainder2Coefficient5 19 = 10589490421697306581022864221125
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_20 :
Polynomial.coeff remainder2Coefficient5 20 = 2185427701132490215696739421726
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_21 :
Polynomial.coeff remainder2Coefficient5 21 = -509558385722369015881141643744004
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_22 :
Polynomial.coeff remainder2Coefficient5 22 = -973972135415319263109760588480179
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_23 :
Polynomial.coeff remainder2Coefficient5 23 = 20888946531069052727010274247959325
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_24 :
Polynomial.coeff remainder2Coefficient5 24 = 48030170025326506913702104280824156
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_25 :
Polynomial.coeff remainder2Coefficient5 25 = -676296360117176906042635167860569831
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_26 :
Polynomial.coeff remainder2Coefficient5 26 = -1590442759177347388958151340464345290
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_27 :
Polynomial.coeff remainder2Coefficient5 27 = 19132701444277355709761164775195411393
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_28 :
Polynomial.coeff remainder2Coefficient5 28 = 34285205475050473373020125037058876286
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_29 :
Polynomial.coeff remainder2Coefficient5 29 = -466785756737243618782844261631760400715
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_30 :
Polynomial.coeff remainder2Coefficient5 30 = -412588225219251476476316758306081249061
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_31 :
Polynomial.coeff remainder2Coefficient5 31 = 9692705499083531167630753290409160783478
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_32 :
Polynomial.coeff remainder2Coefficient5 32 = -2380408842837340426918169537663901078116
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_33 :
Polynomial.coeff remainder2Coefficient5 33 = -163589430880070156827029618454308988307158
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_34 :
Polynomial.coeff remainder2Coefficient5 34 = 252102819302740101766946367034325092681392
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_35 :
Polynomial.coeff remainder2Coefficient5 35 = 2069187720024328570227264006657291355787421
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_36 :
Polynomial.coeff remainder2Coefficient5 36 = -6686117133490773997916420110131588575194757
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_37 :
Polynomial.coeff remainder2Coefficient5 37 = -15713983361751386062903313597586957964997198
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_38 :
Polynomial.coeff remainder2Coefficient5 38 = 108107639108100048200385184492677540844180312
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_39 :
Polynomial.coeff remainder2Coefficient5 39 = -20984404370839676984211613442320871622164412
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_40 :
Polynomial.coeff remainder2Coefficient5 40 = -1099916178960450575915685818529555687157919662
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_41 :
Polynomial.coeff remainder2Coefficient5 41 = 2396380361633016720239785833367126775002379437
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_42 :
Polynomial.coeff remainder2Coefficient5 42 = 5210269669951627349681283239449495527787077121
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_43 :
Polynomial.coeff remainder2Coefficient5 43 = -31726243031577828134638573492632902354471093984
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_44 :
Polynomial.coeff remainder2Coefficient5 44 = 27161067309970447311973679620919266785043335179
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_45 :
Polynomial.coeff remainder2Coefficient5 45 = 178205050773421933199244930914495314572679868757
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_46 :
Polynomial.coeff remainder2Coefficient5 46 = -596676247251947916726407473354347441926711917636
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_47 :
Polynomial.coeff remainder2Coefficient5 47 = 217432829839310336002817984518166135227832232782
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_48 :
Polynomial.coeff remainder2Coefficient5 48 = 3120093033409065786758827883803080316430806655045
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2A5_coeff_49 :
Polynomial.coeff remainder2Coefficient5 49 = -8665970048652318840432392931146127238888078672941