Recurrence 2 lookup certificate: Scalar4Exceptional coefficient convolution #
This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_199 :
Polynomial.coeff recurrence2Scalar4Exceptional 199 = (971418756180957101299512599038572722132966319218807262192 * 10 ^ 70 + 4465670658807102221860822282011563137166673542812656202806004602578661) * 10 ^ 70 + 3989161024549999633222128039500713466977639121053753180771064390579796
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_200 :
Polynomial.coeff recurrence2Scalar4Exceptional 200 = -((2051659938405932514795905238730171107973950336276057282072 * 10 ^ 70 + 3453202077198186703125595197621912303190074476030696474925461501853701) * 10 ^ 70 + 6285432695776831354380930772268941944562768188127523449784212612432633)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_201 :
Polynomial.coeff recurrence2Scalar4Exceptional 201 = (3522330384359744972281087240950861426186346301733842341836 * 10 ^ 70 + 258900584470586621361324409289564698878131136909439671463822951683408) * 10 ^ 70 + 456364465764334085451505761233369223552810631613567148373512509268934
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_202 :
Polynomial.coeff recurrence2Scalar4Exceptional 202 = -((5286840845243382193652705389759854702617079888339165094514 * 10 ^ 70 + 5008476882234783757270810253787357541598281050955677341416018368376227) * 10 ^ 70 + 7676689783777010061567088154122139599116521435855343267943503897635403)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_203 :
Polynomial.coeff recurrence2Scalar4Exceptional 203 = (7122561807244533584703748027190165742204744452527023701411 * 10 ^ 70 + 5954013255641203648862783486318453701152263775809245216939489193167790) * 10 ^ 70 + 7608654629809249781123740255992647846360222793985689201101987159738359
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_204 :
Polynomial.coeff recurrence2Scalar4Exceptional 204 = -((8683482250700695774933797174154434518837714295302252030450 * 10 ^ 70 + 6676138695782130926958597601031999811944783656165430913311574333457642) * 10 ^ 70 + 1941245591930598508855724500916095364571979607449399198855998511987672)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_205 :
Polynomial.coeff recurrence2Scalar4Exceptional 205 = (9541622888045400482724027187639224223100380547355407571831 * 10 ^ 70 + 4054502829921648682898941310508073646067116881386492231840835553311825) * 10 ^ 70 + 8005278154951915802762999866113269077451826277613910826268696386235100
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_206 :
Polynomial.coeff recurrence2Scalar4Exceptional 206 = -((9268605263099206561811066987499165749154736045435978528040 * 10 ^ 70 + 5984547302203980831262278650106577065705107003173781691084674837093744) * 10 ^ 70 + 7501659314678330665166867491103581693119559681663430794814799850146164)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_207 :
Polynomial.coeff recurrence2Scalar4Exceptional 207 = (7545093881043087290914634183830861911880494892548254445055 * 10 ^ 70 + 4179492837785865483029216408547828321871185326939415779226964011716950) * 10 ^ 70 + 2765819486462297580523780901108149460333942930100807187987684701889545
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_208 :
Polynomial.coeff recurrence2Scalar4Exceptional 208 = -((4272306715210433442484308872735424477047109817493192467111 * 10 ^ 70 + 269666175428778691315990942112797595335231434355703445565279376489157) * 10 ^ 70 + 3894051175330011326232772061527871447383148308727336025348920043580305)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_209 :
Polynomial.coeff recurrence2Scalar4Exceptional 209 = -((348135611787495140812079446480913018284653604059776376065 * 10 ^ 70 + 8965328951880209472715033720954310919718859454072478519965921071991266) * 10 ^ 70 + 8726693718332823775683931373661386709862422357381575162604995216902515)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_210 :
Polynomial.coeff recurrence2Scalar4Exceptional 210 = (5797499422059624264665567766971807002941017433622657724582 * 10 ^ 70 + 2353721756925689333253146236165143804812725256810111012109936859803450) * 10 ^ 70 + 1103929303879882200101659206734693720351558702966548005581619275146358
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_211 :
Polynomial.coeff recurrence2Scalar4Exceptional 211 = -((11303921384775451023876799450134094119699238613837056807654 * 10 ^ 70 + 1404413802688975028132497198774975948300541156832573951811461594289917) * 10 ^ 70 + 3991752104867119758485634281804661558155533737938850172735567673815115)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_212 :
Polynomial.coeff recurrence2Scalar4Exceptional 212 = (15981973015726569468511661300433570967338387075577045136778 * 10 ^ 70 + 4290061251382911833844639859244316365919852228979259778927304159798213) * 10 ^ 70 + 7370543345497513223430293317143612673742779791274143402856792641775010
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_213 :
Polynomial.coeff recurrence2Scalar4Exceptional 213 = -((19018218408017571183934081154745843615292065405605147130175 * 10 ^ 70 + 2054977771154128360929412047136450889703477291616332394918800294904304) * 10 ^ 70 + 284738124199596708120728757800617601844235319373491014121419234255498)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_214 :
Polynomial.coeff recurrence2Scalar4Exceptional 214 = (19855579923513743746291350177681090057744836027476694800346 * 10 ^ 70 + 4979682420646924411526772731965448805182876378705781939325296199672842) * 10 ^ 70 + 6339116182863835441016423373845435079529960831597798963248441895962801
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_215 :
Polynomial.coeff recurrence2Scalar4Exceptional 215 = -((18325680133337420662329403676992757014404031373825651808765 * 10 ^ 70 + 7358946642099168737201457193682191479196826611363671109495390050622676) * 10 ^ 70 + 4653886366759708591007521817950743536992600747998469353164882508936721)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_216 :
Polynomial.coeff recurrence2Scalar4Exceptional 216 = (14691045649607999784326371017787007355760205088889332654576 * 10 ^ 70 + 8194239976256917378442701680239241071613920687384956514944766437129215) * 10 ^ 70 + 1054979057390052838903739333584698297827409183809704695351459267954904
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_217 :
Polynomial.coeff recurrence2Scalar4Exceptional 217 = -((9584566060753889679357543140180253504725830325122748494091 * 10 ^ 70 + 9584736767781182590535257797371868806873247977562013353921255535155324) * 10 ^ 70 + 3907313687324623426607847004159751055403513070329942690783991299028913)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_218 :
Polynomial.coeff recurrence2Scalar4Exceptional 218 = (3863454284969980283377188096789395655490692622981033804189 * 10 ^ 70 + 2089067876185165996302626800679717802329050962010298577296477002230905) * 10 ^ 70 + 8742965028868003520614332032549443220235052816637008745687615315212611
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_219 :
Polynomial.coeff recurrence2Scalar4Exceptional 219 = (1580980924797705480744710123791640071368909661645928936646 * 10 ^ 70 + 5171923365514235818822107623220815863604107745850226286333930859001368) * 10 ^ 70 + 979819724811744241862221220768269495233062069376857438525010666748819
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_220 :
Polynomial.coeff recurrence2Scalar4Exceptional 220 = -((6006077437941323644480685065930613794457795717558526850884 * 10 ^ 70 + 6531938385924799664656054505760662860015523068774365700578319547806095) * 10 ^ 70 + 5096634436464637133573754594317006406580752854096948984362414020579760)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_221 :
Polynomial.coeff recurrence2Scalar4Exceptional 221 = (8947480312828402986922632891180827522608485628562376042751 * 10 ^ 70 + 5036139825141760313643814480927780892384772363738270583915993294771204) * 10 ^ 70 + 8079594822625272429174392632734867001884047793638526270870383061582242
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_222 :
Polynomial.coeff recurrence2Scalar4Exceptional 222 = -((10269423319194229880520883326404986677704385614345727049125 * 10 ^ 70 + 7734646404203192577095278503144226846399676558165713268768023044120988) * 10 ^ 70 + 3319773626819006172356894364463676348304474880624802768509348577347212)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_223 :
Polynomial.coeff recurrence2Scalar4Exceptional 223 = (10134321802662813010263617223579950786128638634082267663589 * 10 ^ 70 + 4708265686835933925815015844293692431047119773917405389093860856058307) * 10 ^ 70 + 4897573822650027085357345794974237496082145330950458509388629748716239
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_224 :
Polynomial.coeff recurrence2Scalar4Exceptional 224 = -((8912369251311182115322244623456193040099545239745026970485 * 10 ^ 70 + 8321390072064130037180680202239782893264882753702245180823182241831485) * 10 ^ 70 + 437475997810214965099275196231361696204928775609828963939337718888007)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_225 :
Polynomial.coeff recurrence2Scalar4Exceptional 225 = (7064322422984259091895334622238664619606426463937167799438 * 10 ^ 70 + 9609885381130153001339250944355526244695293228710929078381612639480815) * 10 ^ 70 + 9084674728125521208330596495967670772976390714335163408887585195212069
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_226 :
Polynomial.coeff recurrence2Scalar4Exceptional 226 = -((5031313772558879349981628386535455786204448899318672914174 * 10 ^ 70 + 2976715810083566383777710939794399340065602792732540867395987199157881) * 10 ^ 70 + 1957553941836871392082621265583211986797513076964538277807201973015973)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_227 :
Polynomial.coeff recurrence2Scalar4Exceptional 227 = (3156363147052915624012906863003185055262887260065674140895 * 10 ^ 70 + 8609266369692650102598413020150336552371446613346827386349738884823792) * 10 ^ 70 + 174110153319859106957932739352163813460738844078898243080541124752205
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_228 :
Polynomial.coeff recurrence2Scalar4Exceptional 228 = -((1648135293194997571158356728926270553708745901875360116580 * 10 ^ 70 + 7151288392580466252009797596175441907259244726597418579240271191143970) * 10 ^ 70 + 5827610989374421678765136566130910428557903019624231496134517052091211)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Exceptional_coeff_229 :
Polynomial.coeff recurrence2Scalar4Exceptional 229 = (583838539178580256363199143168787037339531171033897062861 * 10 ^ 70 + 7781555156541236594691950136884195805206009298144324678464574287152015) * 10 ^ 70 + 6103476088269012072772662329227010176865543517602031482644930218382484