Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1SecondPart0.Coefficients0To42

Recurrence 4 lookup certificate: Scalar1Second coefficient convolution #

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_0 :
Polynomial.coeff recurrence4Scalar1Second 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_1 :
Polynomial.coeff recurrence4Scalar1Second 1 = -23258498993769499515486843778796935654080512
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_2 :
Polynomial.coeff recurrence4Scalar1Second 2 = 43343313797901907018939542499351105956102348800
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_3 :
Polynomial.coeff recurrence4Scalar1Second 3 = 796597013113031302361269243973936816112924614245504
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_4 :
Polynomial.coeff recurrence4Scalar1Second 4 = -3922660850047364316643640564165730230850625169062068384
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_5 :
Polynomial.coeff recurrence4Scalar1Second 5 = 8629628332779613448579122407978770435762855384161926343072
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_6 :
Polynomial.coeff recurrence4Scalar1Second 6 = -11198717867188625909517053141347385330792438431788356252516968
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_7 :
Polynomial.coeff recurrence4Scalar1Second 7 = 9105915855745081354232097627611180923714547852947266504964234368
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_8 :
Polynomial.coeff recurrence4Scalar1Second 8 = -4233315028703934316901376589418998724620202660473017114961692280080
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_9 :
Polynomial.coeff recurrence4Scalar1Second 9 = 339148560301988707501224831380727688080114693939942651697981818909992
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_10 :
Polynomial.coeff recurrence4Scalar1Second 10 = 92 * 10 ^ 70 + 5461615694163654284441100063810557462543812386493163732144891339761352
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_11 :
Polynomial.coeff recurrence4Scalar1Second 11 = -(60007 * 10 ^ 70 + 7296035836807923124828322872795499023111959981741561812985104272439980)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_12 :
Polynomial.coeff recurrence4Scalar1Second 12 = 6373948 * 10 ^ 70 + 167943696378537555737891554122516745342987878920722647867687272271236
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_13 :
Polynomial.coeff recurrence4Scalar1Second 13 = 14143561579 * 10 ^ 70 + 78114755590490924122292716303587061586468721244704989027444397476622
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_14 :
Polynomial.coeff recurrence4Scalar1Second 14 = -(10715051710589 * 10 ^ 70 + 2410454001469608552169500898183886889711982793467374231576783592994394)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_15 :
Polynomial.coeff recurrence4Scalar1Second 15 = 3457874017127725 * 10 ^ 70 + 3738250729115014501882085716661963447779846883062901610874217556535156
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_16 :
Polynomial.coeff recurrence4Scalar1Second 16 = -(78952199732126044 * 10 ^ 70 + 8126084039860486055430307372784442522255385782338054128797334892263110)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_17 :
Polynomial.coeff recurrence4Scalar1Second 17 = -(418384238643930457685 * 10 ^ 70 + 8224586052848214960997116935261680137081466458699440392680330997649000)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_18 :
Polynomial.coeff recurrence4Scalar1Second 18 = 164338580131879063266575 * 10 ^ 70 + 232038197382250709606870028695162184568311083484554631453828452409057
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_19 :
Polynomial.coeff recurrence4Scalar1Second 19 = 255419694450834122595886 * 10 ^ 70 + 7094315998870935160539476233467841448694934178345524435934353663521146
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_20 :
Polynomial.coeff recurrence4Scalar1Second 20 = -(28724500340295172723213284655 * 10 ^ 70 + 3060739998792037546276316163260642967232584940785252394615439289663161)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_21 :
Polynomial.coeff recurrence4Scalar1Second 21 = 16201389799189513301481550840285 * 10 ^ 70 + 5327067933749524782024727463677977945190493617685600301817758956676013
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_22 :
Polynomial.coeff recurrence4Scalar1Second 22 = -(5498464001908456301952592294634542 * 10 ^ 70 + 513368429014424606339040576805966506316858837716049438602925999737205)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_23 :
Polynomial.coeff recurrence4Scalar1Second 23 = 1327790307220918242304386687329358709 * 10 ^ 70 + 7065162077634345582460492223723753016587105423146823739103707609579207
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_24 :
Polynomial.coeff recurrence4Scalar1Second 24 = -(233669642040000239752510547829835243965 * 10 ^ 70 + 6684721157230454052218714618864769294225871535022409935566672541693116)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_25 :
Polynomial.coeff recurrence4Scalar1Second 25 = 27169623390358290231678160941600571464806 * 10 ^ 70 + 1019318360619824668961194962513231974589930252909958525583506512912119
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_26 :
Polynomial.coeff recurrence4Scalar1Second 26 = -(509497992788664404885190792510403617236057 * 10 ^ 70 + 690776184265672912249546825546606741884443035476320300665474010879825)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_27 :
Polynomial.coeff recurrence4Scalar1Second 27 = -(827204639002434422403624426038237894797020099 * 10 ^ 70 + 7547270687262527342452132450454657024885375737541838636359032520013734)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_28 :
Polynomial.coeff recurrence4Scalar1Second 28 = 330728999718793919558036573691826458104195608123 * 10 ^ 70 + 729837500106668071642770887982763320654898339937027444901429213241086
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_29 :
Polynomial.coeff recurrence4Scalar1Second 29 = -(96913528217298798485252249105455410780076491239079 * 10 ^ 70 + 4658487137992241157582182615006278992174368756156651759593389733151452)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_30 :
Polynomial.coeff recurrence4Scalar1Second 30 = 24703552422366824045958441724750343720424124460911411 * 10 ^ 70 + 5717371477819386348980609126388792325092401721159969217339067753107527
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_31 :
Polynomial.coeff recurrence4Scalar1Second 31 = -(5567922160777240612024869251806276424944154059688496221 * 10 ^ 70 + 1375903069155677863846579537202812158706831305317917540671188257795667)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_32 :
Polynomial.coeff recurrence4Scalar1Second 32 = 1100611286117814183351360718204609957344575312064278222814 * 10 ^ 70 + 462996910090575003768419274527639040746470279821772409224477019124982
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_33 :
Polynomial.coeff recurrence4Scalar1Second 33 = -(189105106315087707807414363115397346596869051863459773211006 * 10 ^ 70 + 8676472136776161698934869867929676648501975176027625408029837675709370)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_34 :
Polynomial.coeff recurrence4Scalar1Second 34 = 27941247037242231791573673887983842731517305096099934571899850 * 10 ^ 70 + 7048949741234522462899232726753255443314358697018140131793220413297616
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_35 :
Polynomial.coeff recurrence4Scalar1Second 35 = -(3474627229158903459562894486110169773301032506810156281741548701 * 10 ^ 70 + 4739041949271994557907141551814254680319409319751136423958118656284094)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_36 :
Polynomial.coeff recurrence4Scalar1Second 36 = 343823498238018294142636579208666831870372227239892821029467225400 * 10 ^ 70 + 8571518117031868299680930868132375247707182781415750129916178900430194
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_37 :
Polynomial.coeff recurrence4Scalar1Second 37 = -(22037786149526422758256845730808790839495396525607827596966076393097 * 10 ^ 70 + 5856383215275812040229624263259492809931748845363236292288360980450493)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_38 :
Polynomial.coeff recurrence4Scalar1Second 38 = -(440875861552979054781595186611970014021216969867033210446120243276461 * 10 ^ 70 + 6220705092555797675672563592884002158966099797971758497548978319459956)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_39 :
Polynomial.coeff recurrence4Scalar1Second 39 = (42 * 10 ^ 70 + 2680529105777972016788837601100053055671964557958456961158411611822837) * 10 ^ 70 + 5036530181217493538682918768511384347298208622791157768164521575490899
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_40 :
Polynomial.coeff recurrence4Scalar1Second 40 = -((8379 * 10 ^ 70 + 943226556339050985571177308525741722752672810969093410255224603788549) * 10 ^ 70 + 4755132181961535622475276186766633509497791877933799323559104083904774)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_41 :
Polynomial.coeff recurrence4Scalar1Second 41 = (1183985 * 10 ^ 70 + 1862418431534282183801819317178978587395675367912189150704076422004818) * 10 ^ 70 + 9260661108304850873176546808403734310113429783634871279248098356212467
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_42 :
Polynomial.coeff recurrence4Scalar1Second 42 = -((136587737 * 10 ^ 70 + 1079656294665858199465814854359055763946277051851989773255624190591066) * 10 ^ 70 + 8898267274830768364787578500478516831921538704839989463023593312110186)