Recurrence 4 lookup certificate: B3A3 coefficient convolution

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_246 : Polynomial.coeff recurrence4B3A3 246 = -((88048845557248867395106520396560455691262021 * 10 ^ 70 + 7504760851457590003001033044000290593775652385443777228611689307696016) * 10 ^ 70 + 6412043713851997188802989158382348924577685195588969849153634011943502)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_247 : Polynomial.coeff recurrence4B3A3 247 = (21068484634900988552700135887803821771533763 * 10 ^ 70 + 4959662422130886036273834312881115206326143289991457412626133747907110) * 10 ^ 70 + 3422228894036770445996198708623092258624748960000945307781859988971031

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_248 : Polynomial.coeff recurrence4B3A3 248 = -((4181685818370386685379556227330320506754779 * 10 ^ 70 + 6238537126873161797850552037188058337459721910090167233672776697470233) * 10 ^ 70 + 8454098023015155467180047116660308603815193399779785826366077255270663)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_249 : Polynomial.coeff recurrence4B3A3 249 = -((122074967361057878802022131828935956821160 * 10 ^ 70 + 1700001121976180904668410829149318427009118667132706343212680142599319) * 10 ^ 70 + 7987876352999312351460735634463319562475158410654430885536655352808173)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_250 : Polynomial.coeff recurrence4B3A3 250 = (990223379651402706379343898773149363192590 * 10 ^ 70 + 7867012227552091946231734805017406099981170925405570131770520236234588) * 10 ^ 70 + 4543479011350823615768126496843220712771259182336256734476020419164481

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_251 : Polynomial.coeff recurrence4B3A3 251 = -((894960685253512527205731505035679184670107 * 10 ^ 70 + 9659403248592416819073302786306731150279768565884575348430460318266470) * 10 ^ 70 + 5411363168273020012848109951995674625265707403352609759780097131222745)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_252 : Polynomial.coeff recurrence4B3A3 252 = (601939974285942643279486315184508408631357 * 10 ^ 70 + 4757687675843690085467646296985015314918475091197001876821814175462268) * 10 ^ 70 + 8590445229384010325283206079757340607438747629740773211666309205008203

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_253 : Polynomial.coeff recurrence4B3A3 253 = -((347864950872002107560509230721819852821526 * 10 ^ 70 + 971783173299648908701696134294192633636621808148013782428143785864660) * 10 ^ 70 + 343200926596026698853901972842339184180742373275844451413642672189097)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_254 : Polynomial.coeff recurrence4B3A3 254 = (180615682424410717740851222259952086302876 * 10 ^ 70 + 5161731303119725190850478896802797188327305595686862771519855001207750) * 10 ^ 70 + 5945309818479601527484401003080701106785963285262618495274929973425338

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_255 : Polynomial.coeff recurrence4B3A3 255 = -((85910129753670993294956658337310638843009 * 10 ^ 70 + 8904124028768948420232835191127542140054241908317616670008040806546887) * 10 ^ 70 + 8173120215503495938017156527472720780499112277299716162074398903521380)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_256 : Polynomial.coeff recurrence4B3A3 256 = (37789302759998989735055966864623770552239 * 10 ^ 70 + 5832667376343204968817623640406459726841729693594054794778625628150126) * 10 ^ 70 + 1743386791460258800431543187988364489521417805752474352001619577414937

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_257 : Polynomial.coeff recurrence4B3A3 257 = -((15430518879791395846336510255634765956958 * 10 ^ 70 + 3109851235990820027031827920229105779580185443811514137472372319280893) * 10 ^ 70 + 7117589629814774449752211253135493244734328139101044599499422704909266)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_258 : Polynomial.coeff recurrence4B3A3 258 = (5845733017717549002132196376234109612666 * 10 ^ 70 + 3996198195800314906450936225405913296386303632031258122195694893015530) * 10 ^ 70 + 5196179940127259127715276988372657786438643863457116565087683840742853

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_259 : Polynomial.coeff recurrence4B3A3 259 = -((2043751739092822268139404012902393804160 * 10 ^ 70 + 4038813304263851120369092803551841836678890625722697459167150103026362) * 10 ^ 70 + 2084184994049502417196773160671549709827408624851471127197098730661494)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_260 : Polynomial.coeff recurrence4B3A3 260 = (651121864650145123551268336931765996857 * 10 ^ 70 + 5966944278714161126269375134328633803565558549136339122979733345230933) * 10 ^ 70 + 5398787235056839692213375516723818070259875259115444231241770587986649

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_261 : Polynomial.coeff recurrence4B3A3 261 = -((183897938625094488592552427421583356366 * 10 ^ 70 + 8737166817011117336064785207201218089675185193866337081586782294972088) * 10 ^ 70 + 782605168368075481953428565592697179618175875602314155178063576089106)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_262 : Polynomial.coeff recurrence4B3A3 262 = (42966529614151053276834659905490334207 * 10 ^ 70 + 4732030517502292654128717950704233347126972469539352274262588243356006) * 10 ^ 70 + 2332768690559718867963005877079818132543511115993720246307806050074367

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_263 : Polynomial.coeff recurrence4B3A3 263 = -((6360054921462236715918768354647687098 * 10 ^ 70 + 2430816437963330154179259222183613219603306293359380653689247638217316) * 10 ^ 70 + 3328482197390832441674198676165765467862631248080663353900194931209872)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_264 : Polynomial.coeff recurrence4B3A3 264 = -((840954610983212693243459807136790203 * 10 ^ 70 + 2400354269100047795050455365946230361784619569227042425477702247071742) * 10 ^ 70 + 3913738463039541010839901531785100207067714028226231360401802037451140)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_265 : Polynomial.coeff recurrence4B3A3 265 = (1247466541255782752335306755868728320 * 10 ^ 70 + 3789076938668778708808530826905104761677762616847006442575391870272776) * 10 ^ 70 + 8001789772589512625329286234086517090993087594521189700033763051897537

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_266 : Polynomial.coeff recurrence4B3A3 266 = -((693287335134881302636021205815258568 * 10 ^ 70 + 5401199194826700888087156944273777718513072052087523626388231159853931) * 10 ^ 70 + 7330536769891477760699445337420513994550549061788610773214416266743733)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_267 : Polynomial.coeff recurrence4B3A3 267 = (299277040830515408331918564802901810 * 10 ^ 70 + 1960495163585424676868721624978003856519485540530228576973286096438941) * 10 ^ 70 + 4284006077933859989556481920724815955803521596707802569709854098802394

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_268 : Polynomial.coeff recurrence4B3A3 268 = -((112922845375157998792912945366708568 * 10 ^ 70 + 4348213440159377954191089028620814112469200425490369554768784065356963) * 10 ^ 70 + 5337574266519676230878618897996826534726578177634309387837151180243529)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_269 : Polynomial.coeff recurrence4B3A3 269 = (38897795821580566894715474569928129 * 10 ^ 70 + 1493760661114442269956631592069390166985952457060380154842818497881110) * 10 ^ 70 + 8865539383862293134914300655071865324654763884991602823659198829983752

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_270 : Polynomial.coeff recurrence4B3A3 270 = -((12485369723524815557751417806573370 * 10 ^ 70 + 3495795365563065046161937268763840887430998058654676451576979873232755) * 10 ^ 70 + 4971959389573421258618125298965607254889933784028207981242704807372640)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_271 : Polynomial.coeff recurrence4B3A3 271 = (3763572309804020607700146274424904 * 10 ^ 70 + 3883993229941639419258929694532114855045231988187284186774578237344117) * 10 ^ 70 + 3387336490128793388041678104436034651178163658364620742251117329916830

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_272 : Polynomial.coeff recurrence4B3A3 272 = -((1059075060385397026671362408870924 * 10 ^ 70 + 3322016351961455078192194187664732052987527725745176494159661875962770) * 10 ^ 70 + 8971145515391045171438345420194827526040062759278698875464643880647782)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_273 : Polynomial.coeff recurrence4B3A3 273 = (269686052953525261448358107268726 * 10 ^ 70 + 3442232382267099517818791802857601940925070286053714007334462980351501) * 10 ^ 70 + 2742848378259115599400032687866436455161088122713626896672005603921210

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_274 : Polynomial.coeff recurrence4B3A3 274 = -((56086369835499634535042326725139 * 10 ^ 70 + 1976659834794102292690843377747188249928126712877619690669967912171399) * 10 ^ 70 + 2449096976933691659721360537579033076413464101260443279367752285652970)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_275 : Polynomial.coeff recurrence4B3A3 275 = (5307732595295931689509770643553 * 10 ^ 70 + 1461229917116865587042240018139331474517746249178967814874480321695155) * 10 ^ 70 + 3769146507710776156274493225932204842876058177437240002744469830185693

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_276 : Polynomial.coeff recurrence4B3A3 276 = (3401887042338899462273667791239 * 10 ^ 70 + 2985501339375769786785735953826076542719930201626168124863767993405918) * 10 ^ 70 + 1396201550790625163220462226845337414740458368546156513427310152855247