Recurrence 2 lookup certificate: Scalar1Shift coefficient convolution #
This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_92 :
Polynomial.coeff recurrence2Scalar1Shift 92 = -((1451997 * 10 ^ 70 + 4398548908494021534384444623809363487422606982348111613057213605645487) * 10 ^ 70 + 6794328762429849053561434626414952700354871544600814425319877245324938)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_93 :
Polynomial.coeff recurrence2Scalar1Shift 93 = (6799411 * 10 ^ 70 + 3330144005163362377417756100280565572553719542220554199608393628816124) * 10 ^ 70 + 7216082544411951851202378240147394635073930298156983561417571653451396
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_94 :
Polynomial.coeff recurrence2Scalar1Shift 94 = -((30610358 * 10 ^ 70 + 6571956714602526691549735553815811323808441345327174049973894195029650) * 10 ^ 70 + 2309981055555251488819650490462645416723454661650931604394989425635766)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_95 :
Polynomial.coeff recurrence2Scalar1Shift 95 = (132284928 * 10 ^ 70 + 9596718529236243766972080232782735332279912389066026763341173167115722) * 10 ^ 70 + 693875858657572237969267013873249086070584776757701276526290947896473
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_96 :
Polynomial.coeff recurrence2Scalar1Shift 96 = -((547640838 * 10 ^ 70 + 544732517087077487427788723416142705616726418184659851743851556356731) * 10 ^ 70 + 6054401350773017058542049125907460326905667413505459700978138056652825)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_97 :
Polynomial.coeff recurrence2Scalar1Shift 97 = (2166385111 * 10 ^ 70 + 8042603644074078134166522768373392476525080053949593950804813150051823) * 10 ^ 70 + 3633344612381209507497735436930085470653980346654123769789213114405778
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_98 :
Polynomial.coeff recurrence2Scalar1Shift 98 = -((8166365327 * 10 ^ 70 + 1378507047584990868730449474990982067202742218220727669939189442590554) * 10 ^ 70 + 6098257837904697283938073780100466966432669829226837302119767659143304)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_99 :
Polynomial.coeff recurrence2Scalar1Shift 99 = (29240403716 * 10 ^ 70 + 7770549406675395882169984377354937998907166203475477736353916790391220) * 10 ^ 70 + 3781912835043890653405249808923840337765045592281744172414059412079179
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_100 :
Polynomial.coeff recurrence2Scalar1Shift 100 = -((98957608475 * 10 ^ 70 + 1568886910989372146316349538425428421575907487645861928972692199894747) * 10 ^ 70 + 9192287232234717861245840764856416990039740815156694323206778053271339)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_101 :
Polynomial.coeff recurrence2Scalar1Shift 101 = (313226212363 * 10 ^ 70 + 2966057663349874423927735439610734130088054840118914807369652203523355) * 10 ^ 70 + 3267269080410976683184840542881288454507269876720607900911174263550027
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_102 :
Polynomial.coeff recurrence2Scalar1Shift 102 = -((904087163858 * 10 ^ 70 + 4465625880615351091008149376594267747105622394089850921256797547241528) * 10 ^ 70 + 6311355605943005784218755578979208006792689055014174792838027512874145)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_103 :
Polynomial.coeff recurrence2Scalar1Shift 103 = (2228923234140 * 10 ^ 70 + 9495147304025455585765011644050138363160214791253966113750931535510884) * 10 ^ 70 + 2565758326010184522463657042915574720592074715832236269358379287815450
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_104 :
Polynomial.coeff recurrence2Scalar1Shift 104 = -((3747529266135 * 10 ^ 70 + 602983601610667259879974685238620198551244486054482610863928207215983) * 10 ^ 70 + 6559294789969998926543641951811319756472454384917464445012465070708908)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_105 :
Polynomial.coeff recurrence2Scalar1Shift 105 = -((2335843247938 * 10 ^ 70 + 9434652438604794242468972253170337395133168893981367973391243120293167) * 10 ^ 70 + 1537360853464236648830428684786707414091790719706507844015099815915490)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_106 :
Polynomial.coeff recurrence2Scalar1Shift 106 = (57266112503370 * 10 ^ 70 + 9691368597031589513544373518130999056220002268021256968777491444303076) * 10 ^ 70 + 4800600479730960499975667621282376585730576062433196704142408347836292
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_107 :
Polynomial.coeff recurrence2Scalar1Shift 107 = -((315446315670737 * 10 ^ 70 + 9567483376825740758555964023556599537731800599905013304598605974024784) * 10 ^ 70 + 1418184871678136647581355087662507829938485242546673865201015292120251)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_108 :
Polynomial.coeff recurrence2Scalar1Shift 108 = (1222241170663195 * 10 ^ 70 + 549700776141098076776943479063714127917597642509714909057816389535652) * 10 ^ 70 + 1998282885686938753553824787955790415805480055103615301626086881405719
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_109 :
Polynomial.coeff recurrence2Scalar1Shift 109 = -((3854002500506184 * 10 ^ 70 + 7632536773881844611067177056150013803561192196273699368855940823639931) * 10 ^ 70 + 66962790544456548364719821810812367603677066545523516163830624198782)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_110 :
Polynomial.coeff recurrence2Scalar1Shift 110 = (11469577877298175 * 10 ^ 70 + 511336586383305254482526735184555513038161592014230892448376203690707) * 10 ^ 70 + 8668156322470748965511932494039299706562933868372892576605032771917270
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_111 :
Polynomial.coeff recurrence2Scalar1Shift 111 = -((42573573053180606 * 10 ^ 70 + 4112167809481008665175647167820952230897965130890339526666454987854799) * 10 ^ 70 + 8605077345892666414958426940230898175721197038494372062780055553973196)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_112 :
Polynomial.coeff recurrence2Scalar1Shift 112 = (215058905187210283 * 10 ^ 70 + 7733293231636087297163062659087748103660479996557976196292977842570001) * 10 ^ 70 + 2240280018062099542057937765395060387980768625086896607137603729078459
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_113 :
Polynomial.coeff recurrence2Scalar1Shift 113 = -((1110231886146950343 * 10 ^ 70 + 4398610096748780974928907809054134846540886494626839050110271256162402) * 10 ^ 70 + 4576267775643276850070440379105656898072684025780696937994973511611385)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_114 :
Polynomial.coeff recurrence2Scalar1Shift 114 = (4578912041511971572 * 10 ^ 70 + 2582412658622681987678009712087615979141018029632442085705965612540266) * 10 ^ 70 + 2989234066351841133795185019369068932869410014481388926230161116316446
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_115 :
Polynomial.coeff recurrence2Scalar1Shift 115 = -((11690424970296180441 * 10 ^ 70 + 7686929997028907031613533200091386261868004725961826653733193857926515) * 10 ^ 70 + 3051768664397982726056983745549491058190755408287866149446841884983694)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_116 :
Polynomial.coeff recurrence2Scalar1Shift 116 = -((6267938745199328500 * 10 ^ 70 + 2057725279753823493123878350009475224790072287145348487614509347737824) * 10 ^ 70 + 3562261853430134200207493144415940823127641457885150851159300761828962)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_117 :
Polynomial.coeff recurrence2Scalar1Shift 117 = (246019974802014982550 * 10 ^ 70 + 146481168759269786327246000327126462981995235568921825456617277950075) * 10 ^ 70 + 9376100424628956324037044840100567371552825263777165563532242397028006
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_118 :
Polynomial.coeff recurrence2Scalar1Shift 118 = -((1361181933419323173137 * 10 ^ 70 + 730468335878609284644558212511920193585871811471293092266199881550764) * 10 ^ 70 + 3244040813408453621011003627122168280120846654735205954719634030419828)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_119 :
Polynomial.coeff recurrence2Scalar1Shift 119 = (3744110856050672450493 * 10 ^ 70 + 818777427373720693092262710923859948582105615460975678792748655223547) * 10 ^ 70 + 719655471471368657932093913403889634604334508288534452527791777388428
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_120 :
Polynomial.coeff recurrence2Scalar1Shift 120 = (1106507744134741454055 * 10 ^ 70 + 1349583227441607753741732943063268599519904356927404010172538331533371) * 10 ^ 70 + 9799663197225292479070043454204950005787131169614917548335415950529624
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_121 :
Polynomial.coeff recurrence2Scalar1Shift 121 = -((66932990277988467052704 * 10 ^ 70 + 9871548065955543374138210610804474660315223493994507187235494242724988) * 10 ^ 70 + 8711146877043089138827754082835857848855374470805445962991121919940730)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_122 :
Polynomial.coeff recurrence2Scalar1Shift 122 = (368370309155950935349325 * 10 ^ 70 + 7728700381076253667990688312088278293607154642356348877523265437519861) * 10 ^ 70 + 3239120251766289958143628376809931035215172533681351108468972513127036
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_123 :
Polynomial.coeff recurrence2Scalar1Shift 123 = -((1125287765347765117456369 * 10 ^ 70 + 4312275351821486148139014527396494969100043563166708684888506091175902) * 10 ^ 70 + 7443482926032597361749429343146342148937335564648412948469228203882437)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_124 :
Polynomial.coeff recurrence2Scalar1Shift 124 = (1126268980188048899661833 * 10 ^ 70 + 38420479297862428902591978860276860981842411926439558920579654562630) * 10 ^ 70 + 6283580255098380942350413552011474282982101874119127206293781323154091
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_125 :
Polynomial.coeff recurrence2Scalar1Shift 125 = (10257345217649689498314753 * 10 ^ 70 + 50582448219316117661372305589334878578273537615341526455149445392902) * 10 ^ 70 + 8437761071046304105825706523399787045591956658268708008812349988833171
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_126 :
Polynomial.coeff recurrence2Scalar1Shift 126 = -((80497864512720554306525465 * 10 ^ 70 + 5224741640439317889307427366000623871362210576298114838158619869590806) * 10 ^ 70 + 4319632169205973789099277713288579168550014721955731084153116838450424)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_127 :
Polynomial.coeff recurrence2Scalar1Shift 127 = (331041432225520638251970768 * 10 ^ 70 + 7912518633463427463281463616753214026860297957121683337948674846218779) * 10 ^ 70 + 372027849174816053989057136250504621135492914986579242037080597842928
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_128 :
Polynomial.coeff recurrence2Scalar1Shift 128 = -((715163518158036124319752832 * 10 ^ 70 + 7519774821480211387909498503018701944812191658136688112172873283321748) * 10 ^ 70 + 7153149875066672481922115231169078238064382308517364345746227280102383)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_129 :
Polynomial.coeff recurrence2Scalar1Shift 129 = -((835434174283137432488343193 * 10 ^ 70 + 445844464113391280877793824681725500993801371917350968244940575544112) * 10 ^ 70 + 7113014952672510543831454291715485767303289827149772998317426663867288)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_130 :
Polynomial.coeff recurrence2Scalar1Shift 130 = (13543639959294569738160756276 * 10 ^ 70 + 6184305468856247364674852844453605772386944961875696215449469658460385) * 10 ^ 70 + 8385863418621928494609876501027649661748774831751316719169597179850492
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_131 :
Polynomial.coeff recurrence2Scalar1Shift 131 = -((51077990391366724495825390856 * 10 ^ 70 + 4846546978277681967748594511386383273980165131413943761244608913251509) * 10 ^ 70 + 6364156487286396086227502961529519093319946207004269906231727182425418)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_132 :
Polynomial.coeff recurrence2Scalar1Shift 132 = (71358608537557488790685649835 * 10 ^ 70 + 299431931140737819289343349321257107986921963026896455547636871690222) * 10 ^ 70 + 560845606824140220132960732248989084919402490169008674183090470122083
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_133 :
Polynomial.coeff recurrence2Scalar1Shift 133 = (77932576260329938820607988282 * 10 ^ 70 + 2786874291012368138953016687899542459102086972846999509023383267887349) * 10 ^ 70 + 2503244036639351930861975969830245060481767737296806073166288039611590
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_134 :
Polynomial.coeff recurrence2Scalar1Shift 134 = (356864810624574323932437137918 * 10 ^ 70 + 9733441442285804207446916015307161068711513946387520999960408390052079) * 10 ^ 70 + 2480067267295300931793350843964398102024418146024173730617608717697956
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_135 :
Polynomial.coeff recurrence2Scalar1Shift 135 = -((6864289430779536014953056497142 * 10 ^ 70 + 2563318533377598110052185901385215190972176873784736850317206750200462) * 10 ^ 70 + 8389008914019662886065870554958361069028722742554993572851219566695067)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_136 :
Polynomial.coeff recurrence2Scalar1Shift 136 = (18784300281694937387659747677073 * 10 ^ 70 + 8231867547854190482713069153909740980429680191683896933413222772779402) * 10 ^ 70 + 9394542011273766365629996552267679044168455007691223025677100695860400
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_137 :
Polynomial.coeff recurrence2Scalar1Shift 137 = (106943071162819328694161065393965 * 10 ^ 70 + 3716374472995497559164677553326562689134072198588136747233382843761779) * 10 ^ 70 + 7207739756975474164574346100101929905054781314167846881782005604533019
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_138 :
Polynomial.coeff recurrence2Scalar1Shift 138 = -((1055514723677548783927262738496647 * 10 ^ 70 + 5977300495419592252641919285334646805624902021267894865199248668242669) * 10 ^ 70 + 6816454220968776280107905473870616638549703492368209312476095748895750)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_139 :
Polynomial.coeff recurrence2Scalar1Shift 139 = (3365548612531011313458116509900139 * 10 ^ 70 + 527948166879241853502492280032313836965160446245781249372022582418476) * 10 ^ 70 + 1820286785121438689095969034754040654960256714421084627455120526479798
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_140 :
Polynomial.coeff recurrence2Scalar1Shift 140 = (1979946697721656440965277452607914 * 10 ^ 70 + 7958939825014479409816931347807952851057087710809096347932418713335757) * 10 ^ 70 + 9028912498954797081202038978337516755630912814018032343237071767842326
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_141 :
Polynomial.coeff recurrence2Scalar1Shift 141 = -((60255272430276269558545368782646335 * 10 ^ 70 + 3055417486853073197143020646405484233218715334539608512994593117829969) * 10 ^ 70 + 8722896334538657407987507277291525276395721665647015365752202558038636)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_142 :
Polynomial.coeff recurrence2Scalar1Shift 142 = (216362848521794426597593224899254110 * 10 ^ 70 + 5892447177598909721111781388869788927177235290321638145953515280335760) * 10 ^ 70 + 288432346545850235929326570536973853139619848682323893467998916356275
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_143 :
Polynomial.coeff recurrence2Scalar1Shift 143 = -((1585636123695715718619376617068871 * 10 ^ 70 + 5660587061125081404067989887810250897521213471684532083372707776075557) * 10 ^ 70 + 2239612352415920536428557780968707352588490153539600919253501774760826)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_144 :
Polynomial.coeff recurrence2Scalar1Shift 144 = -((2884027893057669051477861938597859450 * 10 ^ 70 + 2152036978502844563941889316774885502490893440637886450231349760689876) * 10 ^ 70 + 621439318756207790296467147724120947136622972119682771886539849305102)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_145 :
Polynomial.coeff recurrence2Scalar1Shift 145 = (10122438055779914415031797231606787771 * 10 ^ 70 + 3289028075157900737164693888990364921563538562158172423715486538495296) * 10 ^ 70 + 3932065955317403957436070578553338414154306001050785032453708385473838
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_146 :
Polynomial.coeff recurrence2Scalar1Shift 146 = (3715368566491658818855728175777934181 * 10 ^ 70 + 5073330202408980522425314166489058978986122731768535103065834805207614) * 10 ^ 70 + 1295130349398483365510246366201084098796579519141990862257418810132733
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_147 :
Polynomial.coeff recurrence2Scalar1Shift 147 = -((149969431779396145123878755953368372551 * 10 ^ 70 + 6911210905028671826452732551599446205449662512112996829010623869145033) * 10 ^ 70 + 2477309660578302371001896041572274377286322271870709451184259786367707)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_148 :
Polynomial.coeff recurrence2Scalar1Shift 148 = (476190878200581163417639713543955090219 * 10 ^ 70 + 4755226333324277800582552611753601001981446042509630293659683787289559) * 10 ^ 70 + 9944188695080332677552205907116667244981842615188162796015403665994856
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_149 :
Polynomial.coeff recurrence2Scalar1Shift 149 = (323994943227364457659596897693063286725 * 10 ^ 70 + 9986882100549873382126430610667443070167930471615886552876345791191197) * 10 ^ 70 + 517163354179411673972038635355512755245590308639992695224632461331325
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_150 :
Polynomial.coeff recurrence2Scalar1Shift 150 = -((7410503083732124236557560355926716386934 * 10 ^ 70 + 959999302722949608447779019635716502416978703888907879665162809608788) * 10 ^ 70 + 3874502265233934862723568545463397942612641593757425766279075150446304)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_151 :
Polynomial.coeff recurrence2Scalar1Shift 151 = (21826482473566664932364807726249881361712 * 10 ^ 70 + 1589666442831068448254732350274383922807145860239118086099979615288565) * 10 ^ 70 + 785552388887661960926950617069523781509200419576959354112170534771807
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_152 :
Polynomial.coeff recurrence2Scalar1Shift 152 = (18806813619352429909729671846047153817755 * 10 ^ 70 + 4244042264965612184379679336701542847967708932159264773620788868218932) * 10 ^ 70 + 4415388754232545014374676248225669495367005255502528399992584470217136
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_153 :
Polynomial.coeff recurrence2Scalar1Shift 153 = -((345143834050133398628171443640426474864274 * 10 ^ 70 + 2476919979026715075456302028436905487787091629074863878633889394646290) * 10 ^ 70 + 5574698316254213541669663844515234604418068218794699310815099398893541)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_154 :
Polynomial.coeff recurrence2Scalar1Shift 154 = (979657012875872484446286038214742266703822 * 10 ^ 70 + 2461349911889677524114229381798300705178617928874446105231640668831412) * 10 ^ 70 + 1073923701610794940234547233518918840058232660810553651320188899240713