Exact Pell data slice 27eb91109ec4a4ce18d7

Definition
D1Bound5_Prove2MeTransfer_pellSlice_27eb91109ec4a4ce18d7
by tp · Oct 24, 2026 · Mathlib 0df444a (Lean v4.33.1)
diophantine-tuplesnumber-theory
Exact consecutive entries 1–127 of pellMagnitudes_7. The original list is the ordered concatenation of these slices.
Definition code
import Init

namespace D1Bound5.Prove2MeTransfer
set_option maxRecDepth 100000
set_option maxHeartbeats 0

def pellSlice_27eb91109ec4a4ce18d7 : List Int :=
[
  8,
  2024,
  514088,
  130576328,
  33165873224,
  8424001222568,
  2139663144659048,
  543466014742175624,
  138038228081367949448,
  35061166466652716984168,
  8905398244301708746029224,
  2261936092886167368774438728,
  574522862194842209959961407688,
  145926545061397035162461423114024,
  37064767922732652089055241509554408,
  9414305125829032233584868882003705608,
  2391196437192651454678467640787431670024,
  607354480741807640456097195891125640480488,
  154265646911981948024394009288705125250373928,
  39182866961162672990555622262135210687954497224,
  9952293942488406957653103660573054809615191920968,
  2527843478525094204570897774163293786431570793428648,
  642062291251431439554050381533816048698809366338955624,
  163081294134385060552524226011815113075711147479301299848,
  41422006647842553948901599356619504905181932650376191205768,
  10521026607257874317960453712355342430803135182048073264965224,
  2672299336236852234208006341338900357919091154307560233109961128,
  678753510377553209614515650246368335569018350058938251136665161288,
  172400719336562278389852767156236218334172741823816008228479841006024,
  43789103957976441157812988342033753088544307404899207151782742950368808,
  11122260004606679491806109186109417048271919908102574800544588229552671208,
  2825010252066138614477593920283449896507979112350649100131173627563428118024,
  717541481764794601397817049642810164295978422617156768858517556812881189306888,
  182252711358005762616431053015353498281282011365645468640963328256844258655831528,
  46291471143451698909972089648850145753281334908451331878035826859681628817391901224,
  11757851417725373517370294339754921667835177784735272651552459059030876875358887079368,
  2986447968631101421713144790208101253484381875987850802162446565166983044712339926258248,
  758546026180882035741621406418517963463365161323129368476609875093354662480058982382515624,
  192667704201975405976950124085513354618441266594198871742256745827146917286890269185232710248,
  48936838321275572236109589896313973555120618349765190293164736830220223636207648314066725887368,
  12429764265899793372565858883539663769646018619573764135592100898130109656679455781503763142681224,
  3157111186700226241059492046829178283516533608753386325250100463388217632572945560853641771515143528,
  801893811657591565435738414035727744349429890604740552849389925599709148563871493001043506201703774888,
  203677871049841557394436497673028017886471675679995347037419791001862735517590786276704196933461243678024,
  51733377352848097986621434670535080815419456192828213406951777524547535112319495842789864977592954190443208,
  13140074169752367047044449969818237499098655401302686210018714071444072055793634353282349000111676903128896808,
  3337527105739748381851303670899161789690243052474689469131346422369269754636470806237873856163388340440549346024,
  847718744783726336623184087958417276343822636673169822473151972567723073605607791150066677116500526794996404993288,
  215317223647960749753906907037767089029541259471932660218711469685779291426069742481310698113734970417588646318949128,
  54689727087837246711155731203504882196227136083234222525730240148215372299148108982461767254211565985540721168608085224,
  13890975363087012703883801818783202310752663023882020588875262286177018784692193611802807571871624025356925588180134697768,
  3528253052497013389539774506239729882048980180929949995351790890448814555939518029288930661488138290874673558676585605147848,
  896162384358878313930398840783072606838130213293183416798766010911712720189852887245776585210415254258141726978264563572855624,
  227621717374102594724931765784394202407003025196287657916891214980684582113666693842397963712783986443277123978920522561900180648,
  57815020050637700181818738110395344338771930269643771927473569839082972144151150383081837006461922141338131348918834466159073028968,
  14684787471144601743587234548274633067845663285464321781920369847912094240032278530608944201677615439913442085501405033881842649177224,
  3729878202650678205170975756523646403888459702577668088835846467799832853996054595624288745389107859815872951586007959771521873817985928,
  947374378685801119511684254922457911954600918791442230242523082451309632820757835010038732384631718777791816260760520376932674107119248488,
  240629362307990833677762629774547785990064744913323748813512027096164846903618494037954213736951067461699305457281586167781127701334471130024,
  61118910651850985953032196278480215183564490607065440756401812359343419803886276727805360250453186503552845794333262126096029503464848547777608,
  15523962676207842441236500092104200108839390549449708628377246827246132465340210670368523549401372420834961132455191298442223712752370196664382408,
  3943025400846140129088117991198188347430021635069618926167064292308158302776609623996877176187698141705576574797824256542198727009598565104205354024,
  1001512927852243384945940733264247736047116655917133757537805952999444962772793504284536434228125926620795615037514905970420034436725283166271495539688,
  254380340649068973636139858131127726767620200581316904795676544997566712385986773478648257416767797663540380642953988292230146548201212325667855661726728,
  64611605011935667060194578024573178351239483830998576684344304623428945501077867670072372847424792480612635887695275511320486803208671205436469066583049224,
  16411093292691010364315786678383456173488061272873057160918657697805954590561392401424904054988480522277945975093957025887111417868454284968537475056432776168,
  4168353084738504696869149621731373294887616323825925520296654710938089037057092592094255557594226627866117665037977389299814979651784179710803082195267342097448,
  1058745272430287501994399688133090433445281058190512209098189377920576809457910956999539486724878574997471608973671162925127117720135313192259014340122848459975624,
  268917130844208287001880651636183238721806501164066275185419805337115571513272325985290935372561563822729922561647437405592988085934717766654078839309008241491711048,
  68303892489156474610975691115902409544905406014614643384887532366249434587561712889306898045143912332398402859049475429857693846709698177416943766170147970490434630568,
  17348919775114900342900823662787575841167251321210955353486247801222019269669161801557966812531181170865371596276005111746448644076177402346137062528378275496328904453224,
  4406557318986695530622198234656928361246936930181568045142122053978026645061379535882834263484874873487471987051246248908168097901502350497741396938441911828097051296488328,
  1119248210102845549877695450779197016180880813014797072510745515462617545826320732952438344958345686684647019339420271217562950418337520849023968685301717226061154700403582088,
  284284638808803782973404022299681385181582479568828274849684218805450878613240404790383456785156319543026855440225697643012081238159828793301590304669697733507705196851213362024,
  72207179009226058029694743968668292639105768929669367014747280831069060550217236496024445585084746818242136634797987781053851071542178175977754913417417922593731058845507790372008,
  18340339183704609935759491564019446648947683725656450393470959646872735928876564829585418795154740535513959678383248670690035160090475096869556446417719482641074181241562127541128008,
  4658373945481961697624881162516970780540072560547808730574609003024843856874097249478200349523719011273727516172710364367487876811909132426691359635187331172910248304297934887656142024,
  1183208641813234566586784055787746558810529482695417761115557215808663466910091824802633303360229474122991275148190049300671230675064829161282735790891164398436561995110433899337118946088,
  300530336646616097951345525288925108967093948532075563514620958206397495751306449402619380853148762708228510160124099812006125103589654697833388199526720569871713836509745912496740556164328,
  76333522299598675645075176639331189931083052397664497714952607827209155257364928056440520103396425498415918589396373162200255105081097228420519319943996133583016877911480351340272764146793224,
  19388414133761416997751143520864833317386128215058250344034447767152919037874940419886489486881838927834935093196518659099052790565495106364114073877575491209516415275679499494516785352729314568,
  4924580856453100318753145379123028331426145483572397922887034780249014226464977501723111889147883691244575097753326343037997208548530675919256554245584230771083586463144681391255923206829099107048,
  1250824149124953719546301175153728331348923566699174014162962799735482460603066410497250533354075575737194239894251694612992191918536226188384800664304517040364021445223473393879509977749238443875624,
  317704409296881791664441745343667873134295159796106627199469664098032295978952403288799912360046048353556092358042177105356978750099652921173820112179101744021690363500299097364004278425099735645301448,
  80695669137258850129048657016116486047779621664644384134651131718100467696193307368944680488918342206227510264702818733066059610333393305751961923692827538464468988307630747257063207209997583615462692168,
  20496382256454451050986694440348243788262889607659877463574187986733420762537121119308660044272898874333434051142157916021673784045931800008077154797866015668231101339774709504196690627060961138591878509224,
  5206000397470293308100491339191437805732726180723944231363709097498570773216732570997030706564827395738486021479843407850772075088056343808745845356734275152192235271314468583318702356066274131618721678650728,
  1322303604575198045806473813460184854412324187014274174888918536576650242976287535912126490807421885618701116021829083436180085398582265395621436643455708022641159527812535245453446201750206568470016714498775688,
  335859909561702833341536248127547761582924610775444916477553944581371663145203817389109131634378594119754344983523107349381890919164807354144036161592393103475702327829112637876592016542196402117252626761010374024,
  85307094725067944470704400550583671257208438812775994511123813005131825788638793329297807308641355484531984924698847437659564113382462485687189563607824392574805750109066797485408918755516135931213697180582136226408,
  21667666200257696192725576203600124951569360533834327160908970949358902378651108301824253947263269914477004416528523726058179902908226306557192005120225803320897184825375137448655988771884556330126161831241101591133608,
  5503501907770729765007825651313881154027360367155106322876367497324156072351592869870031204797561916921674589813320327571340035774576099403041082110973746219115310139895175845161135739139921791716113891438059222011710024,
  1397867816907565102615794989857522212997997963896863171683436435349386283474925937838686101764633463628190868808166834679394310906839421022065877664182211313851967878348549289533479821752768250539562802263435801289383212488,
  355052921992613765334646919598159328220337455469436090501269978211246791846558836618156399817012102199643559002684562688238583630301438363505329885620170699972180725790391624365658713589463995715257235661021255468281324261928,
  90182044318306988829897701782942611845752715691272870124150891029221335742742469575073886867419309325245835795813070755977920847785658504909331725069859175581620052382881124039587779771902102143424798295097135453142166979317224,
  22905884203927982549028681605947825249492969448127839575443825051444008031864740713232149107924687556510242648577517287455703656753926958808606752837858610427031521124526015114430930403349544480434183509719011383842642131422312968,
  5818004405753389260464455230208964670759368487108779979292607412175748818757901398691390799526003220044276386902893577942992750894649661878881205889091017189290424745577224957941416734671012395928139186670333794360577959214288176648,
  1477750213177156944175422599791471078547630102756181986900746838867588755956475090526900030930496893203689692030686391280232703023584260190277017689076280507469340853855490613302005419676033799021266919230755064756202958998297774555624,
  375342736142592110431296875891803444986427286731583115892810404464955368264125915092433916465546684870517137499407440491601163575239507438668483611819486157880023286454549038553751435180977913939005869345425116114281191007608420448951848,
  95335577230005218892605231053918283555473983199719355254786941987259795950332025958387687882217927460218149235157459198475415315407811305161604560384460407821018445418601600302039562530548714106708469546818748737962666312973540496259213768,
  24214861273685183006611297390819352219645405305441984651599990454359523216016070467515380288166888028210539388592495228972263888950008832003608889854041124100380805113038351927679495131324192405190012259022616754326402962304271677629391345224,
  6150479427938806478460376932037061545506377473599064382151142788465331637072131566722948205506507341238016786553258630699756552377986835517611496418366061061088903480266322788030289723793814322204156405322197836850168389758972032577369142473128,
  1562197559835183160345929129440022813206400232888856911081738668279739876293105401877161328818364697786428053245139099702509192040119706212641316481375125468392481103182532949807765910348497513647450536939579227943188444595816592002974132796829288,
  396792029718708583921387538500833757492880152776296056350379470600265463246811699945232254571659126730411487507478778065806635021638027391175376774772863502910629111304883102928384510938794574652130232226247801699733014758947655396722852361252166024,
  100783613350992145132872088850082334380378352404946309456085303793799147924813878680687115499872599824826731398846364489615182786304018837652333059475825954613831401790337125610859858012543473464127431534930002052504242560328108654175601525625253340808,
  25598640999122286155165589180382412098858608630703586305789316784154383307439478373194582104713068696379259363819469101584190621086199146736301421730085019608410265425634325022055475550675103465313715479639994273534377877308580650505206064656453096399208,
  6501954030163709691266926779728282590775706213846305975361030377871419560941702692912743167481619576280507051678746305437894802573108279252182908786382119154581593586709328218476479930013463736716219604397023615475679476593819157119668164821213461232058024,
  1651470725020583139295644236461803395644930519708331014155395926662556414095885044521463569958226659306552411867037742112123695662948416730907722530319328180244116360758743733168003846747869114022454465801364358336549052676952757327745208658523562699846338888,
  419467062201197953671402369134518334211221576299702231289495204341911457760793859605758834026222089844288032107175907750173980803586324741371309339792322975662850974039134198896454500594028741497966718093942149993867983700469406542090163331100163712299738019528,
  106542982328379259649396906115931195086254635449604658416517626506918847714827544454818222379090452593789853602810813530802079000415263535891581664584719716490183903289579327775966275147036552471369523941395504734084131310866552308933573740890783059361433610621224,
  27061498044346130752993142751077389033574466182623283535564187637553045408108435497664222725454948736732778527081839460915977892124673351791720371495179015665531048584579110120896537432846690298986361114396364260307375484976403817062585640022927796914091837359771368,
  6873513960281588832000608861867540883332828155750864413374887142311966614811827788862257754043177888677531956025184412259127582520666616091561082778110885259328396156579804391379944541667912299390064353532735126613339289052695702981587818992082769633119965255771306248,
  1745845484413479217197401657771604306977504777094536937713685769959601967116796149935515805304241728775356384051869758874357489982357195813904723305268669676853747092722685736300385017046216877354777359436200325795527872043899732153506243438349000559015557083128552015624,
  443437879527063439579308020465125626431402880553856631314862810682596587681051410255832152289523355931051844017218893569674543327936207070115708158455463987035592433155405597215906414385197418935814059232441350016937466159861479271287604245521654059220318379149396440662248,
  112631475554389700173927039796484137509269354155902489817037440227609573669019941408831431165733628164758393023989547096938459647805814238613575967524382584037363624274380299007103928868823098192819416267680666703976320876732771835174897972119061782041401852746863567376195368,
  28607951352935456780737888800286505801727984552718678556896194955002149115343384066432927683944052030492700776249327743728799075999348880400778180043034720881503324973259440542207182026266681743557195917931656901459968565223964184655152797313996170984456850279324196717112961224,
  7266307012170051632607249828232975989501398807036388450961816481130318265723550532932554800290623482116981238774305257360018026844186809807559044154963294721317807179583623517421617130742868339765334943738373172304128039246010170130573635619782908368269998569095599102579315955528,
  1845613373139840179225460718482375614827553569002689947865744490012145837344666491980802486346134420405682741947897286041700850019347450342239596437180633824493841520289267113984548544026662291618651518513628854108347061999921359248981048294627544729369595179700002847858429139742888,
  468778530470507235471634415244695173190209105127876210369448138646603912367279565412590898977117852159561299473527136349334655886887408200119049935999726028126714428346294263328557908565641479202797720367517990570347849619940779239071055693199776578351508905645231627756938422178738024,
  119067901126135697969615916011434091614698285148911554743891961471747381595451664948306107537701588314108164383533944735444960894419382335379896444147493230510360970958438453618339724227128909055219002321831055976014245456402958005364799165024448623356553892438709133447414500804259715208,
  30242778107507996777046971032489014574960174218718407028738188765685188321332355617304338723677226313931314192118148435666670732526636225778293577763527280823603559909015020924794961395782177258546423792024720699917047998076731392583419916860516750555986337170526474664015526265859788924808,
  7681546571405905045671961026336198267948269553269326473744756054522566086236822875130353729706477782150239696633626168714598921100871181965351188855491781835964793855918856876444301854804445894761736424171957226722954177266033370758183294083406230192597173087421285855526496257027582127186024,
  1951082586358992373603901053718361871044285506356190205924139299659966100715831677927492543006721679439846951630748928705072459288888753582973423675717149059054234035843480631595927876158933475092222505315885110866930443977574399441185973277268321952169125977867836080829066033758740000516325288,
  495567295388612656990345195683437579046980570344919042978257637357576867015735009370707975569977600099938975474513594264919690060456642538893284262443300369217939480310388161568489236242514298227529754613810646202973609816126631424690479029132070369620765401205342943244727246078462932549019437128,
  125872141946121255883174075802539426716062020582103080726271515749524864255895976548481898302231303703705059923574822194360896202896698316125311229236922576632297573764802749557764670077722472816317465449402588250444429962852186807471940487426268605561722242780179239748079891437895826127450420705224,
  31971028487019410381669224908649330948300706247283837585429986742741957944130562308305031460791181163140985281612530323773402715845700915653290158941915891164234365796779587999510657710505265581046408694393643604966682236954639322466448193327243093742307828900764321553069047697979461373439857839689768,
  8120515363560984115688099952721127521441663324789512643618490361140707792944906930332929509142657784134106556469659127416249928928605135877619575060017399433138896614808250549126149293798259735112971490910536073073286843756515535719670369164632319541940626818551357495239790035395345293027596440860495848
]

