Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC1Low.Coefficients73To95

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_73 :
Polynomial.coeff remainder4Coefficient1 73 = -(673406662380562441615730444 * 10 ^ 70 + 5650599672541830834807385947703248823246143331196618802803505502368546)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_74 :
Polynomial.coeff remainder4Coefficient1 74 = 1474689695816068070169752835 * 10 ^ 70 + 3137200631707956748052241466478415799451737103455948953483302972125776
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_75 :
Polynomial.coeff remainder4Coefficient1 75 = -(3116335736672213691230325280 * 10 ^ 70 + 3538908418090275412786499396601039306993363165059220917471457421234405)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_76 :
Polynomial.coeff remainder4Coefficient1 76 = 6356434037364467604513070668 * 10 ^ 70 + 6824225731186468962565164485480569693331231251160254622666918536864800
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_77 :
Polynomial.coeff remainder4Coefficient1 77 = -(12517196451644997210490589661 * 10 ^ 70 + 8952793572317513989497192809713253440284703671390066152637559923532985)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_78 :
Polynomial.coeff remainder4Coefficient1 78 = 23802177535863872741551485090 * 10 ^ 70 + 292887210790698825334823730949289720404805058300699356312956639384317
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_79 :
Polynomial.coeff remainder4Coefficient1 79 = -(43714735914136138419305211733 * 10 ^ 70 + 4788662897140316478402336430454409513983949137084300037063944551147298)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_80 :
Polynomial.coeff remainder4Coefficient1 80 = 77556782190389065407585725964 * 10 ^ 70 + 4929527469090857054185679096334035236775874461065468012444502764401853
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_81 :
Polynomial.coeff remainder4Coefficient1 81 = -(132943038148629912951468831578 * 10 ^ 70 + 152789368545902747493388273741052920547537094210665543074496889729088)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_82 :
Polynomial.coeff remainder4Coefficient1 82 = 220207724890644743085359855389 * 10 ^ 70 + 114225462401913753593214322415907050455633764214377182684412614230752
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_83 :
Polynomial.coeff remainder4Coefficient1 83 = -(352518670128378308979139979447 * 10 ^ 70 + 3234358749932651839835564180854538276137875438787011874149603030403537)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_84 :
Polynomial.coeff remainder4Coefficient1 84 = 545469161476402307353104070230 * 10 ^ 70 + 7656316847916493234860914112510162245447135758104736039368205730526987
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_85 :
Polynomial.coeff remainder4Coefficient1 85 = -(815919284864171231676430146758 * 10 ^ 70 + 6974465266589872663432128449433840896684202728687529278870045599237988)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_86 :
Polynomial.coeff remainder4Coefficient1 86 = 1179935232981088818057549535421 * 10 ^ 70 + 8191550837717204166369509184452180437352878650046362069941822351364446
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_87 :
Polynomial.coeff remainder4Coefficient1 87 = -(1649844212643411643634331665034 * 10 ^ 70 + 2857350982664367409294799767717257040382397524622402320096834649432197)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_88 :
Polynomial.coeff remainder4Coefficient1 88 = 2230674435053702559040424812780 * 10 ^ 70 + 7897881866369854183869091199971464307651807369111756289413874227776966
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_89 :
Polynomial.coeff remainder4Coefficient1 89 = -(2916537555750793141066193944546 * 10 ^ 70 + 2312656643238168859178457645928940452388899103897512486821310163953291)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_90 :
Polynomial.coeff remainder4Coefficient1 90 = 3687752601862470316747143276375 * 10 ^ 70 + 5560008013785500787097519619926894089579994372133560093973497750182057
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_91 :
Polynomial.coeff remainder4Coefficient1 91 = -(4509606164795666378851292554584 * 10 ^ 70 + 7092885709740495363050355230729174597368905770385258128005813899488456)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_92 :
Polynomial.coeff remainder4Coefficient1 92 = 5333509602328363454579365935103 * 10 ^ 70 + 5581515286902021828766395956721222300966167730267180761867430032672331
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_93 :
Polynomial.coeff remainder4Coefficient1 93 = -(6100921162395537341992001700498 * 10 ^ 70 + 9634890789284671657517608093554963352535873853749814565156813007108409)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_94 :
Polynomial.coeff remainder4Coefficient1 94 = 6749803593406874386655262991563 * 10 ^ 70 + 9032723311724993287976959976215791065959150148108192669649856306506384
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_95 :
Polynomial.coeff remainder4Coefficient1 95 = -(7222725338548068760455368176789 * 10 ^ 70 + 608447778611744077227400614602145429245539912289115627539754637699390)