Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1LeftPart0.Coefficients135To162

Recurrence 4 lookup certificate: Scalar1Left 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.recurrence4Scalar1Left_coeff_135 :
Polynomial.coeff recurrence4Scalar1Left 135 = -(((230957621458142933088808386290797939463050826354049388654 * 10 ^ 70 + 6186185123122204331584243070414394776414990363953408333385402838719969) * 10 ^ 70 + 3036398359322230819626690306898076961893128781840973394961172672571754) * 10 ^ 70 + 8082343089004018029087659060809547084413237741516711250412300924292991)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_136 :
Polynomial.coeff recurrence4Scalar1Left 136 = ((1305885587246631111664525721926236132945934089649064326486 * 10 ^ 70 + 2039338308394911311618938132016748399500317837132479020812442063913980) * 10 ^ 70 + 5244312942401052746326040882134444837903792049467462839265310473315554) * 10 ^ 70 + 8700926222847752584986928324836628446722601953291435934888414634317032
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_137 :
Polynomial.coeff recurrence4Scalar1Left 137 = -(((7246567143532433742291002529958417240811431214738650230824 * 10 ^ 70 + 7586929486905989430475411464251552148603488558702687236002735479063640) * 10 ^ 70 + 4598386549834817739960622707675886671814119423209703883689071770312476) * 10 ^ 70 + 9695732058912720511873459832424764671522321112952943390827333390351550)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_138 :
Polynomial.coeff recurrence4Scalar1Left 138 = ((39471422123477837227756848367768570976631748109463343824437 * 10 ^ 70 + 7623976770720330407088834248897095885235857573818738750399202199132442) * 10 ^ 70 + 9175645313439270123359122532777108464088636354694085542526156679039393) * 10 ^ 70 + 9751525819691938071595650407026855596294201102043114864171132600586175
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_139 :
Polynomial.coeff recurrence4Scalar1Left 139 = -(((211068477394068145201335917990235780962701742756185757339572 * 10 ^ 70 + 6210116991021289063557811027915826761784511472062592733911270909492305) * 10 ^ 70 + 4115475721753361424052085546373360933560734433556150405745484924040761) * 10 ^ 70 + 5793384683995923449795281582540360672250157650341448429071369041776038)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_140 :
Polynomial.coeff recurrence4Scalar1Left 140 = ((1108202395047440006986964287974530885550475448590885941212739 * 10 ^ 70 + 6647964515239709201609479291328908754435628812301887242549460817323806) * 10 ^ 70 + 8357685028716384396105576428053511575769313530647340001686943995910250) * 10 ^ 70 + 3125549513819604985669902169926263775201767193257958461272984095366608
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_141 :
Polynomial.coeff recurrence4Scalar1Left 141 = -(((5713904628745579487679880378653370690579722667581277769481000 * 10 ^ 70 + 2107084555043936216457602081016290478707187521134807767715897167021718) * 10 ^ 70 + 7577923332404685496596971814593054342570673533642860089911499084574205) * 10 ^ 70 + 1546884602230452653294762802553214219919361014729312094633859754991924)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_142 :
Polynomial.coeff recurrence4Scalar1Left 142 = ((28935192917495262722649811512245059555039439558953041554768845 * 10 ^ 70 + 9424786605040892914284566903250371540724921614294155951948914486607839) * 10 ^ 70 + 1460079470788775490300366721093587425052132773358695805140971065328013) * 10 ^ 70 + 1406169508639045197041270430415690759138307787499084653800020492171881
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_143 :
Polynomial.coeff recurrence4Scalar1Left 143 = -(((143932488174961270478544881182549441310327954436638380990806134 * 10 ^ 70 + 4624350111609449115579532657180148027647887506539819853131005863826140) * 10 ^ 70 + 1539168744434189141795854880018382607912636946322684784207428983738224) * 10 ^ 70 + 1217871795681462709661542979013418607458243470754097336298535246202252)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_144 :
Polynomial.coeff recurrence4Scalar1Left 144 = ((703377107665657374750520656955736560519087885586638954207180399 * 10 ^ 70 + 368719100433791274736913915003165974948543656350580699233105847261142) * 10 ^ 70 + 1539709072976292939995149949564844853269030967684313971901772260908048) * 10 ^ 70 + 1523267959009883751771142100270456748047320911392762656456598024619638
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_145 :
Polynomial.coeff recurrence4Scalar1Left 145 = -(((3377309344523401663786701520981810798711347744734241551753540277 * 10 ^ 70 + 8957010814979120685767647816291671050064954342291495397477804139769639) * 10 ^ 70 + 9642129291452390692006061683399237701205967643483707493525775137279099) * 10 ^ 70 + 9341178807045647488961017793904807973188966272105755812659269328515583)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_146 :
Polynomial.coeff recurrence4Scalar1Left 146 = ((15935341394096552146299900493446153239108982967401328701351865084 * 10 ^ 70 + 8693627957825815273674252891818377366814663493505768066362512292901594) * 10 ^ 70 + 9892627443520054489229291485337963663520244460011417213182549506413780) * 10 ^ 70 + 4494280286932599355252484480405385775305496066654320425595822037636760
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_147 :
Polynomial.coeff recurrence4Scalar1Left 147 = -(((73894651373416678683881211397959528346336996650033823645041323556 * 10 ^ 70 + 5370772859540863891406745742221514835888496374751688888503344009292636) * 10 ^ 70 + 6403205576056386847023482847206632226019434153753083872797712078396369) * 10 ^ 70 + 9256163730753095070241418309444079596888236369883484032188701019729766)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_148 :
Polynomial.coeff recurrence4Scalar1Left 148 = ((336804161931148420131586833911315848036549652301928724522864163409 * 10 ^ 70 + 3985863481735741119027499304633034603045944327108810639627045434193267) * 10 ^ 70 + 6808380569003805656034701073055723761773901215909321469291771715495301) * 10 ^ 70 + 4345382973190821802322088531780476339494667603864164478085207918403533
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_149 :
Polynomial.coeff recurrence4Scalar1Left 149 = -(((1509054720260841208263187787473781710677553240613316285979151733008 * 10 ^ 70 + 4364095839207659815100436651339291346055714811451666712666701791724773) * 10 ^ 70 + 690232480605690455529143479063826324972563328986142373798579700174849) * 10 ^ 70 + 7389841626661889935065914359455396696155174087721670251025678746555943)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_150 :
Polynomial.coeff recurrence4Scalar1Left 150 = ((6647288275614925320626216414137719142167393854878810043228616677496 * 10 ^ 70 + 1360130066434089777867590764691546671458874116101073002962780745874778) * 10 ^ 70 + 8948206810980498162635453760884451368822048136424553936914174765009060) * 10 ^ 70 + 5690223142803018246383251672461531674877719405759733935875881158565783
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_151 :
Polynomial.coeff recurrence4Scalar1Left 151 = -(((28790126248783433606524145756121366587494177432723155402748977105958 * 10 ^ 70 + 1494724753717649529803927807364370539221293130291807880031782330286375) * 10 ^ 70 + 4392197991623570186543050591384478763424803778018697637955247037140782) * 10 ^ 70 + 2134172104182089725678232243613376062200848474450193674497244905107460)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_152 :
Polynomial.coeff recurrence4Scalar1Left 152 = ((122616351217856780084763026543665285998430570631579741267111811155479 * 10 ^ 70 + 7493818085646216693077783306269043229268195971546670238482302513788678) * 10 ^ 70 + 34399598784700607843613487449538316808516364878775197576279761938643) * 10 ^ 70 + 9619206339622846039101404864517374095201315703289396235557731142381545
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_153 :
Polynomial.coeff recurrence4Scalar1Left 153 = -(((513575061846461407439514731207279549554656355659186499926850466038053 * 10 ^ 70 + 637647947531651381963642607165214524287709916470505964204353808178517) * 10 ^ 70 + 1491044139492316830112537063328169339984069195529430861880192312549660) * 10 ^ 70 + 4401316339682256266011063623110058484554790539396587046500665221130487)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_154 :
Polynomial.coeff recurrence4Scalar1Left 154 = ((2115699094989533225165478861583546909537321939865621631356731537201462 * 10 ^ 70 + 6191655394902801391793638496953571634800693465998600129966647168725898) * 10 ^ 70 + 6468815086407716599975943094194293533009665420986429559478361939871887) * 10 ^ 70 + 4818819344018549460644760216725868025405391482030393073211866037288257
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_155 :
Polynomial.coeff recurrence4Scalar1Left 155 = -(((8573157715465033042180239794756596250774418719755672785759979926660745 * 10 ^ 70 + 6051111755659961187590030982535822869950934246476187414335456685919625) * 10 ^ 70 + 3563609482355274962038260558053508539709121654472196233287489355294741) * 10 ^ 70 + 3630104818890341964500423741313522401828606468182916680644315213084489)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_156 :
Polynomial.coeff recurrence4Scalar1Left 156 = (((3 * 10 ^ 70 + 4174800922734981182965463450735471776805296053441893751308003716819026) * 10 ^ 70 + 5474295502728210318866366456314982787759068644793513876753793040462671) * 10 ^ 70 + 1937460715867705960172304585509997810698850599888470333062833476948166) * 10 ^ 70 + 8751146924034491321392950273920409981921977937305355211054346960174327
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_157 :
Polynomial.coeff recurrence4Scalar1Left 157 = -((((13 * 10 ^ 70 + 4026173858778127588761980981574403366284862594866075354133606495674612) * 10 ^ 70 + 3172283854523659335376845722457755566500936925999046079265860582650222) * 10 ^ 70 + 8167432739138624529723963619679060814507415965964755014356715021187815) * 10 ^ 70 + 3693126540558433362953535160300824351735073162889594247005260485409478)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_158 :
Polynomial.coeff recurrence4Scalar1Left 158 = (((51 * 10 ^ 70 + 7166936328631962922708342752439466420729432430051665559925976502627964) * 10 ^ 70 + 1026522102086042207219422163685795682642144598002203006596680901571580) * 10 ^ 70 + 3955639605157031808355620522813620373025171224562947572424656352854885) * 10 ^ 70 + 889634079686815127019649975942196563689124972887540949333123086590920
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_159 :
Polynomial.coeff recurrence4Scalar1Left 159 = -((((196 * 10 ^ 70 + 3664807839383566866539888602367568308140981094587611475773773799724209) * 10 ^ 70 + 5201455631795481236369835759205044187255448445185228493473350033753577) * 10 ^ 70 + 4924263176646624013656637084150383017588825502364581795488243396531328) * 10 ^ 70 + 2699308228407021637338368529969161575771804140567082319741558854943731)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_160 :
Polynomial.coeff recurrence4Scalar1Left 160 = (((733 * 10 ^ 70 + 7301031123220794522986366477019237897598305365485907893024029835872056) * 10 ^ 70 + 627348515824885590022455673822888456550941776212385587543911682181532) * 10 ^ 70 + 9724442063468040282407289710674440584096900918787203333967780506631034) * 10 ^ 70 + 3254088603400413924567211762875668142709611665979742797257663351117083
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_161 :
Polynomial.coeff recurrence4Scalar1Left 161 = -((((2698 * 10 ^ 70 + 1963799780767528004897909398985686593249658446515735058012099542678176) * 10 ^ 70 + 7177136355199734052016703610812792032559515952513718129203553113160546) * 10 ^ 70 + 8577146315254621348328623077639921995550893592433708962533024370488360) * 10 ^ 70 + 9344502120157696401102763121573963063662334789747510607889702104606259)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_162 :
Polynomial.coeff recurrence4Scalar1Left 162 = (((9765 * 10 ^ 70 + 9356167476377851770820528171046157378007860059686520229685329202770280) * 10 ^ 70 + 5536992070057220132941370990691628345360557054557096736194136207860322) * 10 ^ 70 + 5258075204680635428809434206875360895680146121963255727510200588341087) * 10 ^ 70 + 9904303404972139596744935386496663529035057748446106311019740896593142