Recurrence 4 lookup certificate: Scalar1Exceptional 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.recurrence4Scalar1Exceptional_coeff_161 : Polynomial.coeff recurrence4Scalar1Exceptional 161 = -(((7438964948299108939445774825748553312527102567561266544571186154127004 * 10 ^ 70 + 6290776117320429500986614576960335299119684427336421436304599133623256) * 10 ^ 70 + 5050175829624821554218657270005244812686288229842975654416727458452438) * 10 ^ 70 + 8824009763601847179115664293481285514365255725616444903087178660330334)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_162 : Polynomial.coeff recurrence4Scalar1Exceptional 162 = (((3 * 10 ^ 70 + 1363564451929773600693806796189040700201585097823730084285682631880993) * 10 ^ 70 + 9079482386936385240210531519127132044711056231605045543875475095414927) * 10 ^ 70 + 5801606919564139270296248565898853933808404367387371757285571279184945) * 10 ^ 70 + 5037402920409890879996960922840881450603505377196611008021146830405538

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_163 : Polynomial.coeff recurrence4Scalar1Exceptional 163 = -((((12 * 10 ^ 70 + 9252648849833535158123183917211031940008273107098557643027992520005121) * 10 ^ 70 + 4169691211833969287480673653682018300657165782456885124226126635031736) * 10 ^ 70 + 7242869360164745077066210700762016094107525693395167792326480117955494) * 10 ^ 70 + 9631645121857877815521348337407579246538342507108338331331067277940027)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_164 : Polynomial.coeff recurrence4Scalar1Exceptional 164 = (((52 * 10 ^ 70 + 1068320060821841982563519113055400177282750103639817504589859548324415) * 10 ^ 70 + 3926069556028659212909079483104559084416116282288731864271752871489195) * 10 ^ 70 + 3206786806002757962541138793029043751700394911305559818702180133027345) * 10 ^ 70 + 7285472322079783733071408773279812525129912408186401097169000559766569

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_165 : Polynomial.coeff recurrence4Scalar1Exceptional 165 = -((((205 * 10 ^ 70 + 6283366366365814058231721049967591893574872905320780653617461211118894) * 10 ^ 70 + 6083532299939260660086520205708483367071066529071103584143258128010250) * 10 ^ 70 + 5447018558964992413140498721234423267837324634787609060911555295985366) * 10 ^ 70 + 3671072427291044838367952317231620633330960550874933204447081707513586)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_166 : Polynomial.coeff recurrence4Scalar1Exceptional 166 = (((794 * 10 ^ 70 + 7999983837753211047611038792919161983527026908205473466878455079709543) * 10 ^ 70 + 4273571933292225008221942496200029240436596656151979416645274905880309) * 10 ^ 70 + 5823896575877052799169733587947285264271132428496553447959132862008461) * 10 ^ 70 + 2727848970115899831437990019127425876957707632071210700161557139781592

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_167 : Polynomial.coeff recurrence4Scalar1Exceptional 167 = -((((3010 * 10 ^ 70 + 5223070554354595993495862419736152430896352775217802526770699418023718) * 10 ^ 70 + 2510873893723705114231559355936962157899070353195639585429012845592716) * 10 ^ 70 + 4416314559862025114092512658449162272896985557032737444074561760332439) * 10 ^ 70 + 6160505099752697499034778105673547702502848379518634884944475697024419)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_168 : Polynomial.coeff recurrence4Scalar1Exceptional 168 = (((11179 * 10 ^ 70 + 7476057647532745538514761008329270916988361849280202999750385067370129) * 10 ^ 70 + 7356680891605717732660340891475278956630566130391595099256028230912722) * 10 ^ 70 + 7316259994310957252332748685901075458868349776006953824441499869152825) * 10 ^ 70 + 460966893697431959896762156399640250043951398697893473480700372355285

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_169 : Polynomial.coeff recurrence4Scalar1Exceptional 169 = -((((40719 * 10 ^ 70 + 6721515551779084350101809043150587210028956125491007142061874994408612) * 10 ^ 70 + 8083332643594246465442965156611250833241551737014197710268298901669993) * 10 ^ 70 + 688127687438139855498285981782240175644971988322149717108371543070758) * 10 ^ 70 + 2234018860980991142051995151296125858863660489321364491225530412311032)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_170 : Polynomial.coeff recurrence4Scalar1Exceptional 170 = (((145518 * 10 ^ 70 + 796015193231556512052104612986119262924000425099698588635286727249088) * 10 ^ 70 + 8694091417367398136285503858708659168025303081102975336985925245091015) * 10 ^ 70 + 2537871584236222742246978135646220624849297195524515187550792867357130) * 10 ^ 70 + 7850630187116786525854422726810903408035547102939378224810731507332847

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_171 : Polynomial.coeff recurrence4Scalar1Exceptional 171 = -((((510403 * 10 ^ 70 + 1687815335865052082530613394857167814450069816814049184553617808357581) * 10 ^ 70 + 4693337749292881331402453841916286369321776512173851110590902312977802) * 10 ^ 70 + 1193889536363344706658382352430024169195233795103925948649423183110878) * 10 ^ 70 + 8035420806056872070070026677022994328143981779075576239720664745179974)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_172 : Polynomial.coeff recurrence4Scalar1Exceptional 172 = (((1757616 * 10 ^ 70 + 1313326992839288674311728711638413764934476352668289637055841107643844) * 10 ^ 70 + 6999825939171911145901304567615496908936261008705798939916191213185350) * 10 ^ 70 + 1416965734725870765608281253601886719986269868712042616629254800093632) * 10 ^ 70 + 5235564788281859153823733113684450852899899799150393504831783252006622

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_173 : Polynomial.coeff recurrence4Scalar1Exceptional 173 = -((((5943858 * 10 ^ 70 + 8847804968042767810875540181922795804435788665994661264340934936141271) * 10 ^ 70 + 943501467835154236034780647864125043285143719411258191850951711951967) * 10 ^ 70 + 873429764943098233812758876345181796683247005887051402993392453150304) * 10 ^ 70 + 1387580019352011078673823759802483899774965448323318534905005818445814)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_174 : Polynomial.coeff recurrence4Scalar1Exceptional 174 = (((19744981 * 10 ^ 70 + 4854957278864137619656728110125926611944792546064637454041580051596234) * 10 ^ 70 + 309270751373891299890994052725990993101319396716970334144627335475578) * 10 ^ 70 + 6202443257602156364291871407078707539205311092306879025116470850886516) * 10 ^ 70 + 6137611855007491036277626017308198807578306488712425806667937596896359

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_175 : Polynomial.coeff recurrence4Scalar1Exceptional 175 = -((((64445174 * 10 ^ 70 + 7092464820502279284357775706118787813093234482110838363656710767374581) * 10 ^ 70 + 2035589556844066977644708788042342754946623422648473589715765710022566) * 10 ^ 70 + 5491397041078857685705041562457576919911697043774712850275923994188037) * 10 ^ 70 + 724343966868803552114699657268222266082272360291574500033539595991532)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_176 : Polynomial.coeff recurrence4Scalar1Exceptional 176 = (((206711120 * 10 ^ 70 + 9175733865413021509842234836493427785931873073513143516762777960713058) * 10 ^ 70 + 8794891701250073875320023959691832977728530888530617863613983407793861) * 10 ^ 70 + 8913455262298091327806153155244094958216794553632642154756027607536628) * 10 ^ 70 + 3313101166158743143228540659331264363141028380616123470719966098437335

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_177 : Polynomial.coeff recurrence4Scalar1Exceptional 177 = -((((651725768 * 10 ^ 70 + 3324897709904161733548219012201094447339143611527194481221632773761911) * 10 ^ 70 + 7012546372483292489349731354104536212481394142967510564861425125406220) * 10 ^ 70 + 1081632961768068502023538012875094192766136258835339612190748587179960) * 10 ^ 70 + 780204353366687063222990073014799462585046059877763208087279778099528)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_178 : Polynomial.coeff recurrence4Scalar1Exceptional 178 = (((2020112948 * 10 ^ 70 + 5460157049141198767020045927583815496749545749040895780381854133558109) * 10 ^ 70 + 5235538523917783721086312367078628583803889634973178117698489385847874) * 10 ^ 70 + 6671544349350398533226409489309104926061864373265301400298841824055824) * 10 ^ 70 + 2929853707871445862567522930626980807408091909362847506938214107826804

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_179 : Polynomial.coeff recurrence4Scalar1Exceptional 179 = -((((6157055540 * 10 ^ 70 + 6607086122235701833654608495742161752260760226905507231795413728125114) * 10 ^ 70 + 6285151884295080362916006509678515266706053584943003240146235484166099) * 10 ^ 70 + 9019781956107537234221595775303946015999211294796123985365198420326464) * 10 ^ 70 + 3920861332001046404153599253056497178829455985213161861715109622985613)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_180 : Polynomial.coeff recurrence4Scalar1Exceptional 180 = (((18455655722 * 10 ^ 70 + 4045330081579088003778830876301869192246637944894645943662130048188481) * 10 ^ 70 + 7178153703566813172078823680649786854786961987667139462195890307179095) * 10 ^ 70 + 5676465316020677736247697578082975894144883104109498268865005996209310) * 10 ^ 70 + 7498811251958810593232118818048610500484976493999499137447345145600041

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_181 : Polynomial.coeff recurrence4Scalar1Exceptional 181 = -((((54414299582 * 10 ^ 70 + 9043926116934853322694043729609931163251728058729158256672934206424403) * 10 ^ 70 + 1248111700669973336583941814257022056091031380295470642234977657465986) * 10 ^ 70 + 447066216777542602338955773350567050492202989093655550882018929601227) * 10 ^ 70 + 1718620820145336521416231718968383610226253180196564944502147934879724)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_182 : Polynomial.coeff recurrence4Scalar1Exceptional 182 = (((157829489121 * 10 ^ 70 + 1469001873579943117442770330785935826663905207265413179780070125752250) * 10 ^ 70 + 8027985091038400519932118113730622240125729646883797080916680439845786) * 10 ^ 70 + 3582622903789392975783481635188884581459694096624338915309854141337953) * 10 ^ 70 + 4857736834758219211339537427819991200410132777788461702354808509716286