Recurrence 2 lookup certificate: Scalar4Main 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.recurrence2Scalar4Main_coeff_233 : Polynomial.coeff recurrence2Scalar4Main 233 = ((2 * 10 ^ 70 + 5057327041114049748727115200318705275604219425774483380243344447416469) * 10 ^ 70 + 7976960140402595815960747700337511381261661001724427582813933767201133) * 10 ^ 70 + 9661657792775985574807797244229569410629980805620198196598865515037903

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_234 : Polynomial.coeff recurrence2Scalar4Main 234 = -(((2 * 10 ^ 70 + 2871626586340419799051821632226804390158489202336449304145904112507447) * 10 ^ 70 + 3315491754232813452129111558310529182485291173048651998110841942925901) * 10 ^ 70 + 4478908444473150495383945090668640817178841179764994982701578537347509)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_235 : Polynomial.coeff recurrence2Scalar4Main 235 = ((1 * 10 ^ 70 + 9340580889144803740619239846202873320532156981010622271396772677727976) * 10 ^ 70 + 2845681816180731094463493557888206239499274508955980123288363232152193) * 10 ^ 70 + 3527609430417298413517241187396633249172081259795413923536298274313873

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_236 : Polynomial.coeff recurrence2Scalar4Main 236 = -(((1 * 10 ^ 70 + 4813222249161520022515097989814886675980574111494011698786755566714103) * 10 ^ 70 + 1057759198559243826106667402134548158004581776065774406197211719777707) * 10 ^ 70 + 6081050922343524892745915900748796712459117680641636279978490331670013)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_237 : Polynomial.coeff recurrence2Scalar4Main 237 = (9757267909238146691725805794034231007857518492657073064713666088481184 * 10 ^ 70 + 2988935472459700023731527596718774960612944137671374498738210705751160) * 10 ^ 70 + 6325407740643900445367110834182473223077386418415527396020941104428197

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_238 : Polynomial.coeff recurrence2Scalar4Main 238 = -((4682728251802342731016313121774157820511009557814972145284574441846154 * 10 ^ 70 + 7318041728853255985014879879394517075401401915705586780541825540663314) * 10 ^ 70 + 4270156164956538308364238173399694049475247600970711443267101282428110)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_239 : Polynomial.coeff recurrence2Scalar4Main 239 = (61748796257815510421246412051399408222653137690219748412171341687230 * 10 ^ 70 + 924802750423147126588062730447554368661137966891056599496614430757209) * 10 ^ 70 + 5989207753041590226451371923976600515455844711615400014415983117421633

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_240 : Polynomial.coeff recurrence2Scalar4Main 240 = (3738664958035079709476863232766116506872591729057223985461035779771939 * 10 ^ 70 + 5396833779835954650556511224033733810968181453575386717539220945160974) * 10 ^ 70 + 3113630150550106907159338226820304017162548546731770390764400100763789

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_241 : Polynomial.coeff recurrence2Scalar4Main 241 = -((6498643732584501641217682538080534716429929280450152232545971052218296 * 10 ^ 70 + 827262118672688806973524598626311429724259576989410080253548548669141) * 10 ^ 70 + 3155689726407035693706851201286915007033504705083113535286719449867176)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_242 : Polynomial.coeff recurrence2Scalar4Main 242 = (8156732864852994302321558781057420058571793415885866955804940754587738 * 10 ^ 70 + 4545736834011248388916724411814000666178550823271089487421134845274311) * 10 ^ 70 + 5280766023891608928563737744434928286322591221333633909396133572194752

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_243 : Polynomial.coeff recurrence2Scalar4Main 243 = -((8792503298743527171160736932522884589964650048071381744082426214533600 * 10 ^ 70 + 1189984250901718257227121854171774944002982255808239644413259205401778) * 10 ^ 70 + 4300600138488815840078203010088240114019525249247298736425581592901577)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_244 : Polynomial.coeff recurrence2Scalar4Main 244 = (8588495995472722315772285571091482295007062688634599267402870804101743 * 10 ^ 70 + 8798819117019430611580180423043755243631730399018831074305040198061234) * 10 ^ 70 + 8100937997709316720862002533669005920634832900586036890589058070975142

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_245 : Polynomial.coeff recurrence2Scalar4Main 245 = -((7782574146567904921831825077969432401880110868161894806657449746305046 * 10 ^ 70 + 8544964579477549768547894847059329385960382091432644066840493935788021) * 10 ^ 70 + 3658206066710007627277156628794173802674437931789930203137073376187324)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_246 : Polynomial.coeff recurrence2Scalar4Main 246 = (6621648860206775958950719896940714272759502169063566390793938318315170 * 10 ^ 70 + 8894142415421182517420044799066692114551015193846898975195660775242751) * 10 ^ 70 + 1472456342563357817488812595511786961815254858192502791209386628723553

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_247 : Polynomial.coeff recurrence2Scalar4Main 247 = -((5325094848585737509117423149084217047628969015939737292470241774968613 * 10 ^ 70 + 2664045550265553451366319768519072104678813879070703938001475734279360) * 10 ^ 70 + 2712835893403210076795755600045215606120419323748660579296258663675014)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_248 : Polynomial.coeff recurrence2Scalar4Main 248 = (4062197538505271766502390226753265459656479018318820546045166033328825 * 10 ^ 70 + 1874632216477678241463252837018652509886575493508897130908928120623986) * 10 ^ 70 + 7587600705644551005203577860166204347176381371191368882280386437875061

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_249 : Polynomial.coeff recurrence2Scalar4Main 249 = -((2943978365596124189120952559595812440888742705636730322595077179388766 * 10 ^ 70 + 49049003019588345405432080222996238457107202032639569495495340298373) * 10 ^ 70 + 8387258755346882762954649019159399027670215721800979434777258503341089)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_250 : Polynomial.coeff recurrence2Scalar4Main 250 = (2026726229206241035645933191303456762709510557291716601172434074567892 * 10 ^ 70 + 2304969848137410935615323197278048254200114911849375691075692803653404) * 10 ^ 70 + 4152283039884669680007358715807722387004423959236479106479714533605337

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_251 : Polynomial.coeff recurrence2Scalar4Main 251 = -((1322995224996848288132936829843958676897036195564653980357456661234488 * 10 ^ 70 + 470477637762095115299162799720997993022920295211180591239294367811115) * 10 ^ 70 + 552509675163172687111342924661882045084600954932271847318984712757701)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_252 : Polynomial.coeff recurrence2Scalar4Main 252 = (815670964880634805934652467821992919613451842488111359134564563903940 * 10 ^ 70 + 4762893610479595023434483777873863088283930257197982119173133287852682) * 10 ^ 70 + 6820806079894605453422921146491605728751729137097837946277286199067356

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_253 : Polynomial.coeff recurrence2Scalar4Main 253 = -((471562963904417405795405211654924089981323000392068654751242593940905 * 10 ^ 70 + 8618264794686646602694887048771058319841102137616094955804495058974942) * 10 ^ 70 + 3097871432170364679141165033208145221987983146892505159822642759348293)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_254 : Polynomial.coeff recurrence2Scalar4Main 254 = (252314936813368497195438720492528360960868720976288672901623186034958 * 10 ^ 70 + 4381196934744636746341934480780383274106796102059843078316288814217715) * 10 ^ 70 + 7487852164598079830872113007897766178534970089757387536367426871662421

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_255 : Polynomial.coeff recurrence2Scalar4Main 255 = -((121759503221010459329646078505479551556973205866379900759862738370209 * 10 ^ 70 + 6524505682524590607518382983637798213475415155328096794064570310569835) * 10 ^ 70 + 5269468138841201891136495409657823545039563910456841430865924868702220)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_256 : Polynomial.coeff recurrence2Scalar4Main 256 = (49867196691105694092177311588667815558824006320550828971751876906966 * 10 ^ 70 + 9853876314145134769912460959933046888352911370528159329641791972125539) * 10 ^ 70 + 5875903170568847880335730946162732908860890984454919179696251800964341

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_257 : Polynomial.coeff recurrence2Scalar4Main 257 = -((14032551848324608583738555497190769123399987994810644416469534358012 * 10 ^ 70 + 7595516643083006566694767056673811432669592894336594211764222742733803) * 10 ^ 70 + 7723293730861852927781849005881823257727646628223846942485075877988839)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_258 : Polynomial.coeff recurrence2Scalar4Main 258 = -((1364023018918583943348982890060612097670685989474426096329249333825 * 10 ^ 70 + 8382021314911917069695413432931386184362814950702490366438526192991711) * 10 ^ 70 + 3906345757078972131554976241816869336647083313040678932758773580908522)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_259 : Polynomial.coeff recurrence2Scalar4Main 259 = (6262678930443496151115965834328334048569471172112235364066791425843 * 10 ^ 70 + 9680858301833019606512120721555106717022795419288683352676573558756635) * 10 ^ 70 + 3102719228919099889341804714405030033034097985924953078905208084506396

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_260 : Polynomial.coeff recurrence2Scalar4Main 260 = -((6466967141381333246787980441798992966569616507802960249583921296073 * 10 ^ 70 + 9606122424613101208716302252422342169268387711865263400974826599468515) * 10 ^ 70 + 2676021280874677120133562785536825686477512245187653689173118937331312)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_261 : Polynomial.coeff recurrence2Scalar4Main 261 = (5043671314002169760071889092046459285767620760973052532232432161677 * 10 ^ 70 + 2010651031140962690649921963235542100251001163773799410661902511772332) * 10 ^ 70 + 8095721707351994219058872330411554014846936773778292964389401110444430

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_262 : Polynomial.coeff recurrence2Scalar4Main 262 = -((3411735983611044006562077705574801142488066965158784086771254753815 * 10 ^ 70 + 8489774757661790301452396601430545311256217612940401645021331140635002) * 10 ^ 70 + 7113222151514425736206113326178053243895602617665295849225799464559980)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_263 : Polynomial.coeff recurrence2Scalar4Main 263 = (2095315015948059169872687107279616683503135097509927504463696871716 * 10 ^ 70 + 2886847528605335495213413379118857939632023817815886257685958113451165) * 10 ^ 70 + 7846289452102579455288271023447825637470169102012693363576455771498696