Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC1Low.Coefficients0To24

Recurrence 2 lookup certificate: C1 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.recurrence2C1_coeff_0 :
Polynomial.coeff remainder4Coefficient1 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_1 :
Polynomial.coeff remainder4Coefficient1 1 = -49864
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_2 :
Polynomial.coeff remainder4Coefficient1 2 = 142028948
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_3 :
Polynomial.coeff remainder4Coefficient1 3 = 344400204764
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_4 :
Polynomial.coeff remainder4Coefficient1 4 = -587903610648779
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_5 :
Polynomial.coeff remainder4Coefficient1 5 = 158035318466840996
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_6 :
Polynomial.coeff remainder4Coefficient1 6 = 5772722755895982907
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_7 :
Polynomial.coeff remainder4Coefficient1 7 = -3971490080024822192413
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_8 :
Polynomial.coeff remainder4Coefficient1 8 = 292652123040945272506269
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_9 :
Polynomial.coeff remainder4Coefficient1 9 = -107118672277416844731585299
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_10 :
Polynomial.coeff remainder4Coefficient1 10 = 49104202880088014971535860196
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_11 :
Polynomial.coeff remainder4Coefficient1 11 = -14214096746171581073373883013493
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_12 :
Polynomial.coeff remainder4Coefficient1 12 = 3136116976645669102440238442528505
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_13 :
Polynomial.coeff remainder4Coefficient1 13 = -553175092455905043213051246143020842
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_14 :
Polynomial.coeff remainder4Coefficient1 14 = 79750547286391391475211516919307864378
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_15 :
Polynomial.coeff remainder4Coefficient1 15 = -9569938800838338416909800255924360824985
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_16 :
Polynomial.coeff remainder4Coefficient1 16 = 969754651769990576106064394879194168969595
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_17 :
Polynomial.coeff remainder4Coefficient1 17 = -83964776017962601868543027016355974948108380
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_18 :
Polynomial.coeff remainder4Coefficient1 18 = 6273926971987303911366815435118483731917436353
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_19 :
Polynomial.coeff remainder4Coefficient1 19 = -408071179054335301489933550987499700628272411498
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_20 :
Polynomial.coeff remainder4Coefficient1 20 = 23280093578653574715187356656115616759329464117735
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_21 :
Polynomial.coeff remainder4Coefficient1 21 = -1172803729453016030230311719931029727325551630500514
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_22 :
Polynomial.coeff remainder4Coefficient1 22 = 52493206444990632314214067124443872028382507959715506
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_23 :
Polynomial.coeff remainder4Coefficient1 23 = -2099022067975498985007779493293867910670290608749656750
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_24 :
Polynomial.coeff remainder4Coefficient1 24 = 75362672726742822801985248290865075485180660447016592265