Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar0LeftPart0.Coefficients0To92

Recurrence 2 lookup certificate: Scalar0Left 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.recurrence2Scalar0Left_coeff_35 :
Polynomial.coeff recurrence2Scalar0Left 35 = -(177406253491 * 10 ^ 70 + 1237635113951222354987825585814183628280572360452039390334913490965249)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_36 :
Polynomial.coeff recurrence2Scalar0Left 36 = 4279864795246 * 10 ^ 70 + 6921979654980208397844107158956207411820779223661911950758365034887809
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_37 :
Polynomial.coeff recurrence2Scalar0Left 37 = -(33225731760475 * 10 ^ 70 + 5539078265826866517171658656544190255348911053537763033962951818829025)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_38 :
Polynomial.coeff recurrence2Scalar0Left 38 = -(3668960477240823 * 10 ^ 70 + 9077809602148792853776350545984678874099232344052750422947885483534154)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_39 :
Polynomial.coeff recurrence2Scalar0Left 39 = 268713724122282846 * 10 ^ 70 + 9807897565973869288543174362187219399531646501083538994347450499403897
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_40 :
Polynomial.coeff recurrence2Scalar0Left 40 = -(11471371979860071218 * 10 ^ 70 + 8439913658110526501476550446030084981084727587166603906090200290333756)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_41 :
Polynomial.coeff recurrence2Scalar0Left 41 = 357809400522553349979 * 10 ^ 70 + 3751189928842410862715281584024146512223628741413064242816365301116672
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_42 :
Polynomial.coeff recurrence2Scalar0Left 42 = -(8481050553256747931885 * 10 ^ 70 + 6205398359100229948335737960927128694200447428212602401386639042358093)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_43 :
Polynomial.coeff recurrence2Scalar0Left 43 = 152205641993077509983346 * 10 ^ 70 + 1349394983763224720497219768149420380287857786132353559291268393033675
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_44 :
Polynomial.coeff recurrence2Scalar0Left 44 = -(2114751204124533184420422 * 10 ^ 70 + 9037513111491942216151485637335862741307801217669512870211502057112852)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_45 :
Polynomial.coeff recurrence2Scalar0Left 45 = 32040050322500278518998991 * 10 ^ 70 + 3718453794597098028078165027128770149826304441782448075950771562163392
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_46 :
Polynomial.coeff recurrence2Scalar0Left 46 = -(994354142213647319517610002 * 10 ^ 70 + 2732193114750300997920278089151809969525284187653373735077742425254522)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_47 :
Polynomial.coeff recurrence2Scalar0Left 47 = 38501527146762792262904360839 * 10 ^ 70 + 1514718389603058757008662821897124638448426175521713199131773975546435
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_48 :
Polynomial.coeff recurrence2Scalar0Left 48 = -(1196748187328940334187669414254 * 10 ^ 70 + 6301885192505821324263803584862985156819735570194782609123555196267718)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_49 :
Polynomial.coeff recurrence2Scalar0Left 49 = 28816504541697790239472903452504 * 10 ^ 70 + 2361590647598850864458210795883839042880282223177083711207769867270
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_50 :
Polynomial.coeff recurrence2Scalar0Left 50 = -(550392451160621458718303753879402 * 10 ^ 70 + 1209893530965548551945322104603024158424295896194265739594327303222039)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_51 :
Polynomial.coeff recurrence2Scalar0Left 51 = 8451200228414815784840983345826859 * 10 ^ 70 + 652172391853756399262880896175510203867594806291501253891569156240345
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_52 :
Polynomial.coeff recurrence2Scalar0Left 52 = -(103134711568797694637539291712196774 * 10 ^ 70 + 6558019833199794139827306151367125889525706817555162134897677862406323)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_53 :
Polynomial.coeff recurrence2Scalar0Left 53 = 916846077283744152231801506149790664 * 10 ^ 70 + 8906373582401330776614984750192047968341056709102225671533009901229986
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_54 :
Polynomial.coeff recurrence2Scalar0Left 54 = -(2704845444364290362110608855429204120 * 10 ^ 70 + 9952546122443691490860595092754124832801883855266963901041025647570976)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_55 :
Polynomial.coeff recurrence2Scalar0Left 55 = -(127638082343798919815932986184937360012 * 10 ^ 70 + 1035023544862852963019895263747309853539678401967087742379905455985232)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_56 :
Polynomial.coeff recurrence2Scalar0Left 56 = 4423675762218337034244225027565308646327 * 10 ^ 70 + 3910543997635134235259171595039857268054550303379919935003080859409080
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_57 :
Polynomial.coeff recurrence2Scalar0Left 57 = -(102530232329385617442726406548446829348302 * 10 ^ 70 + 341064084751265631704163024743864363505089393608086733429826640166427)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_58 :
Polynomial.coeff recurrence2Scalar0Left 58 = 1984410836151995321588653111673124170468902 * 10 ^ 70 + 8603576728892299610133957185886920621353378491609970647024785154647568
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_59 :
Polynomial.coeff recurrence2Scalar0Left 59 = -(33543626195624401227297198479626123798233712 * 10 ^ 70 + 4138639780333512840682430565350625696337992329479917008652479030389682)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_60 :
Polynomial.coeff recurrence2Scalar0Left 60 = 505312235366690952101326716327370986993199452 * 10 ^ 70 + 5872874601714598876108214552362493753229118560001958282249123519904121
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_61 :
Polynomial.coeff recurrence2Scalar0Left 61 = -(6928429531039379077971883293929204736548735476 * 10 ^ 70 + 6026546209462256980222096740738242174104799029711684963423329514278901)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_62 :
Polynomial.coeff recurrence2Scalar0Left 62 = 88436912062491070703576415135083616524673394624 * 10 ^ 70 + 4332726429791049133236208061905211818139717655671628873528196924608322
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_63 :
Polynomial.coeff recurrence2Scalar0Left 63 = -(1061802675949130376040962844629421857269938220837 * 10 ^ 70 + 1619011475145306547971631141578053408896932515078431561602939376476509)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_64 :
Polynomial.coeff recurrence2Scalar0Left 64 = 11652278993694517042608961550970863867628205337175 * 10 ^ 70 + 1334095215160145411590252725215644299895898948932246854596486337006789
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_65 :
Polynomial.coeff recurrence2Scalar0Left 65 = -(103215442844468393128819317364232349445810394861356 * 10 ^ 70 + 4239940778119915912019351537482611934724523400362676292306672056643220)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_66 :
Polynomial.coeff recurrence2Scalar0Left 66 = 352871468680057599340295081759430730166673124656664 * 10 ^ 70 + 7363204973237216537182786397162731340302833300661108107599378550704801
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_67 :
Polynomial.coeff recurrence2Scalar0Left 67 = 13110852093429395563075148022393590211686836038546597 * 10 ^ 70 + 7990935301260852083371078669727822747334034683583166891514551294616716
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_68 :
Polynomial.coeff recurrence2Scalar0Left 68 = -(442788448834725391205752328934813741762481216156557793 * 10 ^ 70 + 5525155640311154394049075291450723188167525778353420151137585065005997)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_69 :
Polynomial.coeff recurrence2Scalar0Left 69 = 9344304402414016392007765388119396289558506663583160102 * 10 ^ 70 + 6647883206957218911531306099682173611680062699891422513304740186782696
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_70 :
Polynomial.coeff recurrence2Scalar0Left 70 = -(161383750759426451498790871784044371910000147137343152575 * 10 ^ 70 + 8063569382568313063714565627182897878976370326558623900222126984400515)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_71 :
Polynomial.coeff recurrence2Scalar0Left 71 = 2452540921443709874018411815617103441604477005735592297928 * 10 ^ 70 + 4044785931599876288148369357253093383736569480749113840725781645068987
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_72 :
Polynomial.coeff recurrence2Scalar0Left 72 = -(33843666760513230353608814782853161880683984217341572612496 * 10 ^ 70 + 2100570726028665885550573906555280992266367360740011445129720853818479)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_73 :
Polynomial.coeff recurrence2Scalar0Left 73 = 431273041176513512128156245046598324084641312247481705252603 * 10 ^ 70 + 7598017397833346877912204374124949535109387778908488051440036611843089
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_74 :
Polynomial.coeff recurrence2Scalar0Left 74 = -(5126225336572206217369879118328066561754987965938852274991262 * 10 ^ 70 + 8298971177436187443712422414095426300454351064282953152276703263329746)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_75 :
Polynomial.coeff recurrence2Scalar0Left 75 = 57201815650296199288747229708408357518109923270797835193492781 * 10 ^ 70 + 2403467332558718867804028289812551209715540075959942046429692021507029
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_76 :
Polynomial.coeff recurrence2Scalar0Left 76 = -(601906706380701402394849844489857039902065424350450109597609217 * 10 ^ 70 + 9507103583987690285665867492876885855830627720314149589482825142110822)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_77 :
Polynomial.coeff recurrence2Scalar0Left 77 = 5992804846080648589837196947543756605557928830109070296957562082 * 10 ^ 70 + 8398296537699292953286220661432003274090565683753520447325539883319100
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_78 :
Polynomial.coeff recurrence2Scalar0Left 78 = -(56614566814402987275664842744871169677943157338177595347339375656 * 10 ^ 70 + 4404845202752827961685632375375295453402803322009640632324392686163948)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_79 :
Polynomial.coeff recurrence2Scalar0Left 79 = 508713549711488869891087480496237711011050894014295713711689679973 * 10 ^ 70 + 2519538607039022688020598434648329229068252711423994585559132382038278
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_80 :
Polynomial.coeff recurrence2Scalar0Left 80 = -(4356899434067997655863831502741893113486052685119614228735359402737 * 10 ^ 70 + 948817742785910481150839034014935676662620569327619596776327679074803)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_81 :
Polynomial.coeff recurrence2Scalar0Left 81 = 35629916650068479137669189873503294788257897361975997570043435443220 * 10 ^ 70 + 937979231247454189543490132624820751214930737574314852508932128389149
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_82 :
Polynomial.coeff recurrence2Scalar0Left 82 = -(278624689968233956536027564898029623109804514065734671769123729142142 * 10 ^ 70 + 294175682989545861402824947564954391033517415805823581948080099170113)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_83 :
Polynomial.coeff recurrence2Scalar0Left 83 = 2085925219161809944960738605922620640667871278472765218935674335085293 * 10 ^ 70 + 6767547647037446690667120520329644902823181389510705446454302614728378
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_84 :
Polynomial.coeff recurrence2Scalar0Left 84 = -((1 * 10 ^ 70 + 4964363725205963783277700993390474539764523040539562799339888691478889) * 10 ^ 70 + 1962382030656577231460989106035453350139528654161429282811639830802555)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_85 :
Polynomial.coeff recurrence2Scalar0Left 85 = (10 * 10 ^ 70 + 2952743125587399802397106513748494611012729398347514370282712770818669) * 10 ^ 70 + 6668998521667574460589585696462211400292903596766050461224565336502969
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_86 :
Polynomial.coeff recurrence2Scalar0Left 86 = -((67 * 10 ^ 70 + 9737612510315305648739229503015613104353777084703196556880006799106973) * 10 ^ 70 + 460325695379915097807014952020398467677959535703780321300266155413988)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_87 :
Polynomial.coeff recurrence2Scalar0Left 87 = (430 * 10 ^ 70 + 9731391557131688497476727534881178566168862612434716311954908141660735) * 10 ^ 70 + 9400074694035349261080564711803234813023372842216141125557016988614245
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_88 :
Polynomial.coeff recurrence2Scalar0Left 88 = -((2625 * 10 ^ 70 + 5350523266271620822872088547544549665027036719991061355926540779878222) * 10 ^ 70 + 8009588348352044232021712532635597986376721915319557620344130259006784)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_89 :
Polynomial.coeff recurrence2Scalar0Left 89 = (15375 * 10 ^ 70 + 9999759710795671165926441566733965763236895171486691443582616449196900) * 10 ^ 70 + 7205600500989521441797838056792095018890248523537429371977212039568896
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_90 :
Polynomial.coeff recurrence2Scalar0Left 90 = -((86584 * 10 ^ 70 + 3848698145889991291621194615694204863455730394677736389774852927913636) * 10 ^ 70 + 4104340357070913429846876034633975931121637739047618905187123803770189)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_91 :
Polynomial.coeff recurrence2Scalar0Left 91 = (468823 * 10 ^ 70 + 4837785397987378797127782508266466719009594656720752799261439768088093) * 10 ^ 70 + 4344389338693163254153159132199700402190331605442510413258950020796674
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_92 :
Polynomial.coeff recurrence2Scalar0Left 92 = -((2440315 * 10 ^ 70 + 833658571038974490589122897525076362820805031548906776876130638130059) * 10 ^ 70 + 7906139608984540611205934494313511195574628857397442773336285703542873)