Recurrence 4 lookup certificate: A4Square 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.recurrence4A4Square_coeff_166 :
Polynomial.coeff recurrence4A4Square 166 = (22688879267686860141898986220007830093490354607755358166 * 10 ^ 70 + 8007998418475322710832213520759221920740299210311818169466935239223750) * 10 ^ 70 + 1313491809892261041867780212981536113961498956205142351874351611699178
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_167 :
Polynomial.coeff recurrence4A4Square 167 = -((31018768517923557242637002993976237884466726853249663720 * 10 ^ 70 + 4328917292568414406421383267424211210927719282015077047457670271589953) * 10 ^ 70 + 9260216690212470163277747902724496907182595324847399268502691927306956)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_168 :
Polynomial.coeff recurrence4A4Square 168 = (41666055753444141409891377690820591585973483223132225159 * 10 ^ 70 + 6944989113640153187840913829231821215606498519364661506437617799053473) * 10 ^ 70 + 1631342100398570289433050019958036355946351300053700420146132903687342
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_169 :
Polynomial.coeff recurrence4A4Square 169 = -((54991131778316616130147179840578408723516289455059798838 * 10 ^ 70 + 2491977193598665460955257730797438397094309827179725534407811098268231) * 10 ^ 70 + 498463632469328628581827149733834182184246208029522821510963348818188)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_170 :
Polynomial.coeff recurrence4A4Square 170 = (71311684777118168972469672652878866293112455432926783581 * 10 ^ 70 + 3728169750004797491962697999843191426401722461301002199327838536342588) * 10 ^ 70 + 5075936554530186250475725388072447403029498596945512310165686136793644
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_171 :
Polynomial.coeff recurrence4A4Square 171 = -((90863842818953149225682384252812941183362311683410575524 * 10 ^ 70 + 5519937488096363253393616566102916336324502798293086228965116770771874) * 10 ^ 70 + 7163635769465411253329701777724416685241969527201585696676575799192248)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_172 :
Polynomial.coeff recurrence4A4Square 172 = (113759509968405632148179210427780613181098891152445898304 * 10 ^ 70 + 1742591082847119553590493876344077309683654898273590273961045517387115) * 10 ^ 70 + 6599685110470604620329026907050117602674948990896425028658887482665504
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_173 :
Polynomial.coeff recurrence4A4Square 173 = -((139943791505062232844368949209907097226440399351760025241 * 10 ^ 70 + 8582434457709716965483730100935058319666641763310538221523719545120739) * 10 ^ 70 + 777769393695600014481161259628700754256420119308202404766914414112244)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_174 :
Polynomial.coeff recurrence4A4Square 174 = (169157489441048120816101239446191157229112347221408483250 * 10 ^ 70 + 3697054009297957519154247090781587214672333216279180164943846934603234) * 10 ^ 70 + 2379783306976159120183544468335496546535377564918906259905630094506416
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_175 :
Polynomial.coeff recurrence4A4Square 175 = -((200910261541479122978263994878898205238334755480186218655 * 10 ^ 70 + 4403070129495884692939436244497950837323830418924566759382574106163058) * 10 ^ 70 + 1655123389072886078544337432631306573414486021140487142589393579781622)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_176 :
Polynomial.coeff recurrence4A4Square 176 = (234469947483307010792583609477740439270726132438831567924 * 10 ^ 70 + 1556985751779363215943666917215135568056166742852197943002654388054321) * 10 ^ 70 + 4599159755768155904176536313223892610408120204120589731722409068697946
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_177 :
Polynomial.coeff recurrence4A4Square 177 = -((268872623031898976694755990744938881320110903044378211246 * 10 ^ 70 + 1717747836097915009010986821276099468217838749794759512884189798951117) * 10 ^ 70 + 7903666672148586433631684052279059655674918256686892653137686390061182)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_178 :
Polynomial.coeff recurrence4A4Square 178 = (302956121296265715235405604388833002748452345531534964354 * 10 ^ 70 + 1583772919738127824596869978222953110118839822761632626553120599482847) * 10 ^ 70 + 7221273240889637731586594579691954302318974272959759175039896413223536
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_179 :
Polynomial.coeff recurrence4A4Square 179 = -((335417191595079335783426495993733858282663438246096963618 * 10 ^ 70 + 9245548196579066785378767448025345071209330388570229482542484067757334) * 10 ^ 70 + 6754168586836844548816738386479855238052326034094236959998436117312310)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_180 :
Polynomial.coeff recurrence4A4Square 180 = (364889445935595588127778226556197747992916579990507181992 * 10 ^ 70 + 155157968281824950271380045525718896008395591243372434629126814509730) * 10 ^ 70 + 1416636805779186244324208538085233365481594132853852392342715507802426
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_181 :
Polynomial.coeff recurrence4A4Square 181 = -((390036196869353763699375104828793122379655538642745281878 * 10 ^ 70 + 5764190620635005577342473456644392551884481671008259419379767426645783) * 10 ^ 70 + 8567024984539692398859739712045208225513882404210645156627301892310326)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_182 :
Polynomial.coeff recurrence4A4Square 182 = (409649711880739028934204303560564737670602740524565687651 * 10 ^ 70 + 2674092066107389491448590997692071568666379736663681117796326079788308) * 10 ^ 70 + 6738777562007860511138105251988172829465636660969886328024306709295631
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_183 :
Polynomial.coeff recurrence4A4Square 183 = -((422746770411582793389201425312733717363928457383588656520 * 10 ^ 70 + 8563115521943428032215668811959204880553903183075208734628445978984787) * 10 ^ 70 + 4714667974035909919925700123351675836383922010928261298194778588933740)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_184 :
Polynomial.coeff recurrence4A4Square 184 = (428650065522276463701204830429357589939076007943086726674 * 10 ^ 70 + 9517082736975542038740678984156082776842721343499772745689681165490047) * 10 ^ 70 + 986479937542070486259211742675675426788510321949576921307272431047380
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_185 :
Polynomial.coeff recurrence4A4Square 185 = -((427046101246395825590689270159520357403031420306069981024 * 10 ^ 70 + 2404045644313236304050586421977875136476729292816473686402708965047837) * 10 ^ 70 + 2358405295703182647212180528360124181080306112147951454612015927943084)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_186 :
Polynomial.coeff recurrence4A4Square 186 = (418012713579035398656406837399545159213685379028800105881 * 10 ^ 70 + 573043378037156460763877649021941778563234905535031595313910373661106) * 10 ^ 70 + 9550831061193223386083379575976995792565383295702990848881812434668914
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_187 :
Polynomial.coeff recurrence4A4Square 187 = -((402012860082047760077834425387693313101317980388448299299 * 10 ^ 70 + 8248750239925089045538968805326449410704860059228917138934678224525407) * 10 ^ 70 + 7681640844510851563329380488555362774340677207358475557948493552970212)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_188 :
Polynomial.coeff recurrence4A4Square 188 = (379855361764639814868774632597611954391606058747143626934 * 10 ^ 70 + 9134229371815264139989493451200183841919261620314483570216767095025299) * 10 ^ 70 + 1943284564366756845737814851135769065370509685434712328331043251439314
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_189 :
Polynomial.coeff recurrence4A4Square 189 = -((352627224344112058833064197867527899329811709830901650004 * 10 ^ 70 + 429178705801982359290940643522738108516331135384702503139137347836167) * 10 ^ 70 + 3296156587544902908715820036167254021694322009813308814520932050515204)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_190 :
Polynomial.coeff recurrence4A4Square 190 = (321605413274647149330150240458141247854441728113719832717 * 10 ^ 70 + 8369363029256315482242558810801402024801627685447936758473774396741428) * 10 ^ 70 + 4625928630795363015699345199335017392457471549276417421347603121203316
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_191 :
Polynomial.coeff recurrence4A4Square 191 = -((288158034220106430055545520947246978491622560600922626775 * 10 ^ 70 + 3293637295374103543012839853674581312791010455165484029592460902541929) * 10 ^ 70 + 92504357120275270745142458396075988692583908505266638448455001819938)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_192 :
Polynomial.coeff recurrence4A4Square 192 = (253645515155670428821528993759992467496785290024952004519 * 10 ^ 70 + 838507393764447853442853728171040953831993587991183076824569677780794) * 10 ^ 70 + 6168771320087229645517206485004641437333247027760157635088927403332371
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_193 :
Polynomial.coeff recurrence4A4Square 193 = -((219331585529996803506930266222367925793192036311821557426 * 10 ^ 70 + 9362255143411226401453693267658757778821652230648636140651353026990416) * 10 ^ 70 + 7242163051305740772679773979373445859556903934349752063136196590984210)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_194 :
Polynomial.coeff recurrence4A4Square 194 = (186311827670682026624166658136892876353430733663949858630 * 10 ^ 70 + 4494055147848451640516762877928860288819313715970733845301390386972743) * 10 ^ 70 + 759978687420081503163177224832344008107082038074965450923467902626372
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_195 :
Polynomial.coeff recurrence4A4Square 195 = -((155464741962837488812586687621201157480021822867450682578 * 10 ^ 70 + 2488101330879698442746027115673006546637988778676654712462175465165993) * 10 ^ 70 + 4544325407678509775665733024487058393867305959041687234755984963198008)