Recurrence 2 lookup certificate: Scalar4Shift 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.recurrence2Scalar4Shift_coeff_297 : Polynomial.coeff recurrence2Scalar4Shift 297 = (2179422365886486134348317089949227245450650318752 * 10 ^ 70 + 1628362229848749923007235250439825172357353410815488889596698190389219) * 10 ^ 70 + 550961675577297055912966787239460583031766098607418930088458403738219

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_298 : Polynomial.coeff recurrence2Scalar4Shift 298 = -((45633366001094955902410162417243649728610998057 * 10 ^ 70 + 8440954596743643445502450317029396707049804677740304822190385144370467) * 10 ^ 70 + 5846638701571275029386081062097203456427734398680947440861146496519945)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_299 : Polynomial.coeff recurrence2Scalar4Shift 299 = -((67674409684653836291896309403445112984741030582 * 10 ^ 70 + 1921617213562958342332703545563354148067526433365893589122859614418329) * 10 ^ 70 + 6873101165429969258838803835027208908925261118504505661268110385681785)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_300 : Polynomial.coeff recurrence2Scalar4Shift 300 = (24939193210780447497604447045624329433138664328 * 10 ^ 70 + 1946880070531197042162116907585174619179238435680999450856677752721438) * 10 ^ 70 + 4322404234245670409619666464677086186627555534583185924875011464892876

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_301 : Polynomial.coeff recurrence2Scalar4Shift 301 = -((6011611110526513660149756794669875186553443717 * 10 ^ 70 + 2463278037830452037888053400343296824601046231888173329674936019274222) * 10 ^ 70 + 6950506114746177319470775668364787428713564663033029205517544443363008)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_302 : Polynomial.coeff recurrence2Scalar4Shift 302 = (1145290374869774145947921199709782022380267077 * 10 ^ 70 + 934923568222825979606178110130406978759448936263188514314331575256367) * 10 ^ 70 + 9459604681573714839260244676598853457518514048812730868385016329124528

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_303 : Polynomial.coeff recurrence2Scalar4Shift 303 = -((178591451315305569246247780964111604195777270 * 10 ^ 70 + 5886939635283527748421763538422558816172479062132406394608299870673877) * 10 ^ 70 + 492899267973111647791649124515164765450530980291280783942491564772236)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_304 : Polynomial.coeff recurrence2Scalar4Shift 304 = (22169980683515453382366054960806258559928575 * 10 ^ 70 + 8734159627248979146249099733385903191683521230444654699244593709389148) * 10 ^ 70 + 7804608782876022105190700577355603447304706402970934308318924082279873

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_305 : Polynomial.coeff recurrence2Scalar4Shift 305 = -((1885826539433721509329173026109540052979632 * 10 ^ 70 + 8007137196034569212938985913077847176929508487014351589134714569611615) * 10 ^ 70 + 4080196730389428883757428998174790615945562308250624399260136978144663)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_306 : Polynomial.coeff recurrence2Scalar4Shift 306 = (11057244888595468090508373753914321925849 * 10 ^ 70 + 4400394684741926874902748788038876713172759858531426568280266908675479) * 10 ^ 70 + 3515582605772660496188212021101020428460225393571635132163747613008047

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_307 : Polynomial.coeff recurrence2Scalar4Shift 307 = (35819195749819141432660950100646018688330 * 10 ^ 70 + 5532897623216876870818739700521647890905388716032047956385290962196848) * 10 ^ 70 + 5283825094639016200169451625634081998629649840484125822868990301475588

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_308 : Polynomial.coeff recurrence2Scalar4Shift 308 = -((8965085383093432793310991101121250128856 * 10 ^ 70 + 8736989066675764488102073577095850239430758891324141495338978398845404) * 10 ^ 70 + 9177365189549922912470210643096471085584430939794727051569998973139895)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_309 : Polynomial.coeff recurrence2Scalar4Shift 309 = (1473282450604524928764385991055865511218 * 10 ^ 70 + 1577039041959032495940881925250354999101389821381031689722589254255762) * 10 ^ 70 + 2961241043627054358231650338268351530041219120986842899257435108205245

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_310 : Polynomial.coeff recurrence2Scalar4Shift 310 = -((186135465818924786925727348050945658900 * 10 ^ 70 + 6544425830825438405675642881922815129650930230982245701521795357746182) * 10 ^ 70 + 8385859760238495698631791384437695228460182960856862069468923588427158)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_311 : Polynomial.coeff recurrence2Scalar4Shift 311 = (18213434735494388941087991994578891374 * 10 ^ 70 + 8249101930275196559980316099738430151248251663460744244996827950676624) * 10 ^ 70 + 3641078307536674966780275780409591682604137480323100128783107943413885

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_312 : Polynomial.coeff recurrence2Scalar4Shift 312 = -((1236119533976088127498582460779464127 * 10 ^ 70 + 1981335205935901657309684407548749900858296568590791568046164810178945) * 10 ^ 70 + 4274779012907006610356706361916236195285723371961696454129262981766763)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_313 : Polynomial.coeff recurrence2Scalar4Shift 313 = (21950055095868905594382465243356709 * 10 ^ 70 + 4586362036948190055061613570459957693925407104582089977826152431382513) * 10 ^ 70 + 1088169086940167733774942427607370361562182002398861752236531118328380

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_314 : Polynomial.coeff recurrence2Scalar4Shift 314 = (8894563880452419676089106850015975 * 10 ^ 70 + 600628313029610826000871765820254461106534505891408968593217683241415) * 10 ^ 70 + 4878972364355874481698794664101672992326424122135392473094728802954728

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_315 : Polynomial.coeff recurrence2Scalar4Shift 315 = -((1676022483341003611333383912977050 * 10 ^ 70 + 8160378656705522712981487238258957676964055399281275453874490354484212) * 10 ^ 70 + 8202553190787977662999755150453809643910951982266913827204566777324592)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_316 : Polynomial.coeff recurrence2Scalar4Shift 316 = (186845502115647990724023934667057 * 10 ^ 70 + 6462561428452043828636831377088766518355280625131423191944824877180600) * 10 ^ 70 + 8707404475187622463810909620402209711141335417859943013171130945770001

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_317 : Polynomial.coeff recurrence2Scalar4Shift 317 = -((14833999417213202349570281797353 * 10 ^ 70 + 1274201553187001403323477528684133278783365207994415206249527970168729) * 10 ^ 70 + 4869410503747493942931324313270524189005922853129979162996655834532255)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_318 : Polynomial.coeff recurrence2Scalar4Shift 318 = (794818589538113363714110850006 * 10 ^ 70 + 8538555380483115635388135997909310663310801575007562078627372982987190) * 10 ^ 70 + 2429041645758023009376207982017378015290600479584221567141089476221519

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_319 : Polynomial.coeff recurrence2Scalar4Shift 319 = -((15122366422211861040830262797 * 10 ^ 70 + 4302007772414043778299835625283008192345158022851557240439983915481537) * 10 ^ 70 + 9491885803271156255567532371363290929458174891076551058670399218593023)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_320 : Polynomial.coeff recurrence2Scalar4Shift 320 = -((2225366037047929959986202952 * 10 ^ 70 + 6210993403409932743712364791853640759723803746816284727712683921617984) * 10 ^ 70 + 4642636705986367336957397282554813402307592919078522047374602797622135)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_321 : Polynomial.coeff recurrence2Scalar4Shift 321 = (305451495797320627408452692 * 10 ^ 70 + 663838879895611431857033339489627118897276033371584202236046577800907) * 10 ^ 70 + 9680791153626665220715107378209878798238201455141561847673851572957919

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_322 : Polynomial.coeff recurrence2Scalar4Shift 322 = -((21740552965139200008651689 * 10 ^ 70 + 3923429433448601914537405394268996929981872486733009282831069877881833) * 10 ^ 70 + 9921817705047710822991183449015142403142944636909969443096996818117894)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_323 : Polynomial.coeff recurrence2Scalar4Shift 323 = (967180525808139614917594 * 10 ^ 70 + 1800057486971414325270454092381910707895588910136284655778836387563773) * 10 ^ 70 + 1001255536631308867289207147677936180666335402095700293574608616031849

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_324 : Polynomial.coeff recurrence2Scalar4Shift 324 = -((18842427101357941343196 * 10 ^ 70 + 3547928244509460039930248327046630625719397181702544921516367626081014) * 10 ^ 70 + 5278353517716714348634981849475717206231988719113283222573687256030)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_325 : Polynomial.coeff recurrence2Scalar4Shift 325 = -((887107056760758530464 * 10 ^ 70 + 2870245635797301492237285375390808898083428901098890592392900822450148) * 10 ^ 70 + 8199705927616653175237375352015941938504674894841879464746851179430609)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_326 : Polynomial.coeff recurrence2Scalar4Shift 326 = (96731116432805337857 * 10 ^ 70 + 1030264477598055137850434012187012521474709194607035343398983325060840) * 10 ^ 70 + 1499127228550021149576633395446653614706230020708565142004392154361852

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_327 : Polynomial.coeff recurrence2Scalar4Shift 327 = -((4297382788160724339 * 10 ^ 70 + 8574716297939116502477232396571559610047408335075769009010673791978802) * 10 ^ 70 + 163094591965042213743469951692551926505967737097706890185103798646637)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_328 : Polynomial.coeff recurrence2Scalar4Shift 328 = (94762487626908762 * 10 ^ 70 + 1837280876470010059609681128866265190070500912355967566917120569115879) * 10 ^ 70 + 154379303913442470615113372120749483269263839555413268568522189118093

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_329 : Polynomial.coeff recurrence2Scalar4Shift 329 = (392137868862818 * 10 ^ 70 + 8075014458538778057976973824063482855951254765447450638875346435891851) * 10 ^ 70 + 694912840059164120618977447732929580090653561231941048998217341228550

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_330 : Polynomial.coeff recurrence2Scalar4Shift 330 = -((100600563589410 * 10 ^ 70 + 2131550592102984041130362540286315428325441888867885974053560976903428) * 10 ^ 70 + 2499891113850143309000423870727585484868110810038483154654104112497960)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_331 : Polynomial.coeff recurrence2Scalar4Shift 331 = (3192449178508 * 10 ^ 70 + 8455314463870412907949482967471394528866738342949318096564379229956703) * 10 ^ 70 + 1725955828328306637224337864312601477395446088603856115412696503530482