Recurrence 2 lookup certificate: Scalar3Shift 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.recurrence2Scalar3Shift_coeff_300 : Polynomial.coeff recurrence2Scalar3Shift 300 = -((23898764154797113251399357905195646853363849447805 * 10 ^ 70 + 1639021666097075691941750090293036991890426599221885815010965722007163) * 10 ^ 70 + 1682338733124183112007619739533920431023544309846003953182637180856632)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_301 : Polynomial.coeff recurrence2Scalar3Shift 301 = (5096819024125284467421690692809739429571429805732 * 10 ^ 70 + 2128623081879374657337679965546397560832053083082355784096088352335600) * 10 ^ 70 + 6028829104040986660801736071772705276053171024143695572642004616267400

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_302 : Polynomial.coeff recurrence2Scalar3Shift 302 = -((914736044970298857755319479562490027087103909836 * 10 ^ 70 + 3034588106155218253398012868527308923380480524299785935086409778625413) * 10 ^ 70 + 8859214408701936851290906695821499380175354225607596227045461884060970)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_303 : Polynomial.coeff recurrence2Scalar3Shift 303 = (136641576936893146959594814371194155893667841423 * 10 ^ 70 + 1470904995600545701726500592217765813139141133435285409579179404133801) * 10 ^ 70 + 8630692160229910478982048341092214309018492192027253387661064009753068

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_304 : Polynomial.coeff recurrence2Scalar3Shift 304 = -((15821314632747899021161093010690305768491759541 * 10 ^ 70 + 5229234073179160786652211435251214529041691111229271720760391929168419) * 10 ^ 70 + 9216970578752971164903835731416051254290677147104737830794229579612434)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_305 : Polynomial.coeff recurrence2Scalar3Shift 305 = (1014846042798991912214209860223199286220082255 * 10 ^ 70 + 8902004701092955905843038931665893064628150902208595957632450861494172) * 10 ^ 70 + 7325660408827383695109707497395018407874838659173242362301201232556239

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_306 : Polynomial.coeff recurrence2Scalar3Shift 306 = (108262072426078001072826329669732993262656271 * 10 ^ 70 + 5541618802744472444985231206107662954101972796005282896592347392759218) * 10 ^ 70 + 1406767010935322352508340023463077196805090560346643588247414116021574

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_307 : Polynomial.coeff recurrence2Scalar3Shift 307 = -((53301064334539152553313579593822018554879913 * 10 ^ 70 + 8282635222363399481214830901285571751493719195177500685089753913018216) * 10 ^ 70 + 1177580998142761649200866469423723943417257042066953849357645005475940)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_308 : Polynomial.coeff recurrence2Scalar3Shift 308 = (11588432056410276016394875774461007718251541 * 10 ^ 70 + 7212127660254770438395770628854060628779733742521798472298711552614938) * 10 ^ 70 + 1315741633180302666409125783393912581113185719469942629117310798216615

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_309 : Polynomial.coeff recurrence2Scalar3Shift 309 = -((1822884261106759236142571834499847887865415 * 10 ^ 70 + 2243884793130288665864943044948135104402659668230607770383689578958387) * 10 ^ 70 + 6660821908393052796548205464436917474176783332418896698829956425405531)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_310 : Polynomial.coeff recurrence2Scalar3Shift 310 = (218368209470656221056622522055351831723996 * 10 ^ 70 + 4262037077841531627057268721121796552796332628878158686374609145462500) * 10 ^ 70 + 5944126244646063318059476381193898668575825761202883282591198631928566

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_311 : Polynomial.coeff recurrence2Scalar3Shift 311 = -((18028604189167337040831334855582858755950 * 10 ^ 70 + 6453181908077756248491769028551976504203526444447363547539373692410037) * 10 ^ 70 + 9311789772774767881284818355129364240098934741759706421031304566770474)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_312 : Polynomial.coeff recurrence2Scalar3Shift 312 = (367261709739049883912436760977453702631 * 10 ^ 70 + 2563762428673099573899881651810890752639033632534764854390362694951024) * 10 ^ 70 + 3232645052840193572579071242060365074278698752482678628703774791550435

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_313 : Polynomial.coeff recurrence2Scalar3Shift 313 = (202101879713460729378091813889441061324 * 10 ^ 70 + 9282213494739765172996805780864368249611690622211309914347088689405958) * 10 ^ 70 + 4752873225625932136152911351747721584518459914836101062867944753539764

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_314 : Polynomial.coeff recurrence2Scalar3Shift 314 = -((46732814658551736694930577508032397827 * 10 ^ 70 + 2158374676349228110671162645531561068094141570762903394600170183728280) * 10 ^ 70 + 9314475113039279811987371854679864908115891321124153125435415528390022)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_315 : Polynomial.coeff recurrence2Scalar3Shift 315 = (6467219982354390208481968386769752478 * 10 ^ 70 + 5394590238602251839787034260714099329853143283242106985599366507734382) * 10 ^ 70 + 2959937588513398598522460289484928496438110118810474095296671577845953

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_316 : Polynomial.coeff recurrence2Scalar3Shift 316 = -((636981838681375016228352252358057182 * 10 ^ 70 + 5696951993615077396083962039552834425833981037706747360212501911188463) * 10 ^ 70 + 1188321838357165747571251434670589124330678504715350893942399542528309)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_317 : Polynomial.coeff recurrence2Scalar3Shift 317 = (40873258610628590943332086257414705 * 10 ^ 70 + 1390806687759443389222788762314174529028140633785903880073821398721622) * 10 ^ 70 + 798285556410255205197156877368900523139374236274318221135667593408084

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_318 : Polynomial.coeff recurrence2Scalar3Shift 318 = -((398069549374174767139478476067331 * 10 ^ 70 + 3297358641510058743683729706634080753487859280221974353139377501722721) * 10 ^ 70 + 1466009925800745182889650512900684903729278322397723426509427969152557)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_319 : Polynomial.coeff recurrence2Scalar3Shift 319 = -((315869612680423027888739389081269 * 10 ^ 70 + 4405642786024700860154867039092093255864714696519005206107236245590488) * 10 ^ 70 + 7548536709831783673034450521626904644261388563611750715992075356428369)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_320 : Polynomial.coeff recurrence2Scalar3Shift 320 = (51259158690130321894850995325899 * 10 ^ 70 + 2468783260239492925724296140915838404028326155112225835746544186162366) * 10 ^ 70 + 5248302171718683088523586537537471133035859213440255773029301487964101

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_321 : Polynomial.coeff recurrence2Scalar3Shift 321 = -((4952760419246593641383599979357 * 10 ^ 70 + 6846925312305552934784878500452599564234309485302190806829440313446926) * 10 ^ 70 + 2866493612372266681395670223710479811979568854376411886883892172819478)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_322 : Polynomial.coeff recurrence2Scalar3Shift 322 = (321527027857941854138989077303 * 10 ^ 70 + 1273334297738246090278960832550967332613115819119928251607075276663966) * 10 ^ 70 + 7534184404694164282756476925428256463415403642631750945780799751059442

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_323 : Polynomial.coeff recurrence2Scalar3Shift 323 = -((11061259688620477869926207105 * 10 ^ 70 + 8289142389862590826565346154263387421400468442006726455618165945672841) * 10 ^ 70 + 4641767162770408794475637543468507868276897776823309577380800128850721)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_324 : Polynomial.coeff recurrence2Scalar3Shift 324 = -((369435669482380152851931893 * 10 ^ 70 + 3026972397287633927550305040526357865050044073074305270812872567259865) * 10 ^ 70 + 9357281627248237078012683081281084444923908834813865538476364073846095)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_325 : Polynomial.coeff recurrence2Scalar3Shift 325 = (88675754914654568680606328 * 10 ^ 70 + 8016799464780418963653001154915712424337310955607756898707510102675234) * 10 ^ 70 + 2573599446362874172981030506066057711450829314988542860986596528147510

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_326 : Polynomial.coeff recurrence2Scalar3Shift 326 = -((7260745550125830388303648 * 10 ^ 70 + 8811424974968258593864655427623588856410115355974914379570475086456292) * 10 ^ 70 + 9221352921738046212009237987612527488833191190170110844188936817589784)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_327 : Polynomial.coeff recurrence2Scalar3Shift 327 = (356427983171439196716601 * 10 ^ 70 + 1355558604818157615450511608444729654590119124981237344435471156849873) * 10 ^ 70 + 6768992614223563915634664912755870953123643863719582460097555924812329

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_328 : Polynomial.coeff recurrence2Scalar3Shift 328 = -((8500731867432920524017 * 10 ^ 70 + 2163207452612863077777908803167380716253246678855356477681842171251842) * 10 ^ 70 + 4365678766902651366217202374410248447999958826961282390983502900807722)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_329 : Polynomial.coeff recurrence2Scalar3Shift 329 = -((227654867472782899381 * 10 ^ 70 + 1108652810125951596190039353104901023886936930154441407210031309870382) * 10 ^ 70 + 7065308319138120651898314570509375136421686524691069546954595746836015)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_330 : Polynomial.coeff recurrence2Scalar3Shift 330 = (32193326328317321431 * 10 ^ 70 + 8314597259696478245163884909569741194915965593934616997506621440817237) * 10 ^ 70 + 317689700140931517851968815633936166813793939598562333270050779663979

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_331 : Polynomial.coeff recurrence2Scalar3Shift 331 = -((1522419035547277143 * 10 ^ 70 + 9120203981289647394957645224268192199241881827308576955665463784477787) * 10 ^ 70 + 5598058043073761419315647817677296569429307681696117737008162334663773)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_332 : Polynomial.coeff recurrence2Scalar3Shift 332 = (35338316776429816 * 10 ^ 70 + 8918081041052995139774874453293979272738602542028812091457846737275728) * 10 ^ 70 + 7541317979101159257736434767528411614690886104973892369667999934290277

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_333 : Polynomial.coeff recurrence2Scalar3Shift 333 = (82936043550752 * 10 ^ 70 + 8259196518862366003424057584577156798705365459864710287754087191365355) * 10 ^ 70 + 1900108990292771863071184368019820248508885742401371430615680152946385

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_334 : Polynomial.coeff recurrence2Scalar3Shift 334 = -((35059301771352 * 10 ^ 70 + 4950674648106323375496334187492851025155712264337316105281665154232640) * 10 ^ 70 + 3433160686925053170313291735790565812483088886183450849166505875208925)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Shift_coeff_335 : Polynomial.coeff recurrence2Scalar3Shift 335 = (1136712399084 * 10 ^ 70 + 8202985952212429392296325601449831801177290838841695146247249145814385) * 10 ^ 70 + 4344623470617119543721388193477972144534597462648953279530979838029331