Recurrence 5 lookup certificate: LeadingSquare 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.recurrence5LeadingSquare_coeff_188 :
Polynomial.coeff recurrence5LeadingSquare 188 = -(((57305697164852468745897396574251 * 10 ^ 70 + 8536540842346309279154144086400067772278270501772690953446170442796367) * 10 ^ 70 + 9381810029238834776882118635213418195635582994435229187214962529635630) * 10 ^ 70 + 9829441148395651582962173443193867135649412017262941482196052300131110)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_189 :
Polynomial.coeff recurrence5LeadingSquare 189 = ((109415433767492921484401829492976 * 10 ^ 70 + 9466003016425338174055725158692667301088852439514267675406443471478551) * 10 ^ 70 + 3762558631473380099234593513848349489246460766761713170293094921588577) * 10 ^ 70 + 8280722152329515743525974277388666828046091196961963589959322921071648
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_190 :
Polynomial.coeff recurrence5LeadingSquare 190 = -(((46771800549827266353163172634838 * 10 ^ 70 + 6104624482616314469036113274895200074706453023796327427868124826897633) * 10 ^ 70 + 3488923469880891157767347781162631885318397170990192378981357505332718) * 10 ^ 70 + 7359789764964832455756070690319859400950409525094939156856129544573870)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_191 :
Polynomial.coeff recurrence5LeadingSquare 191 = -(((1518218411610012736610964251804 * 10 ^ 70 + 857504151331239220892587356727778367571078301325235292559993977074076) * 10 ^ 70 + 359079653815481249227096722606317825598717545587680742894271702393416) * 10 ^ 70 + 3288412638379560804517140607826908888391729682482307967786864872238108)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_192 :
Polynomial.coeff recurrence5LeadingSquare 192 = ((20035942949914707870622949514886 * 10 ^ 70 + 3877994478758845193140012307932656552891918201448906815983108469298927) * 10 ^ 70 + 959433132760148511742548018277602923921712522118024785316340466061122) * 10 ^ 70 + 9699542523152283146570332271478011651578344762781051170514929132963764
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_193 :
Polynomial.coeff recurrence5LeadingSquare 193 = -(((20752150461589044147011438194726 * 10 ^ 70 + 5063267210990641615171920691174185309507178270474945919646780346572539) * 10 ^ 70 + 6679906074862077320785090323671120773976389247902542538296410656252711) * 10 ^ 70 + 1955008446805265794987318195084715257960021494328831202050434142961136)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_194 :
Polynomial.coeff recurrence5LeadingSquare 194 = ((15178500374983483554262274701318 * 10 ^ 70 + 2377649184698535953781744587670487054796783430173857114232521117284435) * 10 ^ 70 + 6126231204830301007614497604769037573487123396435462579408520367534162) * 10 ^ 70 + 3747051611586087410613057885454835753705021518531850712263544696225443
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_195 :
Polynomial.coeff recurrence5LeadingSquare 195 = -(((9294831266591315350088940417749 * 10 ^ 70 + 9324338414913948022002938164038591678483804415713493261225588872559347) * 10 ^ 70 + 1785994110798206160407883414621684880117047693568509593943403052142198) * 10 ^ 70 + 4536015865724733425051570819895713480118980345908855197693111453412712)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_196 :
Polynomial.coeff recurrence5LeadingSquare 196 = ((5049483288546871965505697155193 * 10 ^ 70 + 1150225498553959005987996271086689148886835884811032491115940987659354) * 10 ^ 70 + 6775617667870017512103550669956429329720952166741176191276844103351342) * 10 ^ 70 + 1419276262716597254735310735191508025801043031581220963232439096454002
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_197 :
Polynomial.coeff recurrence5LeadingSquare 197 = -(((2501220017928891549454046015972 * 10 ^ 70 + 4913134468005643561371673837800955004991029862612884239608433772037017) * 10 ^ 70 + 9776018170652392568844714906868043902620643033012940781369597490254093) * 10 ^ 70 + 7020219206023952361296304267029318552411376595660629602894365608646498)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_198 :
Polynomial.coeff recurrence5LeadingSquare 198 = ((1147061609157469137530491668612 * 10 ^ 70 + 7226631887511495590496071116242538069923343896489885738338452218407341) * 10 ^ 70 + 8273506685043791761229861437283523399227026192062484582972197058604853) * 10 ^ 70 + 8010727591921792896496335814707563398390887809871420687642997914505660
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_199 :
Polynomial.coeff recurrence5LeadingSquare 199 = -(((491577514076117302202282675818 * 10 ^ 70 + 1730304685388622120675000460021599174088459451948823465142022111134330) * 10 ^ 70 + 2610614973501436611332082502829307813759858235765802646613593279360146) * 10 ^ 70 + 420956756164451914676801165427914068581350353609648097458755078136170)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_200 :
Polynomial.coeff recurrence5LeadingSquare 200 = ((198061891235925932342495473408 * 10 ^ 70 + 9498084747865778350428522699530840314496334967654736545677959389938271) * 10 ^ 70 + 4060533160980235953319451124462569648552625524265600338456728420002951) * 10 ^ 70 + 4369514320755732654172966548694207973111417342657529628469807955600372
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_201 :
Polynomial.coeff recurrence5LeadingSquare 201 = -(((75374806401241770691336945920 * 10 ^ 70 + 8136194246935749697845272971780203811634572789704324093509860238368579) * 10 ^ 70 + 5270950114756954897152770141244983112998371095563951482102167547796540) * 10 ^ 70 + 291229543040602358006500223778478877876031474532683249708895806370654)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_202 :
Polynomial.coeff recurrence5LeadingSquare 202 = ((27246209422624684572014583259 * 10 ^ 70 + 8704846309328100879089028718175822185892250636333908276775542477334071) * 10 ^ 70 + 9581223980950219137882133706792782665083922800020252469699766910955064) * 10 ^ 70 + 4396671401494548121682371385494100122914578361098441664510140702762708
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_203 :
Polynomial.coeff recurrence5LeadingSquare 203 = -(((9463565549019506074240843163 * 10 ^ 70 + 9487186530062638495392676241163114506114503301770975937143156023087785) * 10 ^ 70 + 7869170012351730535573810900159756680126190671677527918336734284063029) * 10 ^ 70 + 8559220364539495311079620500158108742145378527706177144738079951370516)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_204 :
Polynomial.coeff recurrence5LeadingSquare 204 = ((3246923460286435711243066142 * 10 ^ 70 + 1366542451719113800137672014268648134717964761316328906024822519609445) * 10 ^ 70 + 2805183105578747958801565378929487184439316876416024692242755532811224) * 10 ^ 70 + 6182849751980187546093161211854967819215143474890930079530937464666635
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_205 :
Polynomial.coeff recurrence5LeadingSquare 205 = -(((1165478500197750514662113449 * 10 ^ 70 + 7428279907055748164111838427938518641002043566895287684627043240902796) * 10 ^ 70 + 7512873118209372292773330230139062373167550185164154315658899977514040) * 10 ^ 70 + 9665809487191578643807817299874448498108157737705508462172607240992140)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_206 :
Polynomial.coeff recurrence5LeadingSquare 206 = ((474336807998118984160420137 * 10 ^ 70 + 8521885588073118226501008905989863782682420700415625693030633588566042) * 10 ^ 70 + 8430178405693829294343499355070145536576987925821349816252350738006633) * 10 ^ 70 + 2315164955022320746962956844926789269664563444354179981555945219519716
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_207 :
Polynomial.coeff recurrence5LeadingSquare 207 = -(((228175589138297078411983195 * 10 ^ 70 + 917942282916937152192971729686404430180843362819896698723672178922835) * 10 ^ 70 + 3375922620329857764213557868197207252363554960347791065233544497818279) * 10 ^ 70 + 7699361652400178740207099568983679985419419019250021169869370078313648)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_208 :
Polynomial.coeff recurrence5LeadingSquare 208 = ((123912923728941848226725876 * 10 ^ 70 + 1733436447879476131548531791562642172209930178966186798969947298558057) * 10 ^ 70 + 837176470971634435251854907177802789574540888678467174283290607068894) * 10 ^ 70 + 222333623178034138197213722372158702007042785378554077942770718731528
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_209 :
Polynomial.coeff recurrence5LeadingSquare 209 = -(((70100544410516239848470800 * 10 ^ 70 + 5130404648657893790504567323768439600378473335142927028722229087174900) * 10 ^ 70 + 2882913726861117023791105416149378694389788911306676299479547038688187) * 10 ^ 70 + 5599082763576696874021963140059410508655793684132236863762243814417840)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_210 :
Polynomial.coeff recurrence5LeadingSquare 210 = ((39105907149812825762747511 * 10 ^ 70 + 360368187665813272597707905406469221799486486533310163989885352764200) * 10 ^ 70 + 1373190167725137616049953796197824449382294340719723958740517920958900) * 10 ^ 70 + 8115489125989224414751412210322221279582727167407877376835005849835440
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_211 :
Polynomial.coeff recurrence5LeadingSquare 211 = -(((20994629118224934827213970 * 10 ^ 70 + 673641107191032933427485286392779506340768883163812629235757287301501) * 10 ^ 70 + 5165079766987216177241276543262321219320015924255313110350176577166833) * 10 ^ 70 + 892711549142460103875287857335634482629335063021032749722272196085060)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_212 :
Polynomial.coeff recurrence5LeadingSquare 212 = ((10767008320033385746546252 * 10 ^ 70 + 6501966401112609053166131724117738566689211411467315368448435296413820) * 10 ^ 70 + 4515558740072963403706929589484915288010430984672230766027917880558084) * 10 ^ 70 + 6297170034904554243399407129653858179371651149196417890738479381497483
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_213 :
Polynomial.coeff recurrence5LeadingSquare 213 = -(((5273555039819055791058267 * 10 ^ 70 + 732850789538346652663696197686623878791534075323476983052920829428264) * 10 ^ 70 + 137599547612874360076864334063659991286588278856612314537331053577577) * 10 ^ 70 + 8666505306986162141372673341775816118215310013927234320083335906162544)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_214 :
Polynomial.coeff recurrence5LeadingSquare 214 = ((2472659973898489151797243 * 10 ^ 70 + 1099637456122381620108709620491250925647797335641806979304861270190094) * 10 ^ 70 + 9188807008793619418666231061594128353507129831488293219737143810961488) * 10 ^ 70 + 4025630494587969935303831513815379728661395299735649010960651706527615
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_215 :
Polynomial.coeff recurrence5LeadingSquare 215 = -(((1113285844235815162880225 * 10 ^ 70 + 7701074253687219398787347020629062687382176276942535024055510091530704) * 10 ^ 70 + 6628284258263235937642365790573510646858989025807932307684281326709298) * 10 ^ 70 + 73727431314654348585258082613612890013175692434384037942064125531966)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_216 :
Polynomial.coeff recurrence5LeadingSquare 216 = ((482749234360082379960423 * 10 ^ 70 + 2819320076373015599661394038816459034988387319472092697501036609444159) * 10 ^ 70 + 2779016428878154623917981749351453710393099727035669463347530881810990) * 10 ^ 70 + 4345700088605309616109067712494757771498328951139028606562785637946689
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5LeadingSquare_coeff_217 :
Polynomial.coeff recurrence5LeadingSquare 217 = -(((202128893669259090276436 * 10 ^ 70 + 2504291822283139603997043669949998444186432705585959735714699552506212) * 10 ^ 70 + 8268987706097628426876675143272167467478087565081278385727016719752594) * 10 ^ 70 + 8086221394872808065754583152285053814818585607405037152708002809829220)