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_216 : Polynomial.coeff recurrence4B3A3 216 = -((162907507112988861466196978259514282638107941738360350109 * 10 ^ 70 + 2493225316981760294620130013372181266301610777090458534960796851291147) * 10 ^ 70 + 1575888792630358899830735195343151711895887559820782285176735080239030)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_217 : Polynomial.coeff recurrence4B3A3 217 = (96928802240674423151420597880601914064756573826942238988 * 10 ^ 70 + 4574162773091193872868937877956314742746474888761860434077736140086019) * 10 ^ 70 + 1898433690205533107639954262481403939882591095913094528640016657571350

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_218 : Polynomial.coeff recurrence4B3A3 218 = -((55545780931422231640323494561067333627973291044091735965 * 10 ^ 70 + 3706713918425572904462746588522243484164690042458289222994993577520690) * 10 ^ 70 + 3484460196822648312146688184894171415417599220454191692004579985951344)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_219 : Polynomial.coeff recurrence4B3A3 219 = (30804251780684071664874590057773063344958189908537575911 * 10 ^ 70 + 371190364870268218808001061181705247203338630174447195597893896416059) * 10 ^ 70 + 4103461634388802830723777911008650802234197472571665940100058506597853

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_220 : Polynomial.coeff recurrence4B3A3 220 = -((16583591001733250402307113804725735324667506002767407891 * 10 ^ 70 + 4434625070658671275728473367220184725341466933403263747507479248682046) * 10 ^ 70 + 5093302501219238505443293845740196846597894105088624840731492299271350)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_221 : Polynomial.coeff recurrence4B3A3 221 = (8684557911595689712582383311505491087486056107152693021 * 10 ^ 70 + 9457660076038232542624042617082407235022389873883853737864896964985584) * 10 ^ 70 + 6172144663836220684929006589969105885992109966426478074331586136956322

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_222 : Polynomial.coeff recurrence4B3A3 222 = -((4430072578823469080338982769514912682096148732144099177 * 10 ^ 70 + 2843682504665372762991425895759630138561937456338440847810722971214227) * 10 ^ 70 + 7914360142609686163594839761557187214048423271934430960437355184769161)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_223 : Polynomial.coeff recurrence4B3A3 223 = (2203194131743833870606146055660331018168606677132247978 * 10 ^ 70 + 1396254489070417823299368203194040037021809765424528324715460761734974) * 10 ^ 70 + 5568799933055365971801243433569310023575645751563877622355626442736482

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_224 : Polynomial.coeff recurrence4B3A3 224 = -((1068829146535208598753090674483752294947771456404942101 * 10 ^ 70 + 4140622421838989869617652007252236802429431677929711501361888489410967) * 10 ^ 70 + 7368122823052459167060210963985747191474984885570803642167473872339640)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_225 : Polynomial.coeff recurrence4B3A3 225 = (505941063026645620268866241986647795041967087083666898 * 10 ^ 70 + 1510273691698359090468633012875699901728839285709958443639938270987654) * 10 ^ 70 + 1828646215464553699807722367618090580370840235558665951635457535491514

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_226 : Polynomial.coeff recurrence4B3A3 226 = -((233702320211071507747881107340708827712846254550438507 * 10 ^ 70 + 6161787757844022913970159072461316923250200479030685144933756843175448) * 10 ^ 70 + 1815496186804370003130392498463023750016333072544559056060737809391351)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_227 : Polynomial.coeff recurrence4B3A3 227 = (105332513172760857666926433148495649970400778320653550 * 10 ^ 70 + 7108483391184996710619342774232498682186438334304516042327096096234455) * 10 ^ 70 + 9934025505069664385899102831012194156005275634521269298174269242385684

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_228 : Polynomial.coeff recurrence4B3A3 228 = -((46313055379885746572070992908430272108856572935431634 * 10 ^ 70 + 9736179066295727002707873088029360844180554588195335034157134874429952) * 10 ^ 70 + 4779503124252308596753622808951378676760404259975784107759917327895727)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_229 : Polynomial.coeff recurrence4B3A3 229 = (19858112859291337040757617360116221040167025903410814 * 10 ^ 70 + 9225655450537633730818398683512972950029991934160489592684003709306566) * 10 ^ 70 + 9833599861999876612129977445759690814435821852557749877155121388716907

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_230 : Polynomial.coeff recurrence4B3A3 230 = -((8299798788497882845090496243497309834396614424069370 * 10 ^ 70 + 8629837663539455382551628413152615362538844823630287956974216055183604) * 10 ^ 70 + 1521844535545927187573315270470805479141943642646024781027775754286879)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_231 : Polynomial.coeff recurrence4B3A3 231 = (3379424118605110592030091288106623952502344912276142 * 10 ^ 70 + 4806242318821600248697761250943443922448284873337826380006522267364687) * 10 ^ 70 + 145201762857143567447093201902836381012333525735459331810420049035009

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_232 : Polynomial.coeff recurrence4B3A3 232 = -((1339550803788073479545862164834254863410003914562032 * 10 ^ 70 + 4613024162123842639457301018988455233284870805159661383993359146782353) * 10 ^ 70 + 6339587362724563561163813085710382899967089528033614226075850944472501)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_233 : Polynomial.coeff recurrence4B3A3 233 = (516477109792974964657795429219736710995708276605465 * 10 ^ 70 + 5093426241437236188818750639341054462463632502797233103852195417455607) * 10 ^ 70 + 4241511552822685547451657803203235700531840498131593815462652440943296

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_234 : Polynomial.coeff recurrence4B3A3 234 = -((193499485590924828543595843043380051958925351562552 * 10 ^ 70 + 1010109494554018608919784125926677915966417104116760623102583344056636) * 10 ^ 70 + 5287198284930800171038733761425350289319916655484755106239399575700734)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_235 : Polynomial.coeff recurrence4B3A3 235 = (70358928945900705999469451453440754764589908227622 * 10 ^ 70 + 5280190185449314857018055456625661973872719568890244284632276030707016) * 10 ^ 70 + 3850581522519208164318201460609823196922009341245255463655415942526226

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_236 : Polynomial.coeff recurrence4B3A3 236 = -((24793395671674182220349841982905440879036575679813 * 10 ^ 70 + 4522901246741982483204974697137521362077189115625174188720701191029514) * 10 ^ 70 + 1362041763288578316831340250807962820531917265685540372315621087770559)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_237 : Polynomial.coeff recurrence4B3A3 237 = (8452135478762506549854407247831469553100501406244 * 10 ^ 70 + 4264380587085079735778940141003883804472769925575815283740908294307277) * 10 ^ 70 + 3991728911085732944295712180624940402145795093439023344137316265066453

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_238 : Polynomial.coeff recurrence4B3A3 238 = -((2781582081597005723336220331730998402762651373974 * 10 ^ 70 + 9679937482811853220535084083091887738994697673633202043692969214446229) * 10 ^ 70 + 9105893568062922150144836322794782241154077376761704514267047008151933)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_239 : Polynomial.coeff recurrence4B3A3 239 = (881497931794979144307467635608021654975361031817 * 10 ^ 70 + 4228044218152357587447488128004833386752078869126065802815448480369163) * 10 ^ 70 + 5921533752568505255610092899852699810026042234248651899377199183834964

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_240 : Polynomial.coeff recurrence4B3A3 240 = -((268226284412860833754279430764742168829096776264 * 10 ^ 70 + 6110818923222585654081150874609481656548188138063810825834351738375560) * 10 ^ 70 + 6593191340017840100344379431805138692824003688368776190483586727575411)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_241 : Polynomial.coeff recurrence4B3A3 241 = (78126989037989882809247196336486495792915687688 * 10 ^ 70 + 925145587517179372176474322497611212019003335682616596916170410800716) * 10 ^ 70 + 3273982621964341472315226847946884846076873608513275332362437573360283

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_242 : Polynomial.coeff recurrence4B3A3 242 = -((21725751717057152860128714676475204002233738627 * 10 ^ 70 + 1409980880555282415585334882551916151293985979792756658885134458048876) * 10 ^ 70 + 2650057846204600622163799092484736066787571442486288595349207066981790)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_243 : Polynomial.coeff recurrence4B3A3 243 = (5763682828194076862133010060746111361158515150 * 10 ^ 70 + 9803307497561053972627367303363758583417212531600319885192435243943185) * 10 ^ 70 + 2078716450960069192262785569458612261570979340487535909250535844834830

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_244 : Polynomial.coeff recurrence4B3A3 244 = -((1464702832217740737919239733823443788196772702 * 10 ^ 70 + 7142934715613563920029467897403511977408641417365391815928722584236943) * 10 ^ 70 + 6407550550194552584428831711510539491767183501283125704913961558162230)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A3_coeff_245 : Polynomial.coeff recurrence4B3A3 245 = (361127575561655547169102508792432556768856319 * 10 ^ 70 + 3397460004729801951252501720319150948783318027009307731233785621042934) * 10 ^ 70 + 1199236498281230108713161374740178580301062689629989723405661627966044