Recurrence 2 lookup certificate: Scalar1Exceptional 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.recurrence2Scalar1Exceptional_coeff_202 :
Polynomial.coeff recurrence2Scalar1Exceptional 202 = -((347285515127189673730330867788022790042024976237012248592565 * 10 ^ 70 + 2434037241101567341943332950336106897044268946468237684776653146429138) * 10 ^ 70 + 6868137392431627305076480818037216334304181115256593260064474434014139)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_203 :
Polynomial.coeff recurrence2Scalar1Exceptional 203 = (1054330077549446814495652167252447988748891158299243187434561 * 10 ^ 70 + 1977583970167663681078211485013823221758735974776377703166794987910157) * 10 ^ 70 + 5909914192504621111991557386395785106239921322612547930948569175695974
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_204 :
Polynomial.coeff recurrence2Scalar1Exceptional 204 = -((2140396204087968108281405976792218764881073246786400767337432 * 10 ^ 70 + 3081904788802057690765524873406756245076676388460144595994876901540435) * 10 ^ 70 + 9243509713874240803734702170345991351874102409138064470391004782958072)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_205 :
Polynomial.coeff recurrence2Scalar1Exceptional 205 = (3612594425359125471305017897503030455614881325201327612030484 * 10 ^ 70 + 9236400195194158703402704418129498962393364245522687128554633619655880) * 10 ^ 70 + 7720790832566518143272033095512915049979438135440313533958991527244499
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_206 :
Polynomial.coeff recurrence2Scalar1Exceptional 206 = -((5384204818240592054503770542341206838824270707702916711791579 * 10 ^ 70 + 3117596255843540594924630283988703674415746703637467989605435677672021) * 10 ^ 70 + 7751944908632780809495310032421727380310962361716713789456097574079757)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_207 :
Polynomial.coeff recurrence2Scalar1Exceptional 207 = (7249905860939925211175465070270563359114569485219306481675121 * 10 ^ 70 + 3745985092165346441027831242886824015927824396578537618766759111457942) * 10 ^ 70 + 8821947342152062942561968102600469710269345181874257385875428295795550
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_208 :
Polynomial.coeff recurrence2Scalar1Exceptional 208 = -((8885137734617266667087233912557884620642893436338514805807703 * 10 ^ 70 + 3109889262601338422281725328223967043628708400904884978149206504677056) * 10 ^ 70 + 4098439058619138863163019088851048271985184126931803415183618103277955)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_209 :
Polynomial.coeff recurrence2Scalar1Exceptional 209 = (9880158164597627356111020066315389815715663270631170566017834 * 10 ^ 70 + 5451341300850460841511047523221455812851181815039305064342077739026912) * 10 ^ 70 + 8766942708108193422631967718345606913301904084620085625908484883902671
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_210 :
Polynomial.coeff recurrence2Scalar1Exceptional 210 = -((9811421149857523712055342757761654440818608283995678386312077 * 10 ^ 70 + 8427526048226834186178988917998458354354562096075478827334579159063827) * 10 ^ 70 + 4721739363790370320725217941823594768837137420075270534843236411068385)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_211 :
Polynomial.coeff recurrence2Scalar1Exceptional 211 = (8341132044631744423014188472754781860692469586266678857815745 * 10 ^ 70 + 9064428172489291457210090895614021543100328986295861063421618587979885) * 10 ^ 70 + 9890220841459782794000047118141936213862254831713382260777756153389099
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_212 :
Polynomial.coeff recurrence2Scalar1Exceptional 212 = -((5323537619518219233136286587291621794606823084229158750801749 * 10 ^ 70 + 1051039893870346153537950445588278581927304646779869497966837106900040) * 10 ^ 70 + 2284731023913845795701080817181204964352364301639431205554023306036098)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_213 :
Polynomial.coeff recurrence2Scalar1Exceptional 213 = (888272835659897560374579552247480916506555026601730921762746 * 10 ^ 70 + 7473491499027428521464537790405022832498888035228599795727342516365938) * 10 ^ 70 + 5534445670307963638065388293029816704228258044336433256299702565108389
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_214 :
Polynomial.coeff recurrence2Scalar1Exceptional 214 = (4528900246113885002871224992952988683318756898520448698079419 * 10 ^ 70 + 8527330450132906812369999591242793363074273829773981513563247067822775) * 10 ^ 70 + 3164433744304573882516797715557429079908266604037084556228216571639012
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_215 :
Polynomial.coeff recurrence2Scalar1Exceptional 215 = -((10227436991193735904730650110762133839757136931901129541852092 * 10 ^ 70 + 3630739494064143666841274787082860148242972840839384068339649792073097) * 10 ^ 70 + 6619724798082383477934705064676424331513729700678890208989632767476041)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_216 :
Polynomial.coeff recurrence2Scalar1Exceptional 216 = (15356206097807012674892159620491272841612717363562164263343966 * 10 ^ 70 + 5061177840277125919233188213924268693663943451955373148891353008311382) * 10 ^ 70 + 121561745906234362368347652771601509901278116698288458338504580626450
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_217 :
Polynomial.coeff recurrence2Scalar1Exceptional 217 = -((19079325573384746415911275163672754131240598983270783902419453 * 10 ^ 70 + 3954018617958694747180346841657078798793535366339839175972974360483644) * 10 ^ 70 + 4471787657545832616296540729854912823770746085260630891178892823214398)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_218 :
Polynomial.coeff recurrence2Scalar1Exceptional 218 = (20754471620052314415375195753814833378410407880742494953456442 * 10 ^ 70 + 1294940945742094133393956655809555168570900911268442633354847938709708) * 10 ^ 70 + 7183918033042075901865714046763568841753748251290861832744136048040341
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_219 :
Polynomial.coeff recurrence2Scalar1Exceptional 219 = -((20077262452557842118399581824426384071458365441118429983268192 * 10 ^ 70 + 4014434436248556716460755243294459919489708048549400811833758270589139) * 10 ^ 70 + 2198825555121863432588108823513055913754808087144191919600920029424489)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_220 :
Polynomial.coeff recurrence2Scalar1Exceptional 220 = (17152213360587465309018960020727173513163571325271838592630971 * 10 ^ 70 + 4880779003417434143229094620810969353988124400211750242463978178801508) * 10 ^ 70 + 9456075499990520220831007187217514564396122415532052332070389436501752
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_221 :
Polynomial.coeff recurrence2Scalar1Exceptional 221 = -((12470284590133145682437257312622989527887873149136925248452267 * 10 ^ 70 + 5689478614824748493037299414542453171835489436129825940223305147551840) * 10 ^ 70 + 5875658869760810876218728913653297188435354384265321945563487883018610)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_222 :
Polynomial.coeff recurrence2Scalar1Exceptional 222 = (6799111530766476086039006160335400875133298194045517404368922 * 10 ^ 70 + 762548572557924442773360659079191742128666584623959817199631532076049) * 10 ^ 70 + 8740318505864198267898819439455395511553071380836870054855424854011506
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_223 :
Polynomial.coeff recurrence2Scalar1Exceptional 223 = -((1016099539994860607484980764851600074580227907014998196703395 * 10 ^ 70 + 5918974278008917830487596249269022018844666558221848213619142058743703) * 10 ^ 70 + 7283441302594406379074619409922996616714431099199504404562449573911045)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_224 :
Polynomial.coeff recurrence2Scalar1Exceptional 224 = -((4071094537422733494760596813980005415875087118444053486991048 * 10 ^ 70 + 6501439783001669400015045277584179417209158742770091307402308258741165) * 10 ^ 70 + 2812509490523038663347607751502016899244885718982173590410530090226963)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_225 :
Polynomial.coeff recurrence2Scalar1Exceptional 225 = (7871766926660933174292549748040566804358320684854587318163641 * 10 ^ 70 + 6535674023575507538542402779939672791917849943274058811533667152560469) * 10 ^ 70 + 8951044640980592265292387819373442725978000747841490769565133781562706
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_226 :
Polynomial.coeff recurrence2Scalar1Exceptional 226 = -((10094870329833360266158118830755323466679884656197720826852155 * 10 ^ 70 + 1890794698351245540448804395659422207856958635574524695924640326243877) * 10 ^ 70 + 9723006999710894296218050020631495217104888781697909124987206461715313)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_227 :
Polynomial.coeff recurrence2Scalar1Exceptional 227 = (10755760021798172186175041852852899812919554048788723362748470 * 10 ^ 70 + 8010594123806453100112944225468178731856740368161906584445624335807679) * 10 ^ 70 + 4629042921382358068171849199961857308256098101487369037133645247849705
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_228 :
Polynomial.coeff recurrence2Scalar1Exceptional 228 = -((10116945889204214477940856334855119249541110844390605636328127 * 10 ^ 70 + 1179683585602015360287401100990890408856547079530125850730233745781511) * 10 ^ 70 + 7952100640468296015157818838666857541337608843534262892617936249743609)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_229 :
Polynomial.coeff recurrence2Scalar1Exceptional 229 = (8588276842181946613642189432501114920509131109820954733889894 * 10 ^ 70 + 3709458509617185421865695699487844079826906313080981526093109673533571) * 10 ^ 70 + 6465563550863438686792062446676155664734208067434595525434127112129979
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_230 :
Polynomial.coeff recurrence2Scalar1Exceptional 230 = -((6617734345747775450536499591504477957856820991620378804116882 * 10 ^ 70 + 1753766170310731940396123614644052427463063264776643526816352005849030) * 10 ^ 70 + 59036806603635392259143874198467407382345378209275339744987705313781)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_231 :
Polynomial.coeff recurrence2Scalar1Exceptional 231 = (4600039224856351802650757978025086841957256191754640902020308 * 10 ^ 70 + 3690008537652568135771998044594231317488897315921879248580717174822748) * 10 ^ 70 + 8992504747080438662562338088316910498634621250688324983246492208549466