Recurrence 4 lookup certificate: B3A4 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.recurrence4B3A4_coeff_275 : Polynomial.coeff recurrence4B3A4 275 = -((1141731304012086984538121464326 * 10 ^ 70 + 6018490902169508556497014548264331674202284562708892820172010712972553) * 10 ^ 70 + 6533391581151712276972144253061407770467736554729542540344574512367840)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_276 : Polynomial.coeff recurrence4B3A4 276 = (375320799065876464994202718374 * 10 ^ 70 + 3675176555155657022481823197875260641386957455488864223329016950871687) * 10 ^ 70 + 4367098002708167757178410449574187693992150569825624377449574671268937

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_277 : Polynomial.coeff recurrence4B3A4 277 = -((116696621427647539591637102147 * 10 ^ 70 + 3403877628448696364942074983612516821849991891275426978949585007656333) * 10 ^ 70 + 8807457583333221588510785527122135757941545207960670311007326475170336)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_278 : Polynomial.coeff recurrence4B3A4 278 = (33968463048415396149568699211 * 10 ^ 70 + 6805212208157679553864459443061787124892085343187696324907159360164309) * 10 ^ 70 + 5190338785772295223900374606729278043997433641584669701877941450495729

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_279 : Polynomial.coeff recurrence4B3A4 279 = -((9093408220487146119642826777 * 10 ^ 70 + 7289467238086582100635276646693746484378874990448757894976548033300126) * 10 ^ 70 + 3834446300332880325369491299268604522376944937422495616945865426597797)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_280 : Polynomial.coeff recurrence4B3A4 280 = (2163707894380213283710952244 * 10 ^ 70 + 1527762352809112394705789968887923254235083858113419506607844293823716) * 10 ^ 70 + 2441582158565662182813832535242597860427978557914261554877679554099723

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_281 : Polynomial.coeff recurrence4B3A4 281 = -((421564980604112687946980695 * 10 ^ 70 + 4818103806083590786131879629940474239158595390158569596494747924848104) * 10 ^ 70 + 407812808339023925080941538669234654428820681538425921539066689154756)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_282 : Polynomial.coeff recurrence4B3A4 282 = (48088503355252562944210000 * 10 ^ 70 + 1628063081117426270332359942735376377283581828634848954309130442231467) * 10 ^ 70 + 5124043495047022711075481017284980334120677871727351452750782834791348

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_283 : Polynomial.coeff recurrence4B3A4 283 = (9140111395711809664422684 * 10 ^ 70 + 291132443670204696249178457604609188719456867045701131046812597404952) * 10 ^ 70 + 4434230337176717893885073714141644130105519514228539110830262761725311

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_284 : Polynomial.coeff recurrence4B3A4 284 = -((8884643199562520030909140 * 10 ^ 70 + 4458093954789086991662754579918525235352247116016669507087945321720265) * 10 ^ 70 + 5410633488087342476314979163487327272400837711192649700136732106320199)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_285 : Polynomial.coeff recurrence4B3A4 285 = (3998244856203530177734377 * 10 ^ 70 + 2901779083577325904997961231115526220232645432280001599563814331612483) * 10 ^ 70 + 2631069328038218929020752679901929295698285153024331613875668422374971

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_286 : Polynomial.coeff recurrence4B3A4 286 = -((1408470253630098014148235 * 10 ^ 70 + 8750994557069238472102636779927189773465442266143653454236131953761457) * 10 ^ 70 + 3196073471400987722488269425660002685157166495498035310746096722750199)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_287 : Polynomial.coeff recurrence4B3A4 287 = (428258357625952747276528 * 10 ^ 70 + 3764536486621471239690418852411178316626489813909612582524454914494707) * 10 ^ 70 + 9529528380789846029263039630535892458300873079025685985755037218572169

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_288 : Polynomial.coeff recurrence4B3A4 288 = -((116300705409498534090563 * 10 ^ 70 + 7085017125314787704037190246232054842953387693080178126110234001043624) * 10 ^ 70 + 7583502596225993163521785529669579172023275389184983132313992246677838)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_289 : Polynomial.coeff recurrence4B3A4 289 = (28608156234871493318699 * 10 ^ 70 + 767261803498819149191702948487076573720422311498398187747781159088678) * 10 ^ 70 + 5517071887149606453793176500575581180899283186405960539730600814270837

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_290 : Polynomial.coeff recurrence4B3A4 290 = -((6405928967319743493014 * 10 ^ 70 + 9287429287681280378986115840995624324556423002324258233783163060108979) * 10 ^ 70 + 5687212145244017320799619553242290803566504243503479133874580432320305)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_291 : Polynomial.coeff recurrence4B3A4 291 = (1304769057131996391366 * 10 ^ 70 + 9966626878345372983144566767055586372521023202318514551131537685831309) * 10 ^ 70 + 3399177275192390878702706736914750236580799303706443131805816770910579

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_292 : Polynomial.coeff recurrence4B3A4 292 = -((240311059019094910324 * 10 ^ 70 + 5637193310146192990527192742067629599238637895170858395655573402558269) * 10 ^ 70 + 4152220506676112373588314112643363780117410288128733571410014866532188)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_293 : Polynomial.coeff recurrence4B3A4 293 = (39514974651687684243 * 10 ^ 70 + 5055931627983742862510829461986283546187502740474478855164027269827214) * 10 ^ 70 + 6808146605927720021860480869011170394610161049043816523305066896108541

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_294 : Polynomial.coeff recurrence4B3A4 294 = -((5656043345917011716 * 10 ^ 70 + 4263233150444812469698093087210369611392784541139234764801305478855849) * 10 ^ 70 + 4974687592143273275483310703265178229481380917933497910175487462565850)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_295 : Polynomial.coeff recurrence4B3A4 295 = (665991139298971372 * 10 ^ 70 + 4028732943427898077403169124972652634923365194990569106944635505819364) * 10 ^ 70 + 7366239289945378505106352334199686169220368146973592685700672521682820

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_296 : Polynomial.coeff recurrence4B3A4 296 = -((54004257330386423 * 10 ^ 70 + 9347161551734269697817635729433488182215672404028276465329488543425364) * 10 ^ 70 + 4606980784716576880152620129347182619655422909961490586091213129914144)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_297 : Polynomial.coeff recurrence4B3A4 297 = -((136741486262853 * 10 ^ 70 + 8977674482003145914067677581955925543184580900139780890858734574649348) * 10 ^ 70 + 2174500561798989095053483454282159856355081472862544334978881269709966)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_298 : Polynomial.coeff recurrence4B3A4 298 = (1150270989904106 * 10 ^ 70 + 2639333639774956232884781052654498638167311202894650661263628201421055) * 10 ^ 70 + 7948943221452131649268381303302163917074865668466224777884525627413603

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_299 : Polynomial.coeff recurrence4B3A4 299 = -((282958144507157 * 10 ^ 70 + 6337877177643649318687505603214746838100564500428554788481778631930057) * 10 ^ 70 + 5366524324840866153976942937177357717441959000352873148680858564542475)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_300 : Polynomial.coeff recurrence4B3A4 300 = (46851271696355 * 10 ^ 70 + 2234107504002222160203680985299917728380589828476132290763488607594489) * 10 ^ 70 + 411274080241452282192801053865519979341625670377547651124400798993626

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_301 : Polynomial.coeff recurrence4B3A4 301 = -((6041594485685 * 10 ^ 70 + 4566960915032505885963592651487222815554816222539196399533294823046758) * 10 ^ 70 + 8986769549742720522647458451571302739762034232523131451510955442122173)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_302 : Polynomial.coeff recurrence4B3A4 302 = (617741522438 * 10 ^ 70 + 136439189067470112960599556882630156241161668469445222292958240671190) * 10 ^ 70 + 5263281108457988407162016058686180801916500155884632676398193571863208

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_303 : Polynomial.coeff recurrence4B3A4 303 = -((47636885250 * 10 ^ 70 + 8494320125946318296252682781641259487002085748207708574509601716485691) * 10 ^ 70 + 7550653743917625228143092369118778526694988208408019174060367135254475)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_304 : Polynomial.coeff recurrence4B3A4 304 = (2199903365 * 10 ^ 70 + 4367290094223103665978767515080241220364208772059997498924448466032280) * 10 ^ 70 + 293184875076534377734037113475852954989929112585428284385243609489486

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_305 : Polynomial.coeff recurrence4B3A4 305 = (47863889 * 10 ^ 70 + 4824934730033792587195132824854490800343957221760044351916063381050841) * 10 ^ 70 + 6703307812463601149119213835113167498846437395052147241124323403295939

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3A4_coeff_306 : Polynomial.coeff recurrence4B3A4 306 = -((21775099 * 10 ^ 70 + 2171295828534502549854335464459098343868065747407378191957339101618271) * 10 ^ 70 + 5156813472536362597007323732806375454419683790367382484396637869092905)