Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC0Low.Coefficients74To97

Recurrence 2 lookup certificate: C0 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.recurrence2C0_coeff_74 :
Polynomial.coeff remainder4Coefficient0 74 = 877091984276516223227301912 * 10 ^ 70 + 4387112897031501232801110196746143832608541889317368905923470646429335
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_75 :
Polynomial.coeff remainder4Coefficient0 75 = -(1927157339764645003404952377 * 10 ^ 70 + 4069805214443417921045820575471479795673355117669686817980778705336467)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_76 :
Polynomial.coeff remainder4Coefficient0 76 = 4087635345459265407174635325 * 10 ^ 70 + 2011761206551094466884283436548995692673741422330711364913473563022175
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_77 :
Polynomial.coeff remainder4Coefficient0 77 = -(8371766913620828787959910483 * 10 ^ 70 + 5979783516743203546100704133730428311642677841407368228542824643915721)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_78 :
Polynomial.coeff remainder4Coefficient0 78 = 16559748070657190043871716709 * 10 ^ 70 + 2873868588425133217945142839705385257873302472610580920491864676236682
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_79 :
Polynomial.coeff remainder4Coefficient0 79 = -(31643063151446146386796436921 * 10 ^ 70 + 1734007882908553377210873176861967450746453660487280130324779305991769)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_80 :
Polynomial.coeff remainder4Coefficient0 80 = 58422955704673838967458698942 * 10 ^ 70 + 5286503992202649592295700271467845383405589067730884314802796419221016
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_81 :
Polynomial.coeff remainder4Coefficient0 81 = -(104245350404801167085685149183 * 10 ^ 70 + 6046783238729668669918728026912986730319386108799459887279014661430814)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_82 :
Polynomial.coeff remainder4Coefficient0 82 = 179796993080558260279221420551 * 10 ^ 70 + 9726183815259852306846432403121341581982543255244029577645818851102548
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_83 :
Polynomial.coeff remainder4Coefficient0 83 = -(299807251954072261914729804788 * 10 ^ 70 + 2938088605495066869607672772121056283087993811986285799753660362653895)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_84 :
Polynomial.coeff remainder4Coefficient0 84 = 483409145599314153751582281516 * 10 ^ 70 + 8559116475769210647365984170274552135866004812089852982002266574616115
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_85 :
Polynomial.coeff remainder4Coefficient0 85 = -(753837843977681520130181780029 * 10 ^ 70 + 5257363152098877430929499147574127452158415629080105222878627891864087)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_86 :
Polynomial.coeff remainder4Coefficient0 86 = 1137123612057692598698166959408 * 10 ^ 70 + 5091881950338239364148960747191751043145516771316495505414257686275768
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_87 :
Polynomial.coeff remainder4Coefficient0 87 = -(1659511180917703076843649613660 * 10 ^ 70 + 1354035617988662097854306777358389486319929179861922897531904994712005)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_88 :
Polynomial.coeff remainder4Coefficient0 88 = 2343538817729134368586086315801 * 10 ^ 70 + 4217509406710843707448067969711269422730069772867397172527579584838613
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_89 :
Polynomial.coeff remainder4Coefficient0 89 = -(3203035692233677543034133103024 * 10 ^ 70 + 1874977438200640368750943377662360960292298586530160463215722583094871)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_90 :
Polynomial.coeff remainder4Coefficient0 90 = 4237694964683749202580834028176 * 10 ^ 70 + 4096857003286494351749937598679970524384770531354898743124571380337277
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_91 :
Polynomial.coeff remainder4Coefficient0 91 = -(5428251177393272613659067103500 * 10 ^ 70 + 2367731630701682637915427707867611227462934180490392126657667907456342)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_92 :
Polynomial.coeff remainder4Coefficient0 92 = 6733501330921963449621335284059 * 10 ^ 70 + 831169268238333365854208720695242677616955345460937655564127570790800
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_93 :
Polynomial.coeff remainder4Coefficient0 93 = -(8090335925998022791172332624737 * 10 ^ 70 + 5723645827954556020065494930868880071322246256098357069024863089937147)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_94 :
Polynomial.coeff remainder4Coefficient0 94 = 9417526337652128650606095425680 * 10 ^ 70 + 5252053637563917256893966150918698930726744782687970421882795126710194
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_95 :
Polynomial.coeff remainder4Coefficient0 95 = -(10623288182008538018950764289458 * 10 ^ 70 + 2680511849680788815987080183305030182321984418912169171700587559320275)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_96 :
Polynomial.coeff remainder4Coefficient0 96 = 11615761123617550949379524258951 * 10 ^ 70 + 7880995149843237303543704997412073003272616028623079441523364974052631
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_97 :
Polynomial.coeff remainder4Coefficient0 97 = -(12314749793561964620939811485050 * 10 ^ 70 + 2545943268794009388989703572599402961954287641389455918284558198443425)