Recurrence 5 lookup certificate: B2A3 coefficient convolution

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_146 : Polynomial.coeff recurrence5B2A3 146 = ((53004408474654000522 * 10 ^ 70 + 9611925827463304631259607920592550212110385238695884822988485853715405) * 10 ^ 70 + 8363249434209960066376833547331526482403277669120088399250310175558818) * 10 ^ 70 + 7638906587065482330097590106657657368990183769606574003186262685908669

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_147 : Polynomial.coeff recurrence5B2A3 147 = -(((29096292211474475296 * 10 ^ 70 + 7995395455862421799620424308556576681726967162858009151072109886870227) * 10 ^ 70 + 2452368097610724452498160421180639011728583169759208837522353401243654) * 10 ^ 70 + 9081468877072577081150571615767587425983348096642318608005121047754502)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_148 : Polynomial.coeff recurrence5B2A3 148 = ((7998061486996811739 * 10 ^ 70 + 5970116549663901476634124928338779314238051669555229971510569828421100) * 10 ^ 70 + 1752635513483929079870733529178422184386819782443593038251762053947635) * 10 ^ 70 + 6069053840702116929421965734255470228718765317747783027686863916847972

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_149 : Polynomial.coeff recurrence5B2A3 149 = ((9292253853043611941 * 10 ^ 70 + 4126640789505515014455088339428447657316898297875389164229703446551006) * 10 ^ 70 + 4205492434181869306396108664927852040067423861371389559843014253638515) * 10 ^ 70 + 1148071367750654175445103871842545176333758916506603250684135596988842

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_150 : Polynomial.coeff recurrence5B2A3 150 = -(((22246061320683474256 * 10 ^ 70 + 5393668794547888729454947044210143564376071395732400603276429693997845) * 10 ^ 70 + 3278040113019386257273303231487459269338772814209656594109510861625449) * 10 ^ 70 + 4624655591724150992522039412224725505515894164981709423344357174715219)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_151 : Polynomial.coeff recurrence5B2A3 151 = ((30799218932177135680 * 10 ^ 70 + 3657011985011052484516580820163170749826102773150414082499733915962127) * 10 ^ 70 + 9640341814901306290078182266270081156421633764949769026442555988990881) * 10 ^ 70 + 2326476516003671517556055544850354394284603610385058742930841884954008

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_152 : Polynomial.coeff recurrence5B2A3 152 = -(((35286649927210064780 * 10 ^ 70 + 5938946968749822792007080395809881037549378071256546389681648837344232) * 10 ^ 70 + 3379844652405196851259849737670536688348392252154332805462928811523658) * 10 ^ 70 + 8276295097462668905337868891017938280838384187307670278384865103203133)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_153 : Polynomial.coeff recurrence5B2A3 153 = ((36335367073180564643 * 10 ^ 70 + 8740709800868203458260526885325822454776542085697438869002026722070825) * 10 ^ 70 + 3640468637505278027722624459650328232871656346019787515226151416674011) * 10 ^ 70 + 354743640205397931865262017943473960154870645587077069116366758693245

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_154 : Polynomial.coeff recurrence5B2A3 154 = -(((34739001830002142541 * 10 ^ 70 + 3818093932589611276999254814768848368654906929977741899261727878885447) * 10 ^ 70 + 1287023963832946808026087150321068942758686076682323873293375640999817) * 10 ^ 70 + 3908646535344506889450701716392722297707261226206152716599365946595273)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_155 : Polynomial.coeff recurrence5B2A3 155 = ((31336077637203017449 * 10 ^ 70 + 7341781580359141129220286914673216554953620153855359124552427894044392) * 10 ^ 70 + 7992097449119862558512729698057320291968418683003182964491963142320765) * 10 ^ 70 + 7032173330283439057827381038382605548217249228882921611669148441898735

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_156 : Polynomial.coeff recurrence5B2A3 156 = -(((26909320986093728586 * 10 ^ 70 + 7066826604975513389862074553488395034637803833621632085441957375062524) * 10 ^ 70 + 4876604160832371609060453624539476105781423562653543046546300106927094) * 10 ^ 70 + 2899833847335148541346283485289052516742666703693083727437294103975477)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_157 : Polynomial.coeff recurrence5B2A3 157 = ((22116083193368037019 * 10 ^ 70 + 2026194478705153771452642752092938405657763900070086733726268838078882) * 10 ^ 70 + 3013422084451034421510286205043346989723617886346172655164015562014163) * 10 ^ 70 + 2427938047550740087938582762171900802109125265977705710637088259129038

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_158 : Polynomial.coeff recurrence5B2A3 158 = -(((17452429389069999126 * 10 ^ 70 + 9968120860454475721053490833139574943119450663691138648790743560394332) * 10 ^ 70 + 9298798142884233380352125669502636943089223771163022008936793767871471) * 10 ^ 70 + 5131180149512333553488398338612461062182157557921678881657487603809099)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_159 : Polynomial.coeff recurrence5B2A3 159 = ((13247258230331290438 * 10 ^ 70 + 8716252619227681912813221021675071468597523484599286534754522006805207) * 10 ^ 70 + 7287755064554322192497297257890291037860565531302175010385291302330802) * 10 ^ 70 + 2273620631099091691770366320711232910060438501075297474095546246651996

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_160 : Polynomial.coeff recurrence5B2A3 160 = -(((9678886761559339602 * 10 ^ 70 + 5378004227993245050878129836532425238062389942396156436417489371305939) * 10 ^ 70 + 9522460634210852545760406580390157778008547757229344070555787549979933) * 10 ^ 70 + 1665119423699917090012656838575620213701304981948321781190290036700438)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_161 : Polynomial.coeff recurrence5B2A3 161 = ((6805066291257012977 * 10 ^ 70 + 7335403242129249112330335878309475609075967950191529975087126611599468) * 10 ^ 70 + 6001989362806831429383138415792077157436639665900651049451419301042339) * 10 ^ 70 + 3696276529982583461612954487572260639265892513524524648726289065302934

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_162 : Polynomial.coeff recurrence5B2A3 162 = -(((4597985963462190791 * 10 ^ 70 + 2998370441604750016804977865580698293928875272387847360840210762129320) * 10 ^ 70 + 2128150842778610627494369571484436692868860064287990026313181262442785) * 10 ^ 70 + 6227388048424001071341417976218755806977783022992893560510375835440445)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_163 : Polynomial.coeff recurrence5B2A3 163 = ((2977734495562014044 * 10 ^ 70 + 2219350957692283305333716182994404456026553244265870779068348399957940) * 10 ^ 70 + 8873329847634508687723418370097065362066729363770365387713021283952062) * 10 ^ 70 + 758952129534051167051828438124372648527804370767957088745184160029385

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_164 : Polynomial.coeff recurrence5B2A3 164 = -(((1840130105970638463 * 10 ^ 70 + 3556226536370025712746031159984295450081583175123552219770259150969334) * 10 ^ 70 + 7271201233269408297348876391809424029772474549449166440424272935133546) * 10 ^ 70 + 4142970868343618640813478031711842994540973318124595157545597995567222)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_165 : Polynomial.coeff recurrence5B2A3 165 = ((1077142817055600210 * 10 ^ 70 + 870942636855391358285495946195376735149155116078965401257354313713951) * 10 ^ 70 + 139684888531211163645507811212437719040713224824340459209092464049678) * 10 ^ 70 + 5922344635584405042124016944167592343729481189854456451103132313451389

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_166 : Polynomial.coeff recurrence5B2A3 166 = -(((589920634810582804 * 10 ^ 70 + 1151869042895778006487792722750827752290959688008624347539107679189918) * 10 ^ 70 + 8465422673372832673746516591830866850800130061255333253786587170630038) * 10 ^ 70 + 1262740223100332872056176381604860799088126011562202157847120247814918)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_167 : Polynomial.coeff recurrence5B2A3 167 = ((295545544826960237 * 10 ^ 70 + 8375620061028405855117471097061350670942833509776737421426214323911089) * 10 ^ 70 + 298241592303852818995336422122648306295200596273973919252085749474534) * 10 ^ 70 + 1025529250621122583735789808607121961433540641074868308758358297861270

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_168 : Polynomial.coeff recurrence5B2A3 168 = -(((129136069238719625 * 10 ^ 70 + 7708970947275021209986305932267016744811256903160017608979692868603595) * 10 ^ 70 + 9979124016007845442110627114082003858825567878035916508660401028677999) * 10 ^ 70 + 4115409904970844740097236596980621980956156576343568165568354500442443)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_169 : Polynomial.coeff recurrence5B2A3 169 = ((42938663291851582 * 10 ^ 70 + 5507558784369621861603878526077763516388425726368231127393203099175687) * 10 ^ 70 + 5687533966665894206581873776251464169300028471616984972233302506004716) * 10 ^ 70 + 5552409958568118963546305498693136248779983694163375230668387305577826

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_170 : Polynomial.coeff recurrence5B2A3 170 = -(((3798591993263922 * 10 ^ 70 + 1101732191987322226469965983307747779637821134300261239624407620183468) * 10 ^ 70 + 5733310552205879610872571344915887491924366732187945078862297562308506) * 10 ^ 70 + 9939740150625794618245420056660383104732261259740267272036977640275721)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_171 : Polynomial.coeff recurrence5B2A3 171 = -(((9964290086495450 * 10 ^ 70 + 4886812379638302480619127111432388309277600916234528634502517520262377) * 10 ^ 70 + 7511155888245078047700499959315953487779370432595060955103399151578186) * 10 ^ 70 + 614647900210431634269262398170818269553738438058024728593794132508815)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_172 : Polynomial.coeff recurrence5B2A3 172 = ((11614347209406440 * 10 ^ 70 + 7467903802161495642947840273525598629847355584605485052421321608947728) * 10 ^ 70 + 7750694660746558239119792322541372818965083261145835116194372650181773) * 10 ^ 70 + 1427685171878184573629022825785351746572473803848431925862248247980085

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_173 : Polynomial.coeff recurrence5B2A3 173 = -(((8635590250451800 * 10 ^ 70 + 1748517495855765187778672329619050379208419328790435714073641970378097) * 10 ^ 70 + 8362817079015011443204075306313803799761894826357163647541981113541434) * 10 ^ 70 + 9709728004399398187399266899794296227036172443270280551564255972200077)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_174 : Polynomial.coeff recurrence5B2A3 174 = ((4804518517760279 * 10 ^ 70 + 3719427902249051769984849148593519220559198539507836892732511436856961) * 10 ^ 70 + 7645869161216947011962984640767164852127514592103138952850871917689413) * 10 ^ 70 + 8434622767078863414054119311680898669403749711261369627651315853830431

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_175 : Polynomial.coeff recurrence5B2A3 175 = -(((1700153944919593 * 10 ^ 70 + 1303228751228143154972789103399999704644353472736512125836102183673238) * 10 ^ 70 + 3596346141986460874338078584853323768625561553625083253840308792614132) * 10 ^ 70 + 6066040642171526218556771852857617918414332117579906055363831850394492)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_176 : Polynomial.coeff recurrence5B2A3 176 = -(((273807457213637 * 10 ^ 70 + 9533587877892804150006033595874274282992427754880542822431311742172662) * 10 ^ 70 + 3272566500350764975255731090323661083808506230281214333654004593191879) * 10 ^ 70 + 1544031702402574943366875376097273972673202590701346170512831396219438)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_177 : Polynomial.coeff recurrence5B2A3 177 = ((1249746337629726 * 10 ^ 70 + 3251305464378004495496934902177216395473189086886848387695994059172227) * 10 ^ 70 + 7676206281752787194539439557636675472072396621861014592672334717577478) * 10 ^ 70 + 8556870559122917861906268726490850700864648955720523566261390184635516

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_178 : Polynomial.coeff recurrence5B2A3 178 = -(((1533122808269340 * 10 ^ 70 + 3039941496092612657966023249803460431997857211763442687004985087908440) * 10 ^ 70 + 7032365459016582136140395929379203143378120027935148859446144319665775) * 10 ^ 70 + 7212075808283725070924919466075255726987066409072228199962497891941729)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_179 : Polynomial.coeff recurrence5B2A3 179 = ((1422895393243076 * 10 ^ 70 + 1060655786634562774186528664415067553332401562923037936283562397203627) * 10 ^ 70 + 4511328209314206838238331445387295206132438904548510391085017153157230) * 10 ^ 70 + 9350257909828823085519090602960879992475667469044728445891170983450390

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_180 : Polynomial.coeff recurrence5B2A3 180 = -(((1142780404012983 * 10 ^ 70 + 1868106735158263860236220093201600789951923427098617896352405923405576) * 10 ^ 70 + 1662588401541691395456451152217384148378782724650789469670493666163239) * 10 ^ 70 + 8435987974335600761052915172794059133190547547994745085802108313853825)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_181 : Polynomial.coeff recurrence5B2A3 181 = ((831692892770933 * 10 ^ 70 + 9838406854555735707307116055137756715977769977821716451184225308698500) * 10 ^ 70 + 5713730819445154502097407353070204348915202391509385058112553754589470) * 10 ^ 70 + 7874784021722173901274362381969889969220893823906184163454345481825717

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_182 : Polynomial.coeff recurrence5B2A3 182 = -(((559996543992191 * 10 ^ 70 + 2137880438968606639565601097837948926481344843499177733692622839504454) * 10 ^ 70 + 3188598713540091255718969877813515485582376937531081626384534944339593) * 10 ^ 70 + 8181964433682236648926969864747116148463943979765949881198291383739229)