end D1Bound5.Prove2MeTransfer
Source
D1Bound5/PellLightMatchingField7.lean, lines 7-8, SHA-256 cb2b47876127a30e241273d61a4c1a7056c0b462398797ee7f4519b7c4f90d82; D1Bound5/PellLightMatchingField7.lean, lines 10-11, SHA-256 cb2b47876127a30e241273d61a4c1a7056c0b462398797ee7f4519b7c4f90d82; D1Bound5/PellLightMatchingField7.lean, lines 13-14, SHA-256 cb2b47876127a30e241273d61a4c1a7056c0b462398797ee7f4519b7c4f90d82; D1Bound5/PellLightMatchingField7.lean, lines 16-18, SHA-256 cb2b47876127a30e241273d61a4c1a7056c0b462398797ee7f4519b7c4f90d82; D1Bound5/PellLightMatchingField7.lean, lines 20-22, SHA-256 cb2b47876127a30e241273d61a4c1a7056c0b462398797ee7f4519b7c4f90d82; D1Bound5/PellLightMatchingField7.lean, lines 24-26, SHA-256 cb2b47876127a30e241273d61a4c1a7056c0b462398797ee7f4519b7c4f90d82. Project: https://github.com/tomislav-math/d1-bound5-lean. Exact entries 1-127 of pellMagnitudes_7; original literal SHA-256 1f296cbe817151c8fc44627f25fe4b74054e5cdc5147444c640fc2082da464dc.
View graph