Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC1High.Coefficients96To118

Recurrence 2 lookup certificate: C1 source coefficients, high 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_96 :
Polynomial.coeff remainder4Coefficient1 96 = 7475177460798968777583282313269 * 10 ^ 70 + 8066718384764117436995108586200250777778185745543772160125771622169361
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_97 :
Polynomial.coeff remainder4Coefficient1 97 = -(7482451797703971722366361355000 * 10 ^ 70 + 5270950568146464834893398230570805357347094986005454742401472601980335)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_98 :
Polynomial.coeff remainder4Coefficient1 98 = 7243614148603187414932177774770 * 10 ^ 70 + 3511422848650818334217699093914898487931426192418271730445719627103285
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_99 :
Polynomial.coeff remainder4Coefficient1 99 = -(6781690581702507758067397737376 * 10 ^ 70 + 4734538555728387632604968013737638873832540799891614027876921972604357)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_100 :
Polynomial.coeff remainder4Coefficient1 100 = 6140017427523117285803397662541 * 10 ^ 70 + 8448716634365636828083858587388839773345016179486663380073920719746749
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_101 :
Polynomial.coeff remainder4Coefficient1 101 = -(5375554210578042600925739350267 * 10 ^ 70 + 9898302329500112196149001603079423243961347340468666007474433875768123)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_102 :
Polynomial.coeff remainder4Coefficient1 102 = 4550585390331270997222547994034 * 10 ^ 70 + 7099109700348463158141813057573975091384837127745680877471881247431711
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_103 :
Polynomial.coeff remainder4Coefficient1 103 = -(3724477496928350026231910909241 * 10 ^ 70 + 666312848718010993686080104049483661578954328757820846239994666186564)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_104 :
Polynomial.coeff remainder4Coefficient1 104 = 2946975260902021780599264580861 * 10 ^ 70 + 1078341050731413751121957123404828488189389253902530281997849497641148
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_105 :
Polynomial.coeff remainder4Coefficient1 105 = -(2254005457602165681829979393411 * 10 ^ 70 + 3720179010930614624379613894284279184166161606979984431402882679108241)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_106 :
Polynomial.coeff remainder4Coefficient1 106 = 1666289279034895075944571826565 * 10 ^ 70 + 2819970357199525437735572315291797311266751764408473362168504863481880
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_107 :
Polynomial.coeff remainder4Coefficient1 107 = -(1190440923042996367756715697392 * 10 ^ 70 + 986070029279986604449811523739018628786974308457964549438364727944960)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_108 :
Polynomial.coeff remainder4Coefficient1 108 = 821803419234149993591490999051 * 10 ^ 70 + 426746426653445035338274175813464482599086124019518304690865767842911
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_109 :
Polynomial.coeff remainder4Coefficient1 109 = -(548109351697741238166283084386 * 10 ^ 70 + 9470647752374042594647276219032955259228712677159647942417641353568025)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_110 :
Polynomial.coeff remainder4Coefficient1 110 = 353133203097499911730942991457 * 10 ^ 70 + 4129773425014224605868514857643823042759024778782340646601505980952053
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_111 :
Polynomial.coeff remainder4Coefficient1 111 = -(219741463674264861095895267338 * 10 ^ 70 + 1610206486011710546496615755547375075949559716134298998318744939351872)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_112 :
Polynomial.coeff remainder4Coefficient1 112 = 132043159619196054915996181816 * 10 ^ 70 + 4065850479252478099559657915467719041118028544752132163508886933676552
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_113 :
Polynomial.coeff remainder4Coefficient1 113 = -(76608756571631665694525888022 * 10 ^ 70 + 2897239801711860293432438077723790361816585229100664145171205528497700)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_114 :
Polynomial.coeff remainder4Coefficient1 114 = 42907145090774203459211081320 * 10 ^ 70 + 9033435008776763749977098687326871981357776769175542755505404326475257
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_115 :
Polynomial.coeff remainder4Coefficient1 115 = -(23195510046346500749846600983 * 10 ^ 70 + 9129085229474743802767995792118189104328418741467371543881209847745440)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_116 :
Polynomial.coeff remainder4Coefficient1 116 = 12101586850188405689909264983 * 10 ^ 70 + 3770074072198420270202571350979399552965201310838640764313338784743622
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_117 :
Polynomial.coeff remainder4Coefficient1 117 = -(6092470096139417495259241813 * 10 ^ 70 + 2783672712156360001938658891334201444099069419098159487678889689955344)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_118 :
Polynomial.coeff remainder4Coefficient1 118 = 2959449843423416825051695423 * 10 ^ 70 + 8491588558504025273457401767263972416884924298417024656667405485064981