Problems / erdos-257 / spec-a70fcca4--h4--h1--h2
after a skipped m >= 1, another skip within (m, 3m+2]
spec-a70fcca4--h4--h1--h2 spec_a70fcca4__h4__h1__h2
open
Hole hrun of spec-a70fcca4--h4--h1 (split by 20261022T143430Z-t1022-j-partial.lean).
$\displaystyle m \ge 1 \ \wedge\ r_m < \frac{1}{2^m-1} \ \Longrightarrow\ \exists n,\ m < n \le 3m+2 \ \wedge\ r_n < \frac{1}{2^n-1}$
Here r is the greedy remainder of 1/2: r_0 = 1/2, r_(m+1) = r_m - 1/(2^m-1) if that term fits under r_m, else r_m. In words: the set the walk chooses never contains the whole block m+1, ..., 3m+2 right after an element m >= 1 it skipped. This is weaker than the hole of graph PR #865 (window (m, 2m], m >= 2) and essentially equivalent to this node: conversely, the node's bound at a skipped m forces a skip within (m, 3m+3], since the terms over (m, 3m+3] sum to more than 2^-m + 4^-m/3 (both inequalities checked exactly for m <= 120, margins 3/28 and 1/56 times 8^-m).
Lean
theorem spec_a70fcca4__h4__h1__h2 : ∀ (r : ℕ → ℝ),
r (0 : ℕ) = (1 / 2 : ℝ) →
(∀ (m : ℕ),
r (m + (1 : ℕ)) =
if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) →
∀ (m : ℕ),
(1 : ℕ) ≤ m →
r m < (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) →
∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) := by
sorryWhy does it end in sorry?
A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
Explainer
On the partial assembly targets/erdos-257/nodes/spec-a70fcca4--h4--h1--h2/attempts/20261026T203640Z-t1026-a-partial.lean:
Informal account, unverified — unverified prose about a kernel-checked proof; shown section by section, each labelled with who drafted, wrote or verified it (D-3 v3.31).
Unverified: explainer, its words from explainer/dad86c0d0562….md, written by t1026-a, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-26.
Draft · drafted, by the model named above
Overview
Write $e_m = \frac{1}{2^m-1}$ (in Lean $e_0 = \frac10 = 0$) and let $r$ be any sequence with $r_0 = \frac12$ and $r_{m+1} = r_m - e_m$ if $e_m \le r_m$ (step $m$ is taken), else $r_{m+1} = r_m$ (step $m$ is skipped): the greedy remainder of $\frac12$. The statement: for every skipped $m \ge 1$ there is a skipped $n$ with $m < n \le 3m+2$. The partial decides this for every $m \le 100$ by computing the walk exactly, and leaves the same statement for $m > 100$ as its one hole.
The hole. For every $r$ obeying the recursion from $\frac12$ and every $m > 100$ with $r_m < e_m$, there is $n$ with $m < n \le 3m+2$ and $r_n < e_n$. It is left open (node spec-a70fcca4--h4--h1--h2--h1). It is the node's own statement with $1 \le m$ replaced by $100 < m$.
The values of the walk (walk_values). The recursion determines $r_n$ for every $n$, and the lemma states $r_1, \dots, r_{101}$ as explicit rationals, proved one step at a time: $r_{n+1}$ is rewritten by the recursion and the value of $r_n$, and norm_num decides whether $e_n \le r_n$ and performs the subtraction. The first values are $r_1 = r_2 = \frac12$, $r_3 = \frac16$, $r_4 = r_5 = r_6 = \frac1{42}$, $r_7 = \frac1{126}$, $r_8 = \dots = r_{13} = \frac1{16002}$; the denominators reach $1763$ bits at $n = 101$. The steps taken below $101$ are $2, 3, 6, 7, 14, 20, 21, 26, 27, 32, 33, 34, 35, 38, 39, 42, 44, \dots$; the steps skipped are $1, 4, 5, 8, \dots, 13, 15, \dots, 19, 22, \dots, 25, 28, \dots, 31, 36, 37, 40, 41, 43, 52, 54, 61, 62, 64, 67, 68, 69, 71, 72, 73, 76, \dots, 81, 83, 84, 85, 88, 90, 92, 94, 95, 97, 101$.
The finite range (range_1_25, range_26_50, range_51_75, range_76_100). Each lemma takes a block of twenty-five values of $m$ and runs through them (interval_cases). At a taken $m$ the hypothesis $r_m < e_m$ contradicts the computed value of $r_m$ (norm_num). At a skipped $m$ the next skipped step $n$ is named explicitly, $m < n \le 3m+2$ is arithmetic, and $r_n < e_n$ is again the computed value against $e_n$. The widest gap in the range is from $43$ to $52$, so every skipped $m \le 100$ is in fact followed by a skip within $(m, m+9]$, well inside $(m, 3m+2]$.
The assembly. Given $m \ge 1$ with $r_m < e_m$: if $m \le 100$, the block lemma for its range closes the goal; otherwise the hole does.
History: 1 version on record
2026-10-26 · written by t1026-a, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · explainer/dad86c0d0562….md · the first version of its chain
Read this version
Overview
Write $e_m = \frac{1}{2^m-1}$ (in Lean $e_0 = \frac10 = 0$) and let $r$ be any sequence with $r_0 = \frac12$ and $r_{m+1} = r_m - e_m$ if $e_m \le r_m$ (step $m$ is taken), else $r_{m+1} = r_m$ (step $m$ is skipped): the greedy remainder of $\frac12$. The statement: for every skipped $m \ge 1$ there is a skipped $n$ with $m < n \le 3m+2$. The partial decides this for every $m \le 100$ by computing the walk exactly, and leaves the same statement for $m > 100$ as its one hole.
The hole. For every $r$ obeying the recursion from $\frac12$ and every $m > 100$ with $r_m < e_m$, there is $n$ with $m < n \le 3m+2$ and $r_n < e_n$. It is left open (node spec-a70fcca4--h4--h1--h2--h1). It is the node's own statement with $1 \le m$ replaced by $100 < m$.
The values of the walk (
walk_values). The recursion determines $r_n$ for every $n$, and the lemma states $r_1, \dots, r_{101}$ as explicit rationals, proved one step at a time: $r_{n+1}$ is rewritten by the recursion and the value of $r_n$, andnorm_numdecides whether $e_n \le r_n$ and performs the subtraction. The first values are $r_1 = r_2 = \frac12$, $r_3 = \frac16$, $r_4 = r_5 = r_6 = \frac1{42}$, $r_7 = \frac1{126}$, $r_8 = \dots = r_{13} = \frac1{16002}$; the denominators reach $1763$ bits at $n = 101$. The steps taken below $101$ are $2, 3, 6, 7, 14, 20, 21, 26, 27, 32, 33, 34, 35, 38, 39, 42, 44, \dots$; the steps skipped are $1, 4, 5, 8, \dots, 13, 15, \dots, 19, 22, \dots, 25, 28, \dots, 31, 36, 37, 40, 41, 43, 52, 54, 61, 62, 64, 67, 68, 69, 71, 72, 73, 76, \dots, 81, 83, 84, 85, 88, 90, 92, 94, 95, 97, 101$.The finite range (
range_1_25,range_26_50,range_51_75,range_76_100). Each lemma takes a block of twenty-five values of $m$ and runs through them (interval_cases). At a taken $m$ the hypothesis $r_m < e_m$ contradicts the computed value of $r_m$ (norm_num). At a skipped $m$ the next skipped step $n$ is named explicitly, $m < n \le 3m+2$ is arithmetic, and $r_n < e_n$ is again the computed value against $e_n$. The widest gap in the range is from $43$ to $52$, so every skipped $m \le 100$ is in fact followed by a skip within $(m, m+9]$, well inside $(m, 3m+2]$.The assembly. Given $m \ge 1$ with $r_m < e_m$: if $m \le 100$, the block lemma for its range closes the goal; otherwise the hole does.
Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).
How it is being proved
Open. A direct proof, or proofs of its holes, close it.
Proved from this hole by 20261026T203640Z-t1026-a-partial.lean (merged in 0c1da39dcfcf, attestation 000987).
htail→ spec-a70fcca4--h4--h1--h2--h1 (open)$\displaystyle m > 100 \wedge r_m < \frac{1}{2^m-1} \Rightarrow \exists n,\ m < n \le 3m+2 \wedge r_n < \frac{1}{2^n-1}$
Read the partial proof (Lean)
private theorem walk_values (r : ℕ → ℝ) (h0 : r 0 = 1 / 2)
(hrs : ∀ m : ℕ, r (m + 1) = if (1 : ℝ) / ((2 : ℝ) ^ m - 1) ≤ r m then r m - 1 / ((2 : ℝ) ^ m - 1) else r m) :
r 1 = 1 / 2 ∧
r 2 = 1 / 2 ∧
r 3 = 1 / 6 ∧
r 4 = 1 / 42 ∧
r 5 = 1 / 42 ∧
r 6 = 1 / 42 ∧
r 7 = 1 / 126 ∧
r 8 = 1 / 16002 ∧
r 9 = 1 / 16002 ∧
r 10 = 1 / 16002 ∧
r 11 = 1 / 16002 ∧
r 12 = 1 / 16002 ∧
r 13 = 1 / 16002 ∧
r 14 = 1 / 16002 ∧
r 15 = 1 / 688086 ∧
r 16 = 1 / 688086 ∧
r 17 = 1 / 688086 ∧
r 18 = 1 / 688086 ∧
r 19 = 1 / 688086 ∧
r 20 = 1 / 688086 ∧
r 21 = 120163 / 240503259150 ∧
r 22 = 12932167 / 567347188334850 ∧
r 23 = 12932167 / 567347188334850 ∧
r 24 = 12932167 / 567347188334850 ∧
r 25 = 12932167 / 567347188334850 ∧
r 26 = 12932167 / 567347188334850 ∧
r 27 = 100171945053757 / 12691341578466215591850 ∧
r 28 = 107644170831134536927 / 243343288463189657575723817850 ∧
r 29 = 107644170831134536927 / 243343288463189657575723817850 ∧
r 30 = 107644170831134536927 / 243343288463189657575723817850 ∧
r 31 = 107644170831134536927 / 243343288463189657575723817850 ∧
r 32 = 107644170831134536927 / 243343288463189657575723817850 ∧
r 33 = 14598993650261743084714065641 / 69676764360476692711332185574552481050 ∧
r 34 = 7961090884242287202286887174188286683 / 85502692624144962281478559794068509473752428650 ∧
r 35 = 17089269107037109310175073431588929983696187113 / 489641691359023146408090293693780137366287632111847097650 ∧
r 36 = 24775495057665137934850160116999839971296655500713733 / 4273294490391516376753649556370453526829302383904245353406731150 ∧
r 37 = 24775495057665137934850160116999839971296655500713733 / 4273294490391516376753649556370453526829302383904245353406731150 ∧
r 38 = 24775495057665137934850160116999839971296655500713733 / 4273294490391516376753649556370453526829302383904245353406731150 ∧
r 39 = 845647244845372609119117317639626159048890492622691072083139023 / 391544748423291282081983403730543585794163711509479738425458531026506458150 ∧
r 40 = 1279361336100174444251942992473714966534258700082741704514992885791523 / 3754190171139528729585651254462415212675896584673329663463798639720328923217380650 ∧
r 41 = 1279361336100174444251942992473714966534258700082741704514992885791523 / 3754190171139528729585651254462415212675896584673329663463798639720328923217380650 ∧
r 42 = 1279361336100174444251942992473714966534258700082741704514992885791523 / 3754190171139528729585651254462415212675896584673329663463798639720328923217380650 ∧
r 43 = 2307178909358625844288230048113688514917493874182843861668184598259080687 / 20343956537405106185624644147931828037490683592344773446310324828644462434914985742350 ∧
r 44 = 2307178909358625844288230048113688514917493874182843861668184598259080687 / 20343956537405106185624644147931828037490683592344773446310324828644462434914985742350 ∧
r 45 = 659318159054952992368158389296038659826449069734600364727101743112098359598562611 / 11655908428123218204725844561756938739161153600678265505596657245523679800986195160837595468050 ∧
r 46 = 728602171895038678636394825276913166726248096645486542004397068685941640433698111948589851 / 25888884487622534734603867774700751495820189468709549988355020113039400587330235326362886993608342757550 ∧
r 47 = 8460645117916361525949041843570964695646901621569788945241573199933079840413055250334293685177039980221 / 607256096518192733364976633800564606357882531919006885021700723676812860062069999895812681580588233238576338844868550 ∧
r 48 = 583473847243115429710805323201397105794687109693978440309296238195743045193725738895896654861024781126198971055118717 / 85463697812430478601160467988164408038970436424688174871843944772162618813142138992772085377175290216341013777227236169933007265850 ∧
r 49 = 57235566419689740527216894644994090719061380449165398277406761889413767481516239955879524226149880396024414727845120310098331 / 17479494673046627672470862948133885139494627045732135374353110002317959629414713279514555065754621917880396537985539383414639696059681412050 ∧
r 50 = 116072950999685541383889664443572968628785973521095383728800241565844348269673906801493179079294274435122845507376543935730052352256689133 / 77480950488343722797022987731006171783678220639000435235009231243407940099381827934169581918016008090643185870271101231402724248618403158229303693245650 ∧
r 51 = 52009358972776708178754179196384591028396521395320498229273554009840029694048630162582390457279735168652989630775356150931336575678539518770484821183 / 85274481854256190162461282209750638404229496029888703103179320728362117630070146079717615316644475894677228969932350223380505975143341603386178767416794463169725650 ∧
r 52 = 34703310191239350769791367194664875178207907367958832542389658785757420961031869707529629835487322095292587580834041950889210513131813649056401396910662146983 / 209287945738809026219275100016580785098653830240066914142002489661478086867667048653939453375339890321169299805069374587184442865964663479716191899209781729053151957374213150 ∧
r 53 = 34703310191239350769791367194664875178207907367958832542389658785757420961031869707529629835487322095292587580834041950889210513131813649056401396910662146983 / 209287945738809026219275100016580785098653830240066914142002489661478086867667048653939453375339890321169299805069374587184442865964663479716191899209781729053151957374213150 ∧
r 54 = 103291683952767491891750666081103226355445470584688441325011751615328556690820348361282592828209747923435398251461622534779356283796512611067700294596444193396392448262867003 / 1885098228884873624011666960437368710807715308673609950293344297722004703388546146422304622652660491593324418280896776831792432687454926388554749762781569931017735810002476605563665676231650 ∧
r 55 = 103291683952767491891750666081103226355445470584688441325011751615328556690820348361282592828209747923435398251461622534779356283796512611067700294596444193396392448262867003 / 1885098228884873624011666960437368710807715308673609950293344297722004703388546146422304622652660491593324418280896776831792432687454926388554749762781569931017735810002476605563665676231650 ∧
r 56 = 28938917471616433418063823334248580477925844332221809806946710850025199523666410189545280477180319867467850932655442170871209577637393520505272503891542587694137356662057229169799115843 / 1070296759211774725790722296265701945389278514404776283394742030382279204391468452707922952872717892265133839389903409221994041786988893799546129514616776566503136411715372889274746954488854107634141150 ∧
r 57 = 728855957470306119334593881931744942956142754004476924984700530768600816655305995140906089684413857284101903609145096158189222185393049431628902589347323399187883947612398562037347430239561427101 / 55382379421561065182045979674407837221285399325700332325063054260807863800561242927602172086732743266112478175431395232227810531545303976647967939928233628940877491234355065569144896930081128892169042044460584550 ∧
r 58 = 13530439290334195123461135883479018102160530020573828556310705205007657426531168222845267832154258915552077758695870547161451592553201757208235114669067033546506286268525644984209563061752893538537245727269 / 2174774510478498224736179492882261487661050920345209052654298823288346005246886234411414465360628354503363235912647440635882326083647002338444270460678806075426147442420032739736200222486882628185299642261392074115165321450 ∧
r 59 = 575036365224142176549557972960792401892643933350466454371918100412412971297422931568155615545322194948506149669732040287690842251996221220639368584504554591045666926100230376653342614117168461627403099246222822910705766139 / 208945358400124104949235415244691686114962683800358894460826058310106658811443985405572795329331717950013243329535403617448660300734306322775707283805867223434719156807351560923670145333707376980063290573359754503462073691363759616778262450 ∧
r 60 = 122540537298811081787554294908318876860372406152460299283777662198098217662773335223345710071119759659686279915472401339021892987080447397300047204812597448933144587150850904333062193701401976701479325018660830279102201614410150104123644243 / 120448798493643987670593566453438201063416656796404566564359731723408761251570315791261128143224656578079675899796472567165097293912530926952910833137360264577005092035542403362619104429371181816825044452427808354064179620507384745919782717533006498380163150 ∧
r 61 = 481911530313702823199688566801587999878141309126864033454464576361934382525679879400612226733440039413542369946350682895603880716260765622402501592726925153711825200963655376896979987420389115951869457334063798859287989978009289894830407929161239 / 3212647812998803962430237159045270718043979792653966281224804280403324460226632701152727892046940583118736898378576353014395863368493431680806320096708778695840163263355610036175222527881665695855902618223979209467997912798034943739828425694465502089816707767539650 ∧
r 62 = 481911530313702823199688566801587999878141309126864033454464576361934382525679879400612226733440039413542369946350682895603880716260765622402501592726925153711825200963655376896979987420389115951869457334063798859287989978009289894830407929161239 / 3212647812998803962430237159045270718043979792653966281224804280403324460226632701152727892046940583118736898378576353014395863368493431680806320096708778695840163263355610036175222527881665695855902618223979209467997912798034943739828425694465502089816707767539650 ∧
r 63 = 481911530313702823199688566801587999878141309126864033454464576361934382525679879400612226733440039413542369946350682895603880716260765622402501592726925153711825200963655376896979987420389115951869457334063798859287989978009289894830407929161239 / 3212647812998803962430237159045270718043979792653966281224804280403324460226632701152727892046940583118736898378576353014395863368493431680806320096708778695840163263355610036175222527881665695855902618223979209467997912798034943739828425694465502089816707767539650 ∧
r 64 = 8048763716019973698502388369119050162801369194007823389218812806080971929153589774583918578332999720638682917277694095491865889315713519158242374179229177270147051859294286358957245234130770334542150581649154454782167749492850889449860772858057703657648401 / 193553167709305267953039471956075321100700279238345312815503511435274760560763667152195609660494142061645655404022610538081841829773431029405700662478077997116082761037326028592789847426537440986931396746554714620619606818651759356704187703089196440734480775469225194021436850 ∧
r 65 = 8048763716019973698502388369119050162801369194007823389218812806080971929153589774583918578332999720638682917277694095491865889315713519158242374179229177270147051859294286358957245234130770334542150581649154454782167749492850889449860772858057703657648401 / 193553167709305267953039471956075321100700279238345312815503511435274760560763667152195609660494142061645655404022610538081841829773431029405700662478077997116082761037326028592789847426537440986931396746554714620619606818651759356704187703089196440734480775469225194021436850 ∧
r 66 = 407188854206838223647708076247283161846499777423034694492943360482135632116747857491287309186023039085039011547273157697294772044296151791058934478070156810174326798350402000053472771812951986905227286176145679892235130039050138032888616893913757526970900952284918205661 / 28122335288450643321298259765041266230974318006908246854900456191763861850619549099411034907572721724737166437423306356558371344379707144474817848022592079392437421413207179507314556794737474020122496148137670787743514852948411824098475027348717241770421924037313766742452154446717691790350 ∧
r 67 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 ∧
r 68 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 ∧
r 69 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 ∧
r 70 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 ∧
r 71 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 ∧
r 72 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 ∧
r 73 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 ∧
r 74 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 ∧
r 75 = 159964742255280287252007403680852356718468955486655582796138215043268508523404698399092363050236460750020965043497268463261460813104623030344176518783847346908302141162051473749502547418078740588025473883244848090485920191077491746663073295302807911847290317196943416398797297243804402225308642529514099 / 5991615048287496872973786254379493828285679024998760976850704496994359646577100787089412393551004381083960434983220620346300807882132714002552937788602375656459552354649787559992629326866999071212873512973392403929715070563144240802326570360892832376505271838369324405361909504615297187691606917709989831007596911499462418150 ∧
r 76 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 ∧
r 77 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 ∧
r 78 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 ∧
r 79 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 ∧
r 80 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 ∧
r 81 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 ∧
r 82 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 ∧
r 83 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 ∧
r 84 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 ∧
r 85 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 ∧
r 86 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 ∧
r 87 = 2282074496642673776260768825238797350444591093432047699080242255305205892697221899727430224539768138483840882757379412130118108590650658064506054831375799629136183685930304075867961412852921974736582118770738057838549640338377085026802986387405501468831461075878050587213266253369778685819799541124657252873155959941008808846879901517869328869456285957624995229 / 265317241810557507380526149530850180254452898359821411986845851562677563831912203833914503581009138564266606920502256299450743021984270794162590933028315745966580987541693744354898707749543166513580742193509746730032205826657540706189083618947955651725032930464089061027562381711879362817617142758055067187490721762435122970327338796192603808167802793568121892214293687744322005236076150 ∧
r 88 = 23367331058921374616615207499262436035856746986047844280626339436870958291313779858280158825389623139014543875063122503853605095459172944543557922575453129251484013390961492319118333117986934520495895766587427989931367752620373401851764206656520615546375164359705563335484058837479235396890766007707872995694606945243518850940965289959275023803608491983782060389338553366599829 / 10924641221290394633676715177212711022334407879583031671968036680192101044070310606814717946527149436351707378686347555961869667410954701112777255058988460110773547723742724745629101249248549122926701508987033300471557533755647394952987986734020789236912876791862293318417134338752081063425186941945958230463654220910562360481283638476530381724103183465784872007702460747679783474225968644022518231618650 ∧
r 89 = 23367331058921374616615207499262436035856746986047844280626339436870958291313779858280158825389623139014543875063122503853605095459172944543557922575453129251484013390961492319118333117986934520495895766587427989931367752620373401851764206656520615546375164359705563335484058837479235396890766007707872995694606945243518850940965289959275023803608491983782060389338553366599829 / 10924641221290394633676715177212711022334407879583031671968036680192101044070310606814717946527149436351707378686347555961869667410954701112777255058988460110773547723742724745629101249248549122926701508987033300471557533755647394952987986734020789236912876791862293318417134338752081063425186941945958230463654220910562360481283638476530381724103183465784872007702460747679783474225968644022518231618650 ∧
r 90 = 3539036143247411942363317528160010236417878256559156557439946970859330270341139842034767600089174976756089489486873630374377741568860487924221017915515239226168163422567198170803806467131679016480182589590561479236094757769405184121295462056292942454224626240562626129537660001345182309413768264477884827351875112598111465376573853220171893799327698686816244141491348270598935682423159625338830785860369 / 6762025391331457939022650246359620955027430161278254949252380113744059778741616694439991289265407750129663538246610756564895329700142309618314734053731499737525673306378809301500714844366979576943751732134939213905622267379049847571441327374700154660524987518509706510342956483163140948966609646122655416369705305850263916330487471383579465953294031045973341623805221219194412667768502808686207913733319219244908727997517240970150 ∧
r 91 = 3539036143247411942363317528160010236417878256559156557439946970859330270341139842034767600089174976756089489486873630374377741568860487924221017915515239226168163422567198170803806467131679016480182589590561479236094757769405184121295462056292942454224626240562626129537660001345182309413768264477884827351875112598111465376573853220171893799327698686816244141491348270598935682423159625338830785860369 / 6762025391331457939022650246359620955027430161278254949252380113744059778741616694439991289265407750129663538246610756564895329700142309618314734053731499737525673306378809301500714844366979576943751732134939213905622267379049847571441327374700154660524987518509706510342956483163140948966609646122655416369705305850263916330487471383579465953294031045973341623805221219194412667768502808686207913733319219244908727997517240970150 ∧
r 92 = 1922797628928914421157211581250125666244367330545267684475844413272673032955536964797159579258485037740904420183280641420369636194569664263201931890792616436052065579772022975455932586311030203214564139485925604184330521617836531667769741236123389649790179236551407939259327559599285354366417122231020441547483478920007619216396378213134514079432509869564823812436258407770279069827839642858847030312365324818253992421000649 / 16094065175420312418976442914756120349395968539071838616061710926185427022760216874223822139247851367032545214029105992881776408910481938691597572180788857134642428800952435493681759530831486356432449149474485664195498245469778538982696896819808589647245843797423112414808704142631619009891595581387901743793037087126730343033959855448712939628479441427038758847089364734264650581323362592719606114734516547220985984427484054751638579260270936963170650 ∧
r 93 = 1922797628928914421157211581250125666244367330545267684475844413272673032955536964797159579258485037740904420183280641420369636194569664263201931890792616436052065579772022975455932586311030203214564139485925604184330521617836531667769741236123389649790179236551407939259327559599285354366417122231020441547483478920007619216396378213134514079432509869564823812436258407770279069827839642858847030312365324818253992421000649 / 16094065175420312418976442914756120349395968539071838616061710926185427022760216874223822139247851367032545214029105992881776408910481938691597572180788857134642428800952435493681759530831486356432449149474485664195498245469778538982696896819808589647245843797423112414808704142631619009891595581387901743793037087126730343033959855448712939628479441427038758847089364734264650581323362592719606114734516547220985984427484054751638579260270936963170650 ∧
r 94 = 421200028990351211773809617704358922232415859245126380838392897277152007549468876931735597216254130091947449673178431182242150304686934121878907617992778857740031039018795156230610394398106485709729510932310800119608672587637111828199133470925040115710902775360528392706820740420787097896335090198662810782741171033311656358975754686785155156891071370866234035701061764361908089577479531972349540475819773226492470317497299485147969744475771042971387 / 22769700200595762447252288874412593725714991138088344743316097712058365740967734456112561014662512467039386157196278487662525599644949768439108311893225253688001117962311959784992353509304780743163850890965897048053930436417283752757575669914781036279750856527698070883654581753619767223427706174560218009664532416566425408819434730731053356895154565357301382503564552964003245343140244800591166150664221084448146370389083787874983476753865658857743882047246280942843383017633450 ∧
r 95 = 421200028990351211773809617704358922232415859245126380838392897277152007549468876931735597216254130091947449673178431182242150304686934121878907617992778857740031039018795156230610394398106485709729510932310800119608672587637111828199133470925040115710902775360528392706820740420787097896335090198662810782741171033311656358975754686785155156891071370866234035701061764361908089577479531972349540475819773226492470317497299485147969744475771042971387 / 22769700200595762447252288874412593725714991138088344743316097712058365740967734456112561014662512467039386157196278487662525599644949768439108311893225253688001117962311959784992353509304780743163850890965897048053930436417283752757575669914781036279750856527698070883654581753619767223427706174560218009664532416566425408819434730731053356895154565357301382503564552964003245343140244800591166150664221084448146370389083787874983476753865658857743882047246280942843383017633450 ∧
r 96 = 421200028990351211773809617704358922232415859245126380838392897277152007549468876931735597216254130091947449673178431182242150304686934121878907617992778857740031039018795156230610394398106485709729510932310800119608672587637111828199133470925040115710902775360528392706820740420787097896335090198662810782741171033311656358975754686785155156891071370866234035701061764361908089577479531972349540475819773226492470317497299485147969744475771042971387 / 22769700200595762447252288874412593725714991138088344743316097712058365740967734456112561014662512467039386157196278487662525599644949768439108311893225253688001117962311959784992353509304780743163850890965897048053930436417283752757575669914781036279750856527698070883654581753619767223427706174560218009664532416566425408819434730731053356895154565357301382503564552964003245343140244800591166150664221084448146370389083787874983476753865658857743882047246280942843383017633450 ∧
r 97 = 574683659394598440680245744935850408685320969178434055381507638912219027706457263497539495397985872063212051487654576573907024523037206353160129808073130288697853902815923856146182036139967811666691660954581277476389266212011915354440034074019071179564277357117516773760005707863747846985704496970625947286805232071970785213419754548992839986325860468381991906516105146277173556771139227849493495439903572908331020354143726017391984099768061770423737824163237 / 97793625488980793383841525097995356633150866423075026011643401043167545955664392559738215516093971615371914062901319299308197971622675735225668510019950386034267746106302367711924840458647632699533311903150850222631527454340090520555200350807747792647306842342068789914510889289340006372309735705309253730252115295152726061813735156041361879913960835120263301922293987302275308033968086664030093341531354455289673559369834215720816982156080181785549447491694337222118786069631398457505450 ∧
r 98 = 574683659394598440680245744935850408685320969178434055381507638912219027706457263497539495397985872063212051487654576573907024523037206353160129808073130288697853902815923856146182036139967811666691660954581277476389266212011915354440034074019071179564277357117516773760005707863747846985704496970625947286805232071970785213419754548992839986325860468381991906516105146277173556771139227849493495439903572908331020354143726017391984099768061770423737824163237 / 97793625488980793383841525097995356633150866423075026011643401043167545955664392559738215516093971615371914062901319299308197971622675735225668510019950386034267746106302367711924840458647632699533311903150850222631527454340090520555200350807747792647306842342068789914510889289340006372309735705309253730252115295152726061813735156041361879913960835120263301922293987302275308033968086664030093341531354455289673559369834215720816982156080181785549447491694337222118786069631398457505450 ∧
r 99 = 1161253982954115450632071110849528470792494251823669704195891048507909683961669550088715655436330185205983763927901688679489127521003965331376582880032423003281765596557449339474675004089201894144832757183875252874355250984054809052914829031112638493532250971491336405217204084079023968083739549128007221249451900079648014920892729225328437696698036636361730691160479552926955312903539482434838075758639303980691247610301230929503368330302600664849470782584066272028869839 / 426766797782349344100583430358846750964823536309783372046770841116704164267958590422457444493100456265031415212538945525323151306892367836417014838329016866995025124428017812577530045918933128526494194832182867616997302919275351402578931231623862459740463397183417231572130288594375862693574979236303859822646981398531145082686804466115213458533412355713050825517858157571983938938499020501789645999094570966141564893442241222299292590343811955066132768784809995353690988188981260498694410488921268650 ∧
r 100 = 493194876819595682416230825422962914766142554534757606805596000406205047287947302235621696937995691438111870808133487161585734431117036904531160037728958452112516155227623049266632659898265889611070794228324109273048769645189389196373819538040191672739776835073585190189130130250621286217345831542364037295204530177468125642161555537278312899418846717150463420137601137323867684024867443402772128918887917464532087156288032289765368512689837500943156797171821259067456275051384307218945201 / 431367556096659183461813462034098034301924646541448507656611797171215848597996775821001858054438934523961038087543256221766158297120930142251581973321903116546795768085833633375811957742227290711439329146698525913668229877785142086467084198608809858488200226275994330891980275563548884837623422868106630147398229952130785101061543553632324695844746010940320668028940180071385716206994081607649537082973298037867775819070749780467398781681185348645683658246956216740413728849861746611819717559009474875848841639720437850 ∧
r 101 = 167957767397664854045821899531172964829817499952431862669492433107247389252964034728062742778414655188479990722394436597415176502956620950223269873488898280121755560007365838515644187621752596426016075217895015258986489758362689583198372176424813015717638476275834951517147544720139124367157212985565141915856127464101183795558840083531566005572177496731179002611623496742650796159901063943304826312020030262330202382855279370234130468836156740490622182129566192916650902624234683151192394888233431307 / 473830918267472574175258513129986452743223015915862785528202489246551712618137127912249851741941297469648287545053699189791774687390521417468435642174794621396598061921250411544186059725798272912379009411412190496365336129355487964993794460406898705655108628177502890608412889247520649913971137714050675097727592659143286788688385544420998507797576313314888896792418201873055580877901172822953493363228138191107988774906502228997322398171417565290596353686393484628769683750302387214983797782848689486817493892324153198305635164250 := by
have v1 : r 1 = 1 / 2 := by rw [hrs 0, h0]; norm_num
have v2 : r 2 = 1 / 2 := by rw [hrs 1, v1]; norm_num
have v3 : r 3 = 1 / 6 := by rw [hrs 2, v2]; norm_num
have v4 : r 4 = 1 / 42 := by rw [hrs 3, v3]; norm_num
have v5 : r 5 = 1 / 42 := by rw [hrs 4, v4]; norm_num
have v6 : r 6 = 1 / 42 := by rw [hrs 5, v5]; norm_num
have v7 : r 7 = 1 / 126 := by rw [hrs 6, v6]; norm_num
have v8 : r 8 = 1 / 16002 := by rw [hrs 7, v7]; norm_num
have v9 : r 9 = 1 / 16002 := by rw [hrs 8, v8]; norm_num
have v10 : r 10 = 1 / 16002 := by rw [hrs 9, v9]; norm_num
have v11 : r 11 = 1 / 16002 := by rw [hrs 10, v10]; norm_num
have v12 : r 12 = 1 / 16002 := by rw [hrs 11, v11]; norm_num
have v13 : r 13 = 1 / 16002 := by rw [hrs 12, v12]; norm_num
have v14 : r 14 = 1 / 16002 := by rw [hrs 13, v13]; norm_num
have v15 : r 15 = 1 / 688086 := by rw [hrs 14, v14]; norm_num
have v16 : r 16 = 1 / 688086 := by rw [hrs 15, v15]; norm_num
have v17 : r 17 = 1 / 688086 := by rw [hrs 16, v16]; norm_num
have v18 : r 18 = 1 / 688086 := by rw [hrs 17, v17]; norm_num
have v19 : r 19 = 1 / 688086 := by rw [hrs 18, v18]; norm_num
have v20 : r 20 = 1 / 688086 := by rw [hrs 19, v19]; norm_num
have v21 : r 21 = 120163 / 240503259150 := by rw [hrs 20, v20]; norm_num
have v22 : r 22 = 12932167 / 567347188334850 := by rw [hrs 21, v21]; norm_num
have v23 : r 23 = 12932167 / 567347188334850 := by rw [hrs 22, v22]; norm_num
have v24 : r 24 = 12932167 / 567347188334850 := by rw [hrs 23, v23]; norm_num
have v25 : r 25 = 12932167 / 567347188334850 := by rw [hrs 24, v24]; norm_num
have v26 : r 26 = 12932167 / 567347188334850 := by rw [hrs 25, v25]; norm_num
have v27 : r 27 = 100171945053757 / 12691341578466215591850 := by rw [hrs 26, v26]; norm_num
have v28 : r 28 = 107644170831134536927 / 243343288463189657575723817850 := by rw [hrs 27, v27]; norm_num
have v29 : r 29 = 107644170831134536927 / 243343288463189657575723817850 := by rw [hrs 28, v28]; norm_num
have v30 : r 30 = 107644170831134536927 / 243343288463189657575723817850 := by rw [hrs 29, v29]; norm_num
have v31 : r 31 = 107644170831134536927 / 243343288463189657575723817850 := by rw [hrs 30, v30]; norm_num
have v32 : r 32 = 107644170831134536927 / 243343288463189657575723817850 := by rw [hrs 31, v31]; norm_num
have v33 : r 33 = 14598993650261743084714065641 / 69676764360476692711332185574552481050 := by rw [hrs 32, v32]; norm_num
have v34 : r 34 = 7961090884242287202286887174188286683 / 85502692624144962281478559794068509473752428650 := by rw [hrs 33, v33]; norm_num
have v35 : r 35 = 17089269107037109310175073431588929983696187113 / 489641691359023146408090293693780137366287632111847097650 := by rw [hrs 34, v34]; norm_num
have v36 : r 36 = 24775495057665137934850160116999839971296655500713733 / 4273294490391516376753649556370453526829302383904245353406731150 := by rw [hrs 35, v35]; norm_num
have v37 : r 37 = 24775495057665137934850160116999839971296655500713733 / 4273294490391516376753649556370453526829302383904245353406731150 := by rw [hrs 36, v36]; norm_num
have v38 : r 38 = 24775495057665137934850160116999839971296655500713733 / 4273294490391516376753649556370453526829302383904245353406731150 := by rw [hrs 37, v37]; norm_num
have v39 : r 39 = 845647244845372609119117317639626159048890492622691072083139023 / 391544748423291282081983403730543585794163711509479738425458531026506458150 := by rw [hrs 38, v38]; norm_num
have v40 : r 40 = 1279361336100174444251942992473714966534258700082741704514992885791523 / 3754190171139528729585651254462415212675896584673329663463798639720328923217380650 := by rw [hrs 39, v39]; norm_num
have v41 : r 41 = 1279361336100174444251942992473714966534258700082741704514992885791523 / 3754190171139528729585651254462415212675896584673329663463798639720328923217380650 := by rw [hrs 40, v40]; norm_num
have v42 : r 42 = 1279361336100174444251942992473714966534258700082741704514992885791523 / 3754190171139528729585651254462415212675896584673329663463798639720328923217380650 := by rw [hrs 41, v41]; norm_num
have v43 : r 43 = 2307178909358625844288230048113688514917493874182843861668184598259080687 / 20343956537405106185624644147931828037490683592344773446310324828644462434914985742350 := by rw [hrs 42, v42]; norm_num
have v44 : r 44 = 2307178909358625844288230048113688514917493874182843861668184598259080687 / 20343956537405106185624644147931828037490683592344773446310324828644462434914985742350 := by rw [hrs 43, v43]; norm_num
have v45 : r 45 = 659318159054952992368158389296038659826449069734600364727101743112098359598562611 / 11655908428123218204725844561756938739161153600678265505596657245523679800986195160837595468050 := by rw [hrs 44, v44]; norm_num
have v46 : r 46 = 728602171895038678636394825276913166726248096645486542004397068685941640433698111948589851 / 25888884487622534734603867774700751495820189468709549988355020113039400587330235326362886993608342757550 := by rw [hrs 45, v45]; norm_num
have v47 : r 47 = 8460645117916361525949041843570964695646901621569788945241573199933079840413055250334293685177039980221 / 607256096518192733364976633800564606357882531919006885021700723676812860062069999895812681580588233238576338844868550 := by rw [hrs 46, v46]; norm_num
have v48 : r 48 = 583473847243115429710805323201397105794687109693978440309296238195743045193725738895896654861024781126198971055118717 / 85463697812430478601160467988164408038970436424688174871843944772162618813142138992772085377175290216341013777227236169933007265850 := by rw [hrs 47, v47]; norm_num
have v49 : r 49 = 57235566419689740527216894644994090719061380449165398277406761889413767481516239955879524226149880396024414727845120310098331 / 17479494673046627672470862948133885139494627045732135374353110002317959629414713279514555065754621917880396537985539383414639696059681412050 := by rw [hrs 48, v48]; norm_num
have v50 : r 50 = 116072950999685541383889664443572968628785973521095383728800241565844348269673906801493179079294274435122845507376543935730052352256689133 / 77480950488343722797022987731006171783678220639000435235009231243407940099381827934169581918016008090643185870271101231402724248618403158229303693245650 := by rw [hrs 49, v49]; norm_num
have v51 : r 51 = 52009358972776708178754179196384591028396521395320498229273554009840029694048630162582390457279735168652989630775356150931336575678539518770484821183 / 85274481854256190162461282209750638404229496029888703103179320728362117630070146079717615316644475894677228969932350223380505975143341603386178767416794463169725650 := by rw [hrs 50, v50]; norm_num
have v52 : r 52 = 34703310191239350769791367194664875178207907367958832542389658785757420961031869707529629835487322095292587580834041950889210513131813649056401396910662146983 / 209287945738809026219275100016580785098653830240066914142002489661478086867667048653939453375339890321169299805069374587184442865964663479716191899209781729053151957374213150 := by rw [hrs 51, v51]; norm_num
have v53 : r 53 = 34703310191239350769791367194664875178207907367958832542389658785757420961031869707529629835487322095292587580834041950889210513131813649056401396910662146983 / 209287945738809026219275100016580785098653830240066914142002489661478086867667048653939453375339890321169299805069374587184442865964663479716191899209781729053151957374213150 := by rw [hrs 52, v52]; norm_num
have v54 : r 54 = 103291683952767491891750666081103226355445470584688441325011751615328556690820348361282592828209747923435398251461622534779356283796512611067700294596444193396392448262867003 / 1885098228884873624011666960437368710807715308673609950293344297722004703388546146422304622652660491593324418280896776831792432687454926388554749762781569931017735810002476605563665676231650 := by rw [hrs 53, v53]; norm_num
have v55 : r 55 = 103291683952767491891750666081103226355445470584688441325011751615328556690820348361282592828209747923435398251461622534779356283796512611067700294596444193396392448262867003 / 1885098228884873624011666960437368710807715308673609950293344297722004703388546146422304622652660491593324418280896776831792432687454926388554749762781569931017735810002476605563665676231650 := by rw [hrs 54, v54]; norm_num
have v56 : r 56 = 28938917471616433418063823334248580477925844332221809806946710850025199523666410189545280477180319867467850932655442170871209577637393520505272503891542587694137356662057229169799115843 / 1070296759211774725790722296265701945389278514404776283394742030382279204391468452707922952872717892265133839389903409221994041786988893799546129514616776566503136411715372889274746954488854107634141150 := by rw [hrs 55, v55]; norm_num
have v57 : r 57 = 728855957470306119334593881931744942956142754004476924984700530768600816655305995140906089684413857284101903609145096158189222185393049431628902589347323399187883947612398562037347430239561427101 / 55382379421561065182045979674407837221285399325700332325063054260807863800561242927602172086732743266112478175431395232227810531545303976647967939928233628940877491234355065569144896930081128892169042044460584550 := by rw [hrs 56, v56]; norm_num
have v58 : r 58 = 13530439290334195123461135883479018102160530020573828556310705205007657426531168222845267832154258915552077758695870547161451592553201757208235114669067033546506286268525644984209563061752893538537245727269 / 2174774510478498224736179492882261487661050920345209052654298823288346005246886234411414465360628354503363235912647440635882326083647002338444270460678806075426147442420032739736200222486882628185299642261392074115165321450 := by rw [hrs 57, v57]; norm_num
have v59 : r 59 = 575036365224142176549557972960792401892643933350466454371918100412412971297422931568155615545322194948506149669732040287690842251996221220639368584504554591045666926100230376653342614117168461627403099246222822910705766139 / 208945358400124104949235415244691686114962683800358894460826058310106658811443985405572795329331717950013243329535403617448660300734306322775707283805867223434719156807351560923670145333707376980063290573359754503462073691363759616778262450 := by rw [hrs 58, v58]; norm_num
have v60 : r 60 = 122540537298811081787554294908318876860372406152460299283777662198098217662773335223345710071119759659686279915472401339021892987080447397300047204812597448933144587150850904333062193701401976701479325018660830279102201614410150104123644243 / 120448798493643987670593566453438201063416656796404566564359731723408761251570315791261128143224656578079675899796472567165097293912530926952910833137360264577005092035542403362619104429371181816825044452427808354064179620507384745919782717533006498380163150 := by rw [hrs 59, v59]; norm_num
have v61 : r 61 = 481911530313702823199688566801587999878141309126864033454464576361934382525679879400612226733440039413542369946350682895603880716260765622402501592726925153711825200963655376896979987420389115951869457334063798859287989978009289894830407929161239 / 3212647812998803962430237159045270718043979792653966281224804280403324460226632701152727892046940583118736898378576353014395863368493431680806320096708778695840163263355610036175222527881665695855902618223979209467997912798034943739828425694465502089816707767539650 := by rw [hrs 60, v60]; norm_num
have v62 : r 62 = 481911530313702823199688566801587999878141309126864033454464576361934382525679879400612226733440039413542369946350682895603880716260765622402501592726925153711825200963655376896979987420389115951869457334063798859287989978009289894830407929161239 / 3212647812998803962430237159045270718043979792653966281224804280403324460226632701152727892046940583118736898378576353014395863368493431680806320096708778695840163263355610036175222527881665695855902618223979209467997912798034943739828425694465502089816707767539650 := by rw [hrs 61, v61]; norm_num
have v63 : r 63 = 481911530313702823199688566801587999878141309126864033454464576361934382525679879400612226733440039413542369946350682895603880716260765622402501592726925153711825200963655376896979987420389115951869457334063798859287989978009289894830407929161239 / 3212647812998803962430237159045270718043979792653966281224804280403324460226632701152727892046940583118736898378576353014395863368493431680806320096708778695840163263355610036175222527881665695855902618223979209467997912798034943739828425694465502089816707767539650 := by rw [hrs 62, v62]; norm_num
have v64 : r 64 = 8048763716019973698502388369119050162801369194007823389218812806080971929153589774583918578332999720638682917277694095491865889315713519158242374179229177270147051859294286358957245234130770334542150581649154454782167749492850889449860772858057703657648401 / 193553167709305267953039471956075321100700279238345312815503511435274760560763667152195609660494142061645655404022610538081841829773431029405700662478077997116082761037326028592789847426537440986931396746554714620619606818651759356704187703089196440734480775469225194021436850 := by rw [hrs 63, v63]; norm_num
have v65 : r 65 = 8048763716019973698502388369119050162801369194007823389218812806080971929153589774583918578332999720638682917277694095491865889315713519158242374179229177270147051859294286358957245234130770334542150581649154454782167749492850889449860772858057703657648401 / 193553167709305267953039471956075321100700279238345312815503511435274760560763667152195609660494142061645655404022610538081841829773431029405700662478077997116082761037326028592789847426537440986931396746554714620619606818651759356704187703089196440734480775469225194021436850 := by rw [hrs 64, v64]; norm_num
have v66 : r 66 = 407188854206838223647708076247283161846499777423034694492943360482135632116747857491287309186023039085039011547273157697294772044296151791058934478070156810174326798350402000053472771812951986905227286176145679892235130039050138032888616893913757526970900952284918205661 / 28122335288450643321298259765041266230974318006908246854900456191763861850619549099411034907572721724737166437423306356558371344379707144474817848022592079392437421413207179507314556794737474020122496148137670787743514852948411824098475027348717241770421924037313766742452154446717691790350 := by rw [hrs 65, v65]; norm_num
have v67 : r 67 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 := by rw [hrs 66, v66]; norm_num
have v68 : r 68 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 := by rw [hrs 67, v67]; norm_num
have v69 : r 69 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 := by rw [hrs 68, v68]; norm_num
have v70 : r 70 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 := by rw [hrs 69, v69]; norm_num
have v71 : r 71 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 := by rw [hrs 70, v70]; norm_num
have v72 : r 72 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 := by rw [hrs 71, v71]; norm_num
have v73 : r 73 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 := by rw [hrs 72, v72]; norm_num
have v74 : r 74 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 := by rw [hrs 73, v73]; norm_num
have v75 : r 75 = 159964742255280287252007403680852356718468955486655582796138215043268508523404698399092363050236460750020965043497268463261460813104623030344176518783847346908302141162051473749502547418078740588025473883244848090485920191077491746663073295302807911847290317196943416398797297243804402225308642529514099 / 5991615048287496872973786254379493828285679024998760976850704496994359646577100787089412393551004381083960434983220620346300807882132714002552937788602375656459552354649787559992629326866999071212873512973392403929715070563144240802326570360892832376505271838369324405361909504615297187691606917709989831007596911499462418150 := by rw [hrs 74, v74]; norm_num
have v76 : r 76 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 := by rw [hrs 75, v75]; norm_num
have v77 : r 77 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 := by rw [hrs 76, v76]; norm_num
have v78 : r 78 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 := by rw [hrs 77, v77]; norm_num
have v79 : r 79 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 := by rw [hrs 78, v78]; norm_num
have v80 : r 80 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 := by rw [hrs 79, v79]; norm_num
have v81 : r 81 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 := by rw [hrs 80, v80]; norm_num
have v82 : r 82 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 := by rw [hrs 81, v81]; norm_num
have v83 : r 83 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 := by rw [hrs 82, v82]; norm_num
have v84 : r 84 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 := by rw [hrs 83, v83]; norm_num
have v85 : r 85 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 := by rw [hrs 84, v84]; norm_num
have v86 : r 86 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 := by rw [hrs 85, v85]; norm_num
have v87 : r 87 = 2282074496642673776260768825238797350444591093432047699080242255305205892697221899727430224539768138483840882757379412130118108590650658064506054831375799629136183685930304075867961412852921974736582118770738057838549640338377085026802986387405501468831461075878050587213266253369778685819799541124657252873155959941008808846879901517869328869456285957624995229 / 265317241810557507380526149530850180254452898359821411986845851562677563831912203833914503581009138564266606920502256299450743021984270794162590933028315745966580987541693744354898707749543166513580742193509746730032205826657540706189083618947955651725032930464089061027562381711879362817617142758055067187490721762435122970327338796192603808167802793568121892214293687744322005236076150 := by rw [hrs 86, v86]; norm_num
have v88 : r 88 = 23367331058921374616615207499262436035856746986047844280626339436870958291313779858280158825389623139014543875063122503853605095459172944543557922575453129251484013390961492319118333117986934520495895766587427989931367752620373401851764206656520615546375164359705563335484058837479235396890766007707872995694606945243518850940965289959275023803608491983782060389338553366599829 / 10924641221290394633676715177212711022334407879583031671968036680192101044070310606814717946527149436351707378686347555961869667410954701112777255058988460110773547723742724745629101249248549122926701508987033300471557533755647394952987986734020789236912876791862293318417134338752081063425186941945958230463654220910562360481283638476530381724103183465784872007702460747679783474225968644022518231618650 := by rw [hrs 87, v87]; norm_num
have v89 : r 89 = 23367331058921374616615207499262436035856746986047844280626339436870958291313779858280158825389623139014543875063122503853605095459172944543557922575453129251484013390961492319118333117986934520495895766587427989931367752620373401851764206656520615546375164359705563335484058837479235396890766007707872995694606945243518850940965289959275023803608491983782060389338553366599829 / 10924641221290394633676715177212711022334407879583031671968036680192101044070310606814717946527149436351707378686347555961869667410954701112777255058988460110773547723742724745629101249248549122926701508987033300471557533755647394952987986734020789236912876791862293318417134338752081063425186941945958230463654220910562360481283638476530381724103183465784872007702460747679783474225968644022518231618650 := by rw [hrs 88, v88]; norm_num
have v90 : r 90 = 3539036143247411942363317528160010236417878256559156557439946970859330270341139842034767600089174976756089489486873630374377741568860487924221017915515239226168163422567198170803806467131679016480182589590561479236094757769405184121295462056292942454224626240562626129537660001345182309413768264477884827351875112598111465376573853220171893799327698686816244141491348270598935682423159625338830785860369 / 6762025391331457939022650246359620955027430161278254949252380113744059778741616694439991289265407750129663538246610756564895329700142309618314734053731499737525673306378809301500714844366979576943751732134939213905622267379049847571441327374700154660524987518509706510342956483163140948966609646122655416369705305850263916330487471383579465953294031045973341623805221219194412667768502808686207913733319219244908727997517240970150 := by rw [hrs 89, v89]; norm_num
have v91 : r 91 = 3539036143247411942363317528160010236417878256559156557439946970859330270341139842034767600089174976756089489486873630374377741568860487924221017915515239226168163422567198170803806467131679016480182589590561479236094757769405184121295462056292942454224626240562626129537660001345182309413768264477884827351875112598111465376573853220171893799327698686816244141491348270598935682423159625338830785860369 / 6762025391331457939022650246359620955027430161278254949252380113744059778741616694439991289265407750129663538246610756564895329700142309618314734053731499737525673306378809301500714844366979576943751732134939213905622267379049847571441327374700154660524987518509706510342956483163140948966609646122655416369705305850263916330487471383579465953294031045973341623805221219194412667768502808686207913733319219244908727997517240970150 := by rw [hrs 90, v90]; norm_num
have v92 : r 92 = 1922797628928914421157211581250125666244367330545267684475844413272673032955536964797159579258485037740904420183280641420369636194569664263201931890792616436052065579772022975455932586311030203214564139485925604184330521617836531667769741236123389649790179236551407939259327559599285354366417122231020441547483478920007619216396378213134514079432509869564823812436258407770279069827839642858847030312365324818253992421000649 / 16094065175420312418976442914756120349395968539071838616061710926185427022760216874223822139247851367032545214029105992881776408910481938691597572180788857134642428800952435493681759530831486356432449149474485664195498245469778538982696896819808589647245843797423112414808704142631619009891595581387901743793037087126730343033959855448712939628479441427038758847089364734264650581323362592719606114734516547220985984427484054751638579260270936963170650 := by rw [hrs 91, v91]; norm_num
have v93 : r 93 = 1922797628928914421157211581250125666244367330545267684475844413272673032955536964797159579258485037740904420183280641420369636194569664263201931890792616436052065579772022975455932586311030203214564139485925604184330521617836531667769741236123389649790179236551407939259327559599285354366417122231020441547483478920007619216396378213134514079432509869564823812436258407770279069827839642858847030312365324818253992421000649 / 16094065175420312418976442914756120349395968539071838616061710926185427022760216874223822139247851367032545214029105992881776408910481938691597572180788857134642428800952435493681759530831486356432449149474485664195498245469778538982696896819808589647245843797423112414808704142631619009891595581387901743793037087126730343033959855448712939628479441427038758847089364734264650581323362592719606114734516547220985984427484054751638579260270936963170650 := by rw [hrs 92, v92]; norm_num
have v94 : r 94 = 421200028990351211773809617704358922232415859245126380838392897277152007549468876931735597216254130091947449673178431182242150304686934121878907617992778857740031039018795156230610394398106485709729510932310800119608672587637111828199133470925040115710902775360528392706820740420787097896335090198662810782741171033311656358975754686785155156891071370866234035701061764361908089577479531972349540475819773226492470317497299485147969744475771042971387 / 22769700200595762447252288874412593725714991138088344743316097712058365740967734456112561014662512467039386157196278487662525599644949768439108311893225253688001117962311959784992353509304780743163850890965897048053930436417283752757575669914781036279750856527698070883654581753619767223427706174560218009664532416566425408819434730731053356895154565357301382503564552964003245343140244800591166150664221084448146370389083787874983476753865658857743882047246280942843383017633450 := by rw [hrs 93, v93]; norm_num
have v95 : r 95 = 421200028990351211773809617704358922232415859245126380838392897277152007549468876931735597216254130091947449673178431182242150304686934121878907617992778857740031039018795156230610394398106485709729510932310800119608672587637111828199133470925040115710902775360528392706820740420787097896335090198662810782741171033311656358975754686785155156891071370866234035701061764361908089577479531972349540475819773226492470317497299485147969744475771042971387 / 22769700200595762447252288874412593725714991138088344743316097712058365740967734456112561014662512467039386157196278487662525599644949768439108311893225253688001117962311959784992353509304780743163850890965897048053930436417283752757575669914781036279750856527698070883654581753619767223427706174560218009664532416566425408819434730731053356895154565357301382503564552964003245343140244800591166150664221084448146370389083787874983476753865658857743882047246280942843383017633450 := by rw [hrs 94, v94]; norm_num
have v96 : r 96 = 421200028990351211773809617704358922232415859245126380838392897277152007549468876931735597216254130091947449673178431182242150304686934121878907617992778857740031039018795156230610394398106485709729510932310800119608672587637111828199133470925040115710902775360528392706820740420787097896335090198662810782741171033311656358975754686785155156891071370866234035701061764361908089577479531972349540475819773226492470317497299485147969744475771042971387 / 22769700200595762447252288874412593725714991138088344743316097712058365740967734456112561014662512467039386157196278487662525599644949768439108311893225253688001117962311959784992353509304780743163850890965897048053930436417283752757575669914781036279750856527698070883654581753619767223427706174560218009664532416566425408819434730731053356895154565357301382503564552964003245343140244800591166150664221084448146370389083787874983476753865658857743882047246280942843383017633450 := by rw [hrs 95, v95]; norm_num
have v97 : r 97 = 574683659394598440680245744935850408685320969178434055381507638912219027706457263497539495397985872063212051487654576573907024523037206353160129808073130288697853902815923856146182036139967811666691660954581277476389266212011915354440034074019071179564277357117516773760005707863747846985704496970625947286805232071970785213419754548992839986325860468381991906516105146277173556771139227849493495439903572908331020354143726017391984099768061770423737824163237 / 97793625488980793383841525097995356633150866423075026011643401043167545955664392559738215516093971615371914062901319299308197971622675735225668510019950386034267746106302367711924840458647632699533311903150850222631527454340090520555200350807747792647306842342068789914510889289340006372309735705309253730252115295152726061813735156041361879913960835120263301922293987302275308033968086664030093341531354455289673559369834215720816982156080181785549447491694337222118786069631398457505450 := by rw [hrs 96, v96]; norm_num
have v98 : r 98 = 574683659394598440680245744935850408685320969178434055381507638912219027706457263497539495397985872063212051487654576573907024523037206353160129808073130288697853902815923856146182036139967811666691660954581277476389266212011915354440034074019071179564277357117516773760005707863747846985704496970625947286805232071970785213419754548992839986325860468381991906516105146277173556771139227849493495439903572908331020354143726017391984099768061770423737824163237 / 97793625488980793383841525097995356633150866423075026011643401043167545955664392559738215516093971615371914062901319299308197971622675735225668510019950386034267746106302367711924840458647632699533311903150850222631527454340090520555200350807747792647306842342068789914510889289340006372309735705309253730252115295152726061813735156041361879913960835120263301922293987302275308033968086664030093341531354455289673559369834215720816982156080181785549447491694337222118786069631398457505450 := by rw [hrs 97, v97]; norm_num
have v99 : r 99 = 1161253982954115450632071110849528470792494251823669704195891048507909683961669550088715655436330185205983763927901688679489127521003965331376582880032423003281765596557449339474675004089201894144832757183875252874355250984054809052914829031112638493532250971491336405217204084079023968083739549128007221249451900079648014920892729225328437696698036636361730691160479552926955312903539482434838075758639303980691247610301230929503368330302600664849470782584066272028869839 / 426766797782349344100583430358846750964823536309783372046770841116704164267958590422457444493100456265031415212538945525323151306892367836417014838329016866995025124428017812577530045918933128526494194832182867616997302919275351402578931231623862459740463397183417231572130288594375862693574979236303859822646981398531145082686804466115213458533412355713050825517858157571983938938499020501789645999094570966141564893442241222299292590343811955066132768784809995353690988188981260498694410488921268650 := by rw [hrs 98, v98]; norm_num
have v100 : r 100 = 493194876819595682416230825422962914766142554534757606805596000406205047287947302235621696937995691438111870808133487161585734431117036904531160037728958452112516155227623049266632659898265889611070794228324109273048769645189389196373819538040191672739776835073585190189130130250621286217345831542364037295204530177468125642161555537278312899418846717150463420137601137323867684024867443402772128918887917464532087156288032289765368512689837500943156797171821259067456275051384307218945201 / 431367556096659183461813462034098034301924646541448507656611797171215848597996775821001858054438934523961038087543256221766158297120930142251581973321903116546795768085833633375811957742227290711439329146698525913668229877785142086467084198608809858488200226275994330891980275563548884837623422868106630147398229952130785101061543553632324695844746010940320668028940180071385716206994081607649537082973298037867775819070749780467398781681185348645683658246956216740413728849861746611819717559009474875848841639720437850 := by rw [hrs 99, v99]; norm_num
have v101 : r 101 = 167957767397664854045821899531172964829817499952431862669492433107247389252964034728062742778414655188479990722394436597415176502956620950223269873488898280121755560007365838515644187621752596426016075217895015258986489758362689583198372176424813015717638476275834951517147544720139124367157212985565141915856127464101183795558840083531566005572177496731179002611623496742650796159901063943304826312020030262330202382855279370234130468836156740490622182129566192916650902624234683151192394888233431307 / 473830918267472574175258513129986452743223015915862785528202489246551712618137127912249851741941297469648287545053699189791774687390521417468435642174794621396598061921250411544186059725798272912379009411412190496365336129355487964993794460406898705655108628177502890608412889247520649913971137714050675097727592659143286788688385544420998507797576313314888896792418201873055580877901172822953493363228138191107988774906502228997322398171417565290596353686393484628769683750302387214983797782848689486817493892324153198305635164250 := by rw [hrs 100, v100]; norm_num
exact ⟨v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20, v21, v22, v23, v24, v25, v26, v27, v28, v29, v30, v31, v32, v33, v34, v35, v36, v37, v38, v39, v40, v41, v42, v43, v44, v45, v46, v47, v48, v49, v50, v51, v52, v53, v54, v55, v56, v57, v58, v59, v60, v61, v62, v63, v64, v65, v66, v67, v68, v69, v70, v71, v72, v73, v74, v75, v76, v77, v78, v79, v80, v81, v82, v83, v84, v85, v86, v87, v88, v89, v90, v91, v92, v93, v94, v95, v96, v97, v98, v99, v100, v101⟩
private theorem range_1_25 (r : ℕ → ℝ) (h0 : r 0 = 1 / 2)
(hrs : ∀ m : ℕ, r (m + 1) = if (1 : ℝ) / ((2 : ℝ) ^ m - 1) ≤ r m then r m - 1 / ((2 : ℝ) ^ m - 1) else r m) :
∀ m : ℕ, 1 ≤ m → m ≤ 25 → r m < (1 : ℝ) / ((2 : ℝ) ^ m - 1) →
∃ n : ℕ, m < n ∧ n ≤ 3 * m + 2 ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - 1) := by
intro m hm1 hm2 hlt
obtain ⟨v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20, v21, v22, v23, v24, v25, v26, v27, v28, v29, v30, v31, v32, v33, v34, v35, v36, v37, v38, v39, v40, v41, v42, v43, v44, v45, v46, v47, v48, v49, v50, v51, v52, v53, v54, v55, v56, v57, v58, v59, v60, v61, v62, v63, v64, v65, v66, v67, v68, v69, v70, v71, v72, v73, v74, v75, v76, v77, v78, v79, v80, v81, v82, v83, v84, v85, v86, v87, v88, v89, v90, v91, v92, v93, v94, v95, v96, v97, v98, v99, v100, v101⟩ := walk_values r h0 hrs
interval_cases m
· exact ⟨4, by norm_num, by norm_num, by rw [v4]; norm_num⟩
· rw [v2] at hlt; norm_num at hlt
· rw [v3] at hlt; norm_num at hlt
· exact ⟨5, by norm_num, by norm_num, by rw [v5]; norm_num⟩
· exact ⟨8, by norm_num, by norm_num, by rw [v8]; norm_num⟩
· rw [v6] at hlt; norm_num at hlt
· rw [v7] at hlt; norm_num at hlt
· exact ⟨9, by norm_num, by norm_num, by rw [v9]; norm_num⟩
· exact ⟨10, by norm_num, by norm_num, by rw [v10]; norm_num⟩
· exact ⟨11, by norm_num, by norm_num, by rw [v11]; norm_num⟩
· exact ⟨12, by norm_num, by norm_num, by rw [v12]; norm_num⟩
· exact ⟨13, by norm_num, by norm_num, by rw [v13]; norm_num⟩
· exact ⟨15, by norm_num, by norm_num, by rw [v15]; norm_num⟩
· rw [v14] at hlt; norm_num at hlt
· exact ⟨16, by norm_num, by norm_num, by rw [v16]; norm_num⟩
· exact ⟨17, by norm_num, by norm_num, by rw [v17]; norm_num⟩
· exact ⟨18, by norm_num, by norm_num, by rw [v18]; norm_num⟩
· exact ⟨19, by norm_num, by norm_num, by rw [v19]; norm_num⟩
· exact ⟨22, by norm_num, by norm_num, by rw [v22]; norm_num⟩
· rw [v20] at hlt; norm_num at hlt
· rw [v21] at hlt; norm_num at hlt
· exact ⟨23, by norm_num, by norm_num, by rw [v23]; norm_num⟩
· exact ⟨24, by norm_num, by norm_num, by rw [v24]; norm_num⟩
· exact ⟨25, by norm_num, by norm_num, by rw [v25]; norm_num⟩
· exact ⟨28, by norm_num, by norm_num, by rw [v28]; norm_num⟩
private theorem range_26_50 (r : ℕ → ℝ) (h0 : r 0 = 1 / 2)
(hrs : ∀ m : ℕ, r (m + 1) = if (1 : ℝ) / ((2 : ℝ) ^ m - 1) ≤ r m then r m - 1 / ((2 : ℝ) ^ m - 1) else r m) :
∀ m : ℕ, 26 ≤ m → m ≤ 50 → r m < (1 : ℝ) / ((2 : ℝ) ^ m - 1) →
∃ n : ℕ, m < n ∧ n ≤ 3 * m + 2 ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - 1) := by
intro m hm1 hm2 hlt
obtain ⟨v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20, v21, v22, v23, v24, v25, v26, v27, v28, v29, v30, v31, v32, v33, v34, v35, v36, v37, v38, v39, v40, v41, v42, v43, v44, v45, v46, v47, v48, v49, v50, v51, v52, v53, v54, v55, v56, v57, v58, v59, v60, v61, v62, v63, v64, v65, v66, v67, v68, v69, v70, v71, v72, v73, v74, v75, v76, v77, v78, v79, v80, v81, v82, v83, v84, v85, v86, v87, v88, v89, v90, v91, v92, v93, v94, v95, v96, v97, v98, v99, v100, v101⟩ := walk_values r h0 hrs
interval_cases m
· rw [v26] at hlt; norm_num at hlt
· rw [v27] at hlt; norm_num at hlt
· exact ⟨29, by norm_num, by norm_num, by rw [v29]; norm_num⟩
· exact ⟨30, by norm_num, by norm_num, by rw [v30]; norm_num⟩
· exact ⟨31, by norm_num, by norm_num, by rw [v31]; norm_num⟩
· exact ⟨36, by norm_num, by norm_num, by rw [v36]; norm_num⟩
· rw [v32] at hlt; norm_num at hlt
· rw [v33] at hlt; norm_num at hlt
· rw [v34] at hlt; norm_num at hlt
· rw [v35] at hlt; norm_num at hlt
· exact ⟨37, by norm_num, by norm_num, by rw [v37]; norm_num⟩
· exact ⟨40, by norm_num, by norm_num, by rw [v40]; norm_num⟩
· rw [v38] at hlt; norm_num at hlt
· rw [v39] at hlt; norm_num at hlt
· exact ⟨41, by norm_num, by norm_num, by rw [v41]; norm_num⟩
· exact ⟨43, by norm_num, by norm_num, by rw [v43]; norm_num⟩
· rw [v42] at hlt; norm_num at hlt
· exact ⟨52, by norm_num, by norm_num, by rw [v52]; norm_num⟩
· rw [v44] at hlt; norm_num at hlt
· rw [v45] at hlt; norm_num at hlt
· rw [v46] at hlt; norm_num at hlt
· rw [v47] at hlt; norm_num at hlt
· rw [v48] at hlt; norm_num at hlt
· rw [v49] at hlt; norm_num at hlt
· rw [v50] at hlt; norm_num at hlt
private theorem range_51_75 (r : ℕ → ℝ) (h0 : r 0 = 1 / 2)
(hrs : ∀ m : ℕ, r (m + 1) = if (1 : ℝ) / ((2 : ℝ) ^ m - 1) ≤ r m then r m - 1 / ((2 : ℝ) ^ m - 1) else r m) :
∀ m : ℕ, 51 ≤ m → m ≤ 75 → r m < (1 : ℝ) / ((2 : ℝ) ^ m - 1) →
∃ n : ℕ, m < n ∧ n ≤ 3 * m + 2 ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - 1) := by
intro m hm1 hm2 hlt
obtain ⟨v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20, v21, v22, v23, v24, v25, v26, v27, v28, v29, v30, v31, v32, v33, v34, v35, v36, v37, v38, v39, v40, v41, v42, v43, v44, v45, v46, v47, v48, v49, v50, v51, v52, v53, v54, v55, v56, v57, v58, v59, v60, v61, v62, v63, v64, v65, v66, v67, v68, v69, v70, v71, v72, v73, v74, v75, v76, v77, v78, v79, v80, v81, v82, v83, v84, v85, v86, v87, v88, v89, v90, v91, v92, v93, v94, v95, v96, v97, v98, v99, v100, v101⟩ := walk_values r h0 hrs
interval_cases m
· rw [v51] at hlt; norm_num at hlt
· exact ⟨54, by norm_num, by norm_num, by rw [v54]; norm_num⟩
· rw [v53] at hlt; norm_num at hlt
· exact ⟨61, by norm_num, by norm_num, by rw [v61]; norm_num⟩
· rw [v55] at hlt; norm_num at hlt
· rw [v56] at hlt; norm_num at hlt
· rw [v57] at hlt; norm_num at hlt
· rw [v58] at hlt; norm_num at hlt
· rw [v59] at hlt; norm_num at hlt
· rw [v60] at hlt; norm_num at hlt
· exact ⟨62, by norm_num, by norm_num, by rw [v62]; norm_num⟩
· exact ⟨64, by norm_num, by norm_num, by rw [v64]; norm_num⟩
· rw [v63] at hlt; norm_num at hlt
· exact ⟨67, by norm_num, by norm_num, by rw [v67]; norm_num⟩
· rw [v65] at hlt; norm_num at hlt
· rw [v66] at hlt; norm_num at hlt
· exact ⟨68, by norm_num, by norm_num, by rw [v68]; norm_num⟩
· exact ⟨69, by norm_num, by norm_num, by rw [v69]; norm_num⟩
· exact ⟨71, by norm_num, by norm_num, by rw [v71]; norm_num⟩
· rw [v70] at hlt; norm_num at hlt
· exact ⟨72, by norm_num, by norm_num, by rw [v72]; norm_num⟩
· exact ⟨73, by norm_num, by norm_num, by rw [v73]; norm_num⟩
· exact ⟨76, by norm_num, by norm_num, by rw [v76]; norm_num⟩
· rw [v74] at hlt; norm_num at hlt
· rw [v75] at hlt; norm_num at hlt
private theorem range_76_100 (r : ℕ → ℝ) (h0 : r 0 = 1 / 2)
(hrs : ∀ m : ℕ, r (m + 1) = if (1 : ℝ) / ((2 : ℝ) ^ m - 1) ≤ r m then r m - 1 / ((2 : ℝ) ^ m - 1) else r m) :
∀ m : ℕ, 76 ≤ m → m ≤ 100 → r m < (1 : ℝ) / ((2 : ℝ) ^ m - 1) →
∃ n : ℕ, m < n ∧ n ≤ 3 * m + 2 ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - 1) := by
intro m hm1 hm2 hlt
obtain ⟨v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20, v21, v22, v23, v24, v25, v26, v27, v28, v29, v30, v31, v32, v33, v34, v35, v36, v37, v38, v39, v40, v41, v42, v43, v44, v45, v46, v47, v48, v49, v50, v51, v52, v53, v54, v55, v56, v57, v58, v59, v60, v61, v62, v63, v64, v65, v66, v67, v68, v69, v70, v71, v72, v73, v74, v75, v76, v77, v78, v79, v80, v81, v82, v83, v84, v85, v86, v87, v88, v89, v90, v91, v92, v93, v94, v95, v96, v97, v98, v99, v100, v101⟩ := walk_values r h0 hrs
interval_cases m
· exact ⟨77, by norm_num, by norm_num, by rw [v77]; norm_num⟩
· exact ⟨78, by norm_num, by norm_num, by rw [v78]; norm_num⟩
· exact ⟨79, by norm_num, by norm_num, by rw [v79]; norm_num⟩
· exact ⟨80, by norm_num, by norm_num, by rw [v80]; norm_num⟩
· exact ⟨81, by norm_num, by norm_num, by rw [v81]; norm_num⟩
· exact ⟨83, by norm_num, by norm_num, by rw [v83]; norm_num⟩
· rw [v82] at hlt; norm_num at hlt
· exact ⟨84, by norm_num, by norm_num, by rw [v84]; norm_num⟩
· exact ⟨85, by norm_num, by norm_num, by rw [v85]; norm_num⟩
· exact ⟨88, by norm_num, by norm_num, by rw [v88]; norm_num⟩
· rw [v86] at hlt; norm_num at hlt
· rw [v87] at hlt; norm_num at hlt
· exact ⟨90, by norm_num, by norm_num, by rw [v90]; norm_num⟩
· rw [v89] at hlt; norm_num at hlt
· exact ⟨92, by norm_num, by norm_num, by rw [v92]; norm_num⟩
· rw [v91] at hlt; norm_num at hlt
· exact ⟨94, by norm_num, by norm_num, by rw [v94]; norm_num⟩
· rw [v93] at hlt; norm_num at hlt
· exact ⟨95, by norm_num, by norm_num, by rw [v95]; norm_num⟩
· exact ⟨97, by norm_num, by norm_num, by rw [v97]; norm_num⟩
· rw [v96] at hlt; norm_num at hlt
· exact ⟨101, by norm_num, by norm_num, by rw [v101]; norm_num⟩
· rw [v98] at hlt; norm_num at hlt
· rw [v99] at hlt; norm_num at hlt
· rw [v100] at hlt; norm_num at hlt
theorem spec_a70fcca4__h4__h1__h2 : ∀ (r : ℕ → ℝ),
r (0 : ℕ) = (1 / 2 : ℝ) →
(∀ (m : ℕ),
r (m + (1 : ℕ)) =
if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) →
∀ (m : ℕ),
(1 : ℕ) ≤ m →
r m < (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) →
∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) := by
-- approach: the window statement is decided exactly for every skipped m ≤ 100 by computing the greedy walk of 1/2 to step 101 in the kernel (one `norm_num` per step); what remains is the same statement for m > 100
-- licence: CC-BY-4.0
intro r h0 hrs
-- label: after a skipped m > 100, another skip within (m, 3m+2]
-- claim: $m > 100 \wedge r_m < \frac{1}{2^m-1} \Rightarrow \exists n,\ m < n \le 3m+2 \wedge r_n < \frac{1}{2^n-1}$
-- The node's own statement restricted to m > 100: the tail of the ladder W(3m+2), where no mechanism is known.
-- The range 1 ≤ m ≤ 100 is closed below by exact computation of the walk (steps 1 to 101).
have htail : ∀ m : ℕ, 100 < m → r m < (1 : ℝ) / ((2 : ℝ) ^ m - 1) →
∃ n : ℕ, m < n ∧ n ≤ 3 * m + 2 ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - 1) := by
sorry
intro m hm hlt
by_cases hN : m ≤ 100
· by_cases h25 : m ≤ 25
· exact range_1_25 r h0 hrs m (by omega) h25 hlt
by_cases h50 : m ≤ 50
· exact range_26_50 r h0 hrs m (by omega) h50 hlt
by_cases h75 : m ≤ 75
· exact range_51_75 r h0 hrs m (by omega) h75 hlt
exact range_76_100 r h0 hrs m (by omega) hN hlt
· exact htail m (by omega) hltThe gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-257/nodes/spec-a70fcca4--h4--h1--h2/attempts/20261026T203640Z-t1026-a-partial.lean
Closing it through its holes
Closable through its holes: once they are proved, a proof of this statement may name their theorems, which its Context already carries. A direct proof is accepted at any time.
What is known
Work on it
How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →
Record
Statement: the Lean file and its words (1 version)
Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.
import Mathlib
import Nodes.«spec-a70fcca4--h4--h1--h2».Context
/-! Hole `hrun` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/
theorem spec_a70fcca4__h4__h1__h2 : ∀ (r : ℕ → ℝ),
r (0 : ℕ) = (1 / 2 : ℝ) →
(∀ (m : ℕ),
r (m + (1 : ℕ)) =
if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) →
∀ (m : ℕ),
(1 : ℕ) ≤ m →
r m < (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) →
∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) := by
sorryA statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
In words, unverified — what this statement says; written by t1022-j, drafted with Claude Opus 5.5 (claude-opus-5-5), 2026-10-22; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle m \ge 1 \ \wedge\ r_m < \frac{1}{2^m-1} \ \Longrightarrow\ \exists n,\ m < n \le 3m+2 \ \wedge\ r_n < \frac{1}{2^n-1}$
Here r is the greedy remainder of 1/2: r_0 = 1/2, r_(m+1) = r_m - 1/(2^m-1) if that term fits under r_m, else r_m. In words: the set the walk chooses never contains the whole block m+1, ..., 3m+2 right after an element m >= 1 it skipped. This is weaker than the hole of graph PR #865 (window (m, 2m], m >= 2) and essentially equivalent to this node: conversely, the node's bound at a skipped m forces a skip within (m, 3m+3], since the terms over (m, 3m+3] sum to more than 2^-m + 4^-m/3 (both inequalities checked exactly for m <= 120, margins 3/28 and 1/56 times 8^-m).
Rendered from gloss/87e90bd0c316….md · Improve these words →
Rendered from targets/erdos-257/nodes/spec-a70fcca4--h4--h1--h2/Statement.lean. Origin: compiler-derived.
Depends on (1), each in words
Depends on, each in words where someone has written them:
- spec-a70fcca4--h4--h1--h2--h1
spec_a70fcca4__h4__h1__h2__h1: $m > 100 \wedge r_m < \frac{1}{2^m-1} \Rightarrow \exists n,\ m < n \le 3m+2 \wedge r_n < \frac{1}{2^n-1}$
Attestation: none of a proof
No proof of this statement has been merged. A partial assembly merged under attestations/000987.json: it records an attempt, not a proof (see Attempts below).
Witness
Not checked — no run on this page records step 7 passing for it.
bd0aa0e5869f.import Mathlib
theorem witness : ∃ (r : ℕ → ℝ) (m : ℕ), r 0 = 1 / 2 ∧
(∀ m, r (m + 1) = if (1 : ℝ) / (2 ^ m - 1) ≤ r m then r m - 1 / (2 ^ m - 1) else r m) ∧
1 ≤ m ∧ r m < 1 / (2 ^ m - 1) :=
⟨fun m => Nat.rec (1 / 2 : ℝ)
(fun k rk => if (1 : ℝ) / (2 ^ k - 1) ≤ rk then rk - 1 / (2 ^ k - 1) else rk) m,
1, rfl, fun _ => rfl, le_refl 1, by
show (if (1 : ℝ) / (2 ^ 0 - 1) ≤ (1 / 2 : ℝ) then (1 / 2 : ℝ) - 1 / (2 ^ 0 - 1) else 1 / 2)
< 1 / (2 ^ 1 - 1)
norm_num⟩In words, unverified — what this witness says; written by t1026-a, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-26; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \exists\, r:\mathbb{N}\to\mathbb{R},\ \exists\, m:\mathbb{N}:\quad r_0=\tfrac12\ \wedge\ \forall m:\ r_{m+1}=\begin{cases} r_m-\dfrac{1}{2^m-1} & \text{if } \dfrac{1}{2^m-1}\le r_m,\\[4pt] r_m & \text{otherwise}\end{cases}\ \wedge\ 1\le m\ \wedge\ r_m<\frac{1}{2^m-1}$
The witness is the greedy remainder of $\tfrac12$ itself, defined by recursion on $m$ (Nat.rec): $r_0 = \tfrac12$ and the step rule as written, so both equations hold by definition (rfl). Lean convention: at $m = 0$ the term is $\frac{1}{2^0-1} = \frac10 = 0$, so step $0$ is taken and subtracts nothing; $r_1 = \tfrac12$. The skipped step exhibited is $m = 1$: $r_1 = \tfrac12 < \frac{1}{2^1-1} = 1$ (norm_num).
Rendered from gloss/55c12fcd3e16….md · Improve these words →
Attempts (2)
2 recorded. Routes refuted: none. Failure classes: route-dead-ends 1.
Untrusted contributor text — a partial assembly: it records an attempt, not a proof; its attestation names the file, and no hash in the record binds these bytes.
Untrusted: partial assembly (D-12 #5), by t1026-a; merged in 0c1da39dcfcf under attestations/000987.json, whose step 2 took this file as a partial. A partial records an attempt, not a proof: the gate replayed it with its holes left as sorry. Rendered from targets/erdos-257/nodes/spec-a70fcca4--h4--h1--h2/attempts/20261026T203640Z-t1026-a-partial.lean.
Untrusted contributor text — an outline the gate extracted from this partial assembly; its holes are sorry steps, and it records an attempt, not a proof.
Outline of 20261026T203640Z-t1026-a-partial.lean, extracted by the gate at be99b4fba02b from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.
htailhole∀ (m : ℕ), (100 : ℕ) < m → r m < (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) → ∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))holeLeaves
∀ (m : ℕ), (1 : ℕ) ≤ m → r m < (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) → ∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), withhtail : ∀ (m : ℕ), (100 : ℕ) < m → r m < (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) → ∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)).Left open as a hole; its statement is spec-a70fcca4--h4--h1--h2--h1
spec_a70fcca4__h4__h1__h2__h1(open).Lean, lines 361–363
have htail : ∀ m : ℕ, 100 < m → r m < (1 : ℝ) / ((2 : ℝ) ^ m - 1) → ∃ n : ℕ, m < n ∧ n ≤ 3 * m + 2 ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - 1) := by sorrys2caseLeaves
∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), withhN : m ≤ (100 : ℕ).Lean, lines 366–372
· by_cases h25 : m ≤ 25 · exact range_1_25 r h0 hrs m (by omega) h25 hlt by_cases h50 : m ≤ 50 · exact range_26_50 r h0 hrs m (by omega) h50 hlt by_cases h75 : m ≤ 75 · exact range_51_75 r h0 hrs m (by omega) h75 hlt exact range_76_100 r h0 hrs m (by omega) hN hlts2.s1caseLeaves
∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), withh25 : m ≤ (25 : ℕ).Lean, line 367
· exact range_1_25 r h0 hrs m (by omega) h25 hlt
s2.s2caseLeaves
∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), withh50 : m ≤ (50 : ℕ).Lean, line 369
· exact range_26_50 r h0 hrs m (by omega) h50 hlt
s2.s3caseLeaves
∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), withh75 : m ≤ (75 : ℕ).Lean, line 371
· exact range_51_75 r h0 hrs m (by omega) h75 hlt
s3caseLeaves
∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), withhN : ¬m ≤ (100 : ℕ).Lean, line 373
· exact htail m (by omega) hlt
import Mathlib
import Nodes.«spec-a70fcca4--h4--h1--h2».Context
/-! Hole `hrun` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/
private theorem walk_values (r : ℕ → ℝ) (h0 : r 0 = 1 / 2)
(hrs : ∀ m : ℕ, r (m + 1) = if (1 : ℝ) / ((2 : ℝ) ^ m - 1) ≤ r m then r m - 1 / ((2 : ℝ) ^ m - 1) else r m) :
r 1 = 1 / 2 ∧
r 2 = 1 / 2 ∧
r 3 = 1 / 6 ∧
r 4 = 1 / 42 ∧
r 5 = 1 / 42 ∧
r 6 = 1 / 42 ∧
r 7 = 1 / 126 ∧
r 8 = 1 / 16002 ∧
r 9 = 1 / 16002 ∧
r 10 = 1 / 16002 ∧
r 11 = 1 / 16002 ∧
r 12 = 1 / 16002 ∧
r 13 = 1 / 16002 ∧
r 14 = 1 / 16002 ∧
r 15 = 1 / 688086 ∧
r 16 = 1 / 688086 ∧
r 17 = 1 / 688086 ∧
r 18 = 1 / 688086 ∧
r 19 = 1 / 688086 ∧
r 20 = 1 / 688086 ∧
r 21 = 120163 / 240503259150 ∧
r 22 = 12932167 / 567347188334850 ∧
r 23 = 12932167 / 567347188334850 ∧
r 24 = 12932167 / 567347188334850 ∧
r 25 = 12932167 / 567347188334850 ∧
r 26 = 12932167 / 567347188334850 ∧
r 27 = 100171945053757 / 12691341578466215591850 ∧
r 28 = 107644170831134536927 / 243343288463189657575723817850 ∧
r 29 = 107644170831134536927 / 243343288463189657575723817850 ∧
r 30 = 107644170831134536927 / 243343288463189657575723817850 ∧
r 31 = 107644170831134536927 / 243343288463189657575723817850 ∧
r 32 = 107644170831134536927 / 243343288463189657575723817850 ∧
r 33 = 14598993650261743084714065641 / 69676764360476692711332185574552481050 ∧
r 34 = 7961090884242287202286887174188286683 / 85502692624144962281478559794068509473752428650 ∧
r 35 = 17089269107037109310175073431588929983696187113 / 489641691359023146408090293693780137366287632111847097650 ∧
r 36 = 24775495057665137934850160116999839971296655500713733 / 4273294490391516376753649556370453526829302383904245353406731150 ∧
r 37 = 24775495057665137934850160116999839971296655500713733 / 4273294490391516376753649556370453526829302383904245353406731150 ∧
r 38 = 24775495057665137934850160116999839971296655500713733 / 4273294490391516376753649556370453526829302383904245353406731150 ∧
r 39 = 845647244845372609119117317639626159048890492622691072083139023 / 391544748423291282081983403730543585794163711509479738425458531026506458150 ∧
r 40 = 1279361336100174444251942992473714966534258700082741704514992885791523 / 3754190171139528729585651254462415212675896584673329663463798639720328923217380650 ∧
r 41 = 1279361336100174444251942992473714966534258700082741704514992885791523 / 3754190171139528729585651254462415212675896584673329663463798639720328923217380650 ∧
r 42 = 1279361336100174444251942992473714966534258700082741704514992885791523 / 3754190171139528729585651254462415212675896584673329663463798639720328923217380650 ∧
r 43 = 2307178909358625844288230048113688514917493874182843861668184598259080687 / 20343956537405106185624644147931828037490683592344773446310324828644462434914985742350 ∧
r 44 = 2307178909358625844288230048113688514917493874182843861668184598259080687 / 20343956537405106185624644147931828037490683592344773446310324828644462434914985742350 ∧
r 45 = 659318159054952992368158389296038659826449069734600364727101743112098359598562611 / 11655908428123218204725844561756938739161153600678265505596657245523679800986195160837595468050 ∧
r 46 = 728602171895038678636394825276913166726248096645486542004397068685941640433698111948589851 / 25888884487622534734603867774700751495820189468709549988355020113039400587330235326362886993608342757550 ∧
r 47 = 8460645117916361525949041843570964695646901621569788945241573199933079840413055250334293685177039980221 / 607256096518192733364976633800564606357882531919006885021700723676812860062069999895812681580588233238576338844868550 ∧
r 48 = 583473847243115429710805323201397105794687109693978440309296238195743045193725738895896654861024781126198971055118717 / 85463697812430478601160467988164408038970436424688174871843944772162618813142138992772085377175290216341013777227236169933007265850 ∧
r 49 = 57235566419689740527216894644994090719061380449165398277406761889413767481516239955879524226149880396024414727845120310098331 / 17479494673046627672470862948133885139494627045732135374353110002317959629414713279514555065754621917880396537985539383414639696059681412050 ∧
r 50 = 116072950999685541383889664443572968628785973521095383728800241565844348269673906801493179079294274435122845507376543935730052352256689133 / 77480950488343722797022987731006171783678220639000435235009231243407940099381827934169581918016008090643185870271101231402724248618403158229303693245650 ∧
r 51 = 52009358972776708178754179196384591028396521395320498229273554009840029694048630162582390457279735168652989630775356150931336575678539518770484821183 / 85274481854256190162461282209750638404229496029888703103179320728362117630070146079717615316644475894677228969932350223380505975143341603386178767416794463169725650 ∧
r 52 = 34703310191239350769791367194664875178207907367958832542389658785757420961031869707529629835487322095292587580834041950889210513131813649056401396910662146983 / 209287945738809026219275100016580785098653830240066914142002489661478086867667048653939453375339890321169299805069374587184442865964663479716191899209781729053151957374213150 ∧
r 53 = 34703310191239350769791367194664875178207907367958832542389658785757420961031869707529629835487322095292587580834041950889210513131813649056401396910662146983 / 209287945738809026219275100016580785098653830240066914142002489661478086867667048653939453375339890321169299805069374587184442865964663479716191899209781729053151957374213150 ∧
r 54 = 103291683952767491891750666081103226355445470584688441325011751615328556690820348361282592828209747923435398251461622534779356283796512611067700294596444193396392448262867003 / 1885098228884873624011666960437368710807715308673609950293344297722004703388546146422304622652660491593324418280896776831792432687454926388554749762781569931017735810002476605563665676231650 ∧
r 55 = 103291683952767491891750666081103226355445470584688441325011751615328556690820348361282592828209747923435398251461622534779356283796512611067700294596444193396392448262867003 / 1885098228884873624011666960437368710807715308673609950293344297722004703388546146422304622652660491593324418280896776831792432687454926388554749762781569931017735810002476605563665676231650 ∧
r 56 = 28938917471616433418063823334248580477925844332221809806946710850025199523666410189545280477180319867467850932655442170871209577637393520505272503891542587694137356662057229169799115843 / 1070296759211774725790722296265701945389278514404776283394742030382279204391468452707922952872717892265133839389903409221994041786988893799546129514616776566503136411715372889274746954488854107634141150 ∧
r 57 = 728855957470306119334593881931744942956142754004476924984700530768600816655305995140906089684413857284101903609145096158189222185393049431628902589347323399187883947612398562037347430239561427101 / 55382379421561065182045979674407837221285399325700332325063054260807863800561242927602172086732743266112478175431395232227810531545303976647967939928233628940877491234355065569144896930081128892169042044460584550 ∧
r 58 = 13530439290334195123461135883479018102160530020573828556310705205007657426531168222845267832154258915552077758695870547161451592553201757208235114669067033546506286268525644984209563061752893538537245727269 / 2174774510478498224736179492882261487661050920345209052654298823288346005246886234411414465360628354503363235912647440635882326083647002338444270460678806075426147442420032739736200222486882628185299642261392074115165321450 ∧
r 59 = 575036365224142176549557972960792401892643933350466454371918100412412971297422931568155615545322194948506149669732040287690842251996221220639368584504554591045666926100230376653342614117168461627403099246222822910705766139 / 208945358400124104949235415244691686114962683800358894460826058310106658811443985405572795329331717950013243329535403617448660300734306322775707283805867223434719156807351560923670145333707376980063290573359754503462073691363759616778262450 ∧
r 60 = 122540537298811081787554294908318876860372406152460299283777662198098217662773335223345710071119759659686279915472401339021892987080447397300047204812597448933144587150850904333062193701401976701479325018660830279102201614410150104123644243 / 120448798493643987670593566453438201063416656796404566564359731723408761251570315791261128143224656578079675899796472567165097293912530926952910833137360264577005092035542403362619104429371181816825044452427808354064179620507384745919782717533006498380163150 ∧
r 61 = 481911530313702823199688566801587999878141309126864033454464576361934382525679879400612226733440039413542369946350682895603880716260765622402501592726925153711825200963655376896979987420389115951869457334063798859287989978009289894830407929161239 / 3212647812998803962430237159045270718043979792653966281224804280403324460226632701152727892046940583118736898378576353014395863368493431680806320096708778695840163263355610036175222527881665695855902618223979209467997912798034943739828425694465502089816707767539650 ∧
r 62 = 481911530313702823199688566801587999878141309126864033454464576361934382525679879400612226733440039413542369946350682895603880716260765622402501592726925153711825200963655376896979987420389115951869457334063798859287989978009289894830407929161239 / 3212647812998803962430237159045270718043979792653966281224804280403324460226632701152727892046940583118736898378576353014395863368493431680806320096708778695840163263355610036175222527881665695855902618223979209467997912798034943739828425694465502089816707767539650 ∧
r 63 = 481911530313702823199688566801587999878141309126864033454464576361934382525679879400612226733440039413542369946350682895603880716260765622402501592726925153711825200963655376896979987420389115951869457334063798859287989978009289894830407929161239 / 3212647812998803962430237159045270718043979792653966281224804280403324460226632701152727892046940583118736898378576353014395863368493431680806320096708778695840163263355610036175222527881665695855902618223979209467997912798034943739828425694465502089816707767539650 ∧
r 64 = 8048763716019973698502388369119050162801369194007823389218812806080971929153589774583918578332999720638682917277694095491865889315713519158242374179229177270147051859294286358957245234130770334542150581649154454782167749492850889449860772858057703657648401 / 193553167709305267953039471956075321100700279238345312815503511435274760560763667152195609660494142061645655404022610538081841829773431029405700662478077997116082761037326028592789847426537440986931396746554714620619606818651759356704187703089196440734480775469225194021436850 ∧
r 65 = 8048763716019973698502388369119050162801369194007823389218812806080971929153589774583918578332999720638682917277694095491865889315713519158242374179229177270147051859294286358957245234130770334542150581649154454782167749492850889449860772858057703657648401 / 193553167709305267953039471956075321100700279238345312815503511435274760560763667152195609660494142061645655404022610538081841829773431029405700662478077997116082761037326028592789847426537440986931396746554714620619606818651759356704187703089196440734480775469225194021436850 ∧
r 66 = 407188854206838223647708076247283161846499777423034694492943360482135632116747857491287309186023039085039011547273157697294772044296151791058934478070156810174326798350402000053472771812951986905227286176145679892235130039050138032888616893913757526970900952284918205661 / 28122335288450643321298259765041266230974318006908246854900456191763861850619549099411034907572721724737166437423306356558371344379707144474817848022592079392437421413207179507314556794737474020122496148137670787743514852948411824098475027348717241770421924037313766742452154446717691790350 ∧
r 67 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 ∧
r 68 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 ∧
r 69 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 ∧
r 70 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 ∧
r 71 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 ∧
r 72 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 ∧
r 73 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 ∧
r 74 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 ∧
r 75 = 159964742255280287252007403680852356718468955486655582796138215043268508523404698399092363050236460750020965043497268463261460813104623030344176518783847346908302141162051473749502547418078740588025473883244848090485920191077491746663073295302807911847290317196943416398797297243804402225308642529514099 / 5991615048287496872973786254379493828285679024998760976850704496994359646577100787089412393551004381083960434983220620346300807882132714002552937788602375656459552354649787559992629326866999071212873512973392403929715070563144240802326570360892832376505271838369324405361909504615297187691606917709989831007596911499462418150 ∧
r 76 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 ∧
r 77 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 ∧
r 78 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 ∧
r 79 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 ∧
r 80 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 ∧
r 81 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 ∧
r 82 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 ∧
r 83 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 ∧
r 84 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 ∧
r 85 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 ∧
r 86 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 ∧
r 87 = 2282074496642673776260768825238797350444591093432047699080242255305205892697221899727430224539768138483840882757379412130118108590650658064506054831375799629136183685930304075867961412852921974736582118770738057838549640338377085026802986387405501468831461075878050587213266253369778685819799541124657252873155959941008808846879901517869328869456285957624995229 / 265317241810557507380526149530850180254452898359821411986845851562677563831912203833914503581009138564266606920502256299450743021984270794162590933028315745966580987541693744354898707749543166513580742193509746730032205826657540706189083618947955651725032930464089061027562381711879362817617142758055067187490721762435122970327338796192603808167802793568121892214293687744322005236076150 ∧
r 88 = 23367331058921374616615207499262436035856746986047844280626339436870958291313779858280158825389623139014543875063122503853605095459172944543557922575453129251484013390961492319118333117986934520495895766587427989931367752620373401851764206656520615546375164359705563335484058837479235396890766007707872995694606945243518850940965289959275023803608491983782060389338553366599829 / 10924641221290394633676715177212711022334407879583031671968036680192101044070310606814717946527149436351707378686347555961869667410954701112777255058988460110773547723742724745629101249248549122926701508987033300471557533755647394952987986734020789236912876791862293318417134338752081063425186941945958230463654220910562360481283638476530381724103183465784872007702460747679783474225968644022518231618650 ∧
r 89 = 23367331058921374616615207499262436035856746986047844280626339436870958291313779858280158825389623139014543875063122503853605095459172944543557922575453129251484013390961492319118333117986934520495895766587427989931367752620373401851764206656520615546375164359705563335484058837479235396890766007707872995694606945243518850940965289959275023803608491983782060389338553366599829 / 10924641221290394633676715177212711022334407879583031671968036680192101044070310606814717946527149436351707378686347555961869667410954701112777255058988460110773547723742724745629101249248549122926701508987033300471557533755647394952987986734020789236912876791862293318417134338752081063425186941945958230463654220910562360481283638476530381724103183465784872007702460747679783474225968644022518231618650 ∧
r 90 = 3539036143247411942363317528160010236417878256559156557439946970859330270341139842034767600089174976756089489486873630374377741568860487924221017915515239226168163422567198170803806467131679016480182589590561479236094757769405184121295462056292942454224626240562626129537660001345182309413768264477884827351875112598111465376573853220171893799327698686816244141491348270598935682423159625338830785860369 / 6762025391331457939022650246359620955027430161278254949252380113744059778741616694439991289265407750129663538246610756564895329700142309618314734053731499737525673306378809301500714844366979576943751732134939213905622267379049847571441327374700154660524987518509706510342956483163140948966609646122655416369705305850263916330487471383579465953294031045973341623805221219194412667768502808686207913733319219244908727997517240970150 ∧
r 91 = 3539036143247411942363317528160010236417878256559156557439946970859330270341139842034767600089174976756089489486873630374377741568860487924221017915515239226168163422567198170803806467131679016480182589590561479236094757769405184121295462056292942454224626240562626129537660001345182309413768264477884827351875112598111465376573853220171893799327698686816244141491348270598935682423159625338830785860369 / 6762025391331457939022650246359620955027430161278254949252380113744059778741616694439991289265407750129663538246610756564895329700142309618314734053731499737525673306378809301500714844366979576943751732134939213905622267379049847571441327374700154660524987518509706510342956483163140948966609646122655416369705305850263916330487471383579465953294031045973341623805221219194412667768502808686207913733319219244908727997517240970150 ∧
r 92 = 1922797628928914421157211581250125666244367330545267684475844413272673032955536964797159579258485037740904420183280641420369636194569664263201931890792616436052065579772022975455932586311030203214564139485925604184330521617836531667769741236123389649790179236551407939259327559599285354366417122231020441547483478920007619216396378213134514079432509869564823812436258407770279069827839642858847030312365324818253992421000649 / 16094065175420312418976442914756120349395968539071838616061710926185427022760216874223822139247851367032545214029105992881776408910481938691597572180788857134642428800952435493681759530831486356432449149474485664195498245469778538982696896819808589647245843797423112414808704142631619009891595581387901743793037087126730343033959855448712939628479441427038758847089364734264650581323362592719606114734516547220985984427484054751638579260270936963170650 ∧
r 93 = 1922797628928914421157211581250125666244367330545267684475844413272673032955536964797159579258485037740904420183280641420369636194569664263201931890792616436052065579772022975455932586311030203214564139485925604184330521617836531667769741236123389649790179236551407939259327559599285354366417122231020441547483478920007619216396378213134514079432509869564823812436258407770279069827839642858847030312365324818253992421000649 / 16094065175420312418976442914756120349395968539071838616061710926185427022760216874223822139247851367032545214029105992881776408910481938691597572180788857134642428800952435493681759530831486356432449149474485664195498245469778538982696896819808589647245843797423112414808704142631619009891595581387901743793037087126730343033959855448712939628479441427038758847089364734264650581323362592719606114734516547220985984427484054751638579260270936963170650 ∧
r 94 = 421200028990351211773809617704358922232415859245126380838392897277152007549468876931735597216254130091947449673178431182242150304686934121878907617992778857740031039018795156230610394398106485709729510932310800119608672587637111828199133470925040115710902775360528392706820740420787097896335090198662810782741171033311656358975754686785155156891071370866234035701061764361908089577479531972349540475819773226492470317497299485147969744475771042971387 / 22769700200595762447252288874412593725714991138088344743316097712058365740967734456112561014662512467039386157196278487662525599644949768439108311893225253688001117962311959784992353509304780743163850890965897048053930436417283752757575669914781036279750856527698070883654581753619767223427706174560218009664532416566425408819434730731053356895154565357301382503564552964003245343140244800591166150664221084448146370389083787874983476753865658857743882047246280942843383017633450 ∧
r 95 = 421200028990351211773809617704358922232415859245126380838392897277152007549468876931735597216254130091947449673178431182242150304686934121878907617992778857740031039018795156230610394398106485709729510932310800119608672587637111828199133470925040115710902775360528392706820740420787097896335090198662810782741171033311656358975754686785155156891071370866234035701061764361908089577479531972349540475819773226492470317497299485147969744475771042971387 / 22769700200595762447252288874412593725714991138088344743316097712058365740967734456112561014662512467039386157196278487662525599644949768439108311893225253688001117962311959784992353509304780743163850890965897048053930436417283752757575669914781036279750856527698070883654581753619767223427706174560218009664532416566425408819434730731053356895154565357301382503564552964003245343140244800591166150664221084448146370389083787874983476753865658857743882047246280942843383017633450 ∧
r 96 = 421200028990351211773809617704358922232415859245126380838392897277152007549468876931735597216254130091947449673178431182242150304686934121878907617992778857740031039018795156230610394398106485709729510932310800119608672587637111828199133470925040115710902775360528392706820740420787097896335090198662810782741171033311656358975754686785155156891071370866234035701061764361908089577479531972349540475819773226492470317497299485147969744475771042971387 / 22769700200595762447252288874412593725714991138088344743316097712058365740967734456112561014662512467039386157196278487662525599644949768439108311893225253688001117962311959784992353509304780743163850890965897048053930436417283752757575669914781036279750856527698070883654581753619767223427706174560218009664532416566425408819434730731053356895154565357301382503564552964003245343140244800591166150664221084448146370389083787874983476753865658857743882047246280942843383017633450 ∧
r 97 = 574683659394598440680245744935850408685320969178434055381507638912219027706457263497539495397985872063212051487654576573907024523037206353160129808073130288697853902815923856146182036139967811666691660954581277476389266212011915354440034074019071179564277357117516773760005707863747846985704496970625947286805232071970785213419754548992839986325860468381991906516105146277173556771139227849493495439903572908331020354143726017391984099768061770423737824163237 / 97793625488980793383841525097995356633150866423075026011643401043167545955664392559738215516093971615371914062901319299308197971622675735225668510019950386034267746106302367711924840458647632699533311903150850222631527454340090520555200350807747792647306842342068789914510889289340006372309735705309253730252115295152726061813735156041361879913960835120263301922293987302275308033968086664030093341531354455289673559369834215720816982156080181785549447491694337222118786069631398457505450 ∧
r 98 = 574683659394598440680245744935850408685320969178434055381507638912219027706457263497539495397985872063212051487654576573907024523037206353160129808073130288697853902815923856146182036139967811666691660954581277476389266212011915354440034074019071179564277357117516773760005707863747846985704496970625947286805232071970785213419754548992839986325860468381991906516105146277173556771139227849493495439903572908331020354143726017391984099768061770423737824163237 / 97793625488980793383841525097995356633150866423075026011643401043167545955664392559738215516093971615371914062901319299308197971622675735225668510019950386034267746106302367711924840458647632699533311903150850222631527454340090520555200350807747792647306842342068789914510889289340006372309735705309253730252115295152726061813735156041361879913960835120263301922293987302275308033968086664030093341531354455289673559369834215720816982156080181785549447491694337222118786069631398457505450 ∧
r 99 = 1161253982954115450632071110849528470792494251823669704195891048507909683961669550088715655436330185205983763927901688679489127521003965331376582880032423003281765596557449339474675004089201894144832757183875252874355250984054809052914829031112638493532250971491336405217204084079023968083739549128007221249451900079648014920892729225328437696698036636361730691160479552926955312903539482434838075758639303980691247610301230929503368330302600664849470782584066272028869839 / 426766797782349344100583430358846750964823536309783372046770841116704164267958590422457444493100456265031415212538945525323151306892367836417014838329016866995025124428017812577530045918933128526494194832182867616997302919275351402578931231623862459740463397183417231572130288594375862693574979236303859822646981398531145082686804466115213458533412355713050825517858157571983938938499020501789645999094570966141564893442241222299292590343811955066132768784809995353690988188981260498694410488921268650 ∧
r 100 = 493194876819595682416230825422962914766142554534757606805596000406205047287947302235621696937995691438111870808133487161585734431117036904531160037728958452112516155227623049266632659898265889611070794228324109273048769645189389196373819538040191672739776835073585190189130130250621286217345831542364037295204530177468125642161555537278312899418846717150463420137601137323867684024867443402772128918887917464532087156288032289765368512689837500943156797171821259067456275051384307218945201 / 431367556096659183461813462034098034301924646541448507656611797171215848597996775821001858054438934523961038087543256221766158297120930142251581973321903116546795768085833633375811957742227290711439329146698525913668229877785142086467084198608809858488200226275994330891980275563548884837623422868106630147398229952130785101061543553632324695844746010940320668028940180071385716206994081607649537082973298037867775819070749780467398781681185348645683658246956216740413728849861746611819717559009474875848841639720437850 ∧
r 101 = 167957767397664854045821899531172964829817499952431862669492433107247389252964034728062742778414655188479990722394436597415176502956620950223269873488898280121755560007365838515644187621752596426016075217895015258986489758362689583198372176424813015717638476275834951517147544720139124367157212985565141915856127464101183795558840083531566005572177496731179002611623496742650796159901063943304826312020030262330202382855279370234130468836156740490622182129566192916650902624234683151192394888233431307 / 473830918267472574175258513129986452743223015915862785528202489246551712618137127912249851741941297469648287545053699189791774687390521417468435642174794621396598061921250411544186059725798272912379009411412190496365336129355487964993794460406898705655108628177502890608412889247520649913971137714050675097727592659143286788688385544420998507797576313314888896792418201873055580877901172822953493363228138191107988774906502228997322398171417565290596353686393484628769683750302387214983797782848689486817493892324153198305635164250 := by
have v1 : r 1 = 1 / 2 := by rw [hrs 0, h0]; norm_num
have v2 : r 2 = 1 / 2 := by rw [hrs 1, v1]; norm_num
have v3 : r 3 = 1 / 6 := by rw [hrs 2, v2]; norm_num
have v4 : r 4 = 1 / 42 := by rw [hrs 3, v3]; norm_num
have v5 : r 5 = 1 / 42 := by rw [hrs 4, v4]; norm_num
have v6 : r 6 = 1 / 42 := by rw [hrs 5, v5]; norm_num
have v7 : r 7 = 1 / 126 := by rw [hrs 6, v6]; norm_num
have v8 : r 8 = 1 / 16002 := by rw [hrs 7, v7]; norm_num
have v9 : r 9 = 1 / 16002 := by rw [hrs 8, v8]; norm_num
have v10 : r 10 = 1 / 16002 := by rw [hrs 9, v9]; norm_num
have v11 : r 11 = 1 / 16002 := by rw [hrs 10, v10]; norm_num
have v12 : r 12 = 1 / 16002 := by rw [hrs 11, v11]; norm_num
have v13 : r 13 = 1 / 16002 := by rw [hrs 12, v12]; norm_num
have v14 : r 14 = 1 / 16002 := by rw [hrs 13, v13]; norm_num
have v15 : r 15 = 1 / 688086 := by rw [hrs 14, v14]; norm_num
have v16 : r 16 = 1 / 688086 := by rw [hrs 15, v15]; norm_num
have v17 : r 17 = 1 / 688086 := by rw [hrs 16, v16]; norm_num
have v18 : r 18 = 1 / 688086 := by rw [hrs 17, v17]; norm_num
have v19 : r 19 = 1 / 688086 := by rw [hrs 18, v18]; norm_num
have v20 : r 20 = 1 / 688086 := by rw [hrs 19, v19]; norm_num
have v21 : r 21 = 120163 / 240503259150 := by rw [hrs 20, v20]; norm_num
have v22 : r 22 = 12932167 / 567347188334850 := by rw [hrs 21, v21]; norm_num
have v23 : r 23 = 12932167 / 567347188334850 := by rw [hrs 22, v22]; norm_num
have v24 : r 24 = 12932167 / 567347188334850 := by rw [hrs 23, v23]; norm_num
have v25 : r 25 = 12932167 / 567347188334850 := by rw [hrs 24, v24]; norm_num
have v26 : r 26 = 12932167 / 567347188334850 := by rw [hrs 25, v25]; norm_num
have v27 : r 27 = 100171945053757 / 12691341578466215591850 := by rw [hrs 26, v26]; norm_num
have v28 : r 28 = 107644170831134536927 / 243343288463189657575723817850 := by rw [hrs 27, v27]; norm_num
have v29 : r 29 = 107644170831134536927 / 243343288463189657575723817850 := by rw [hrs 28, v28]; norm_num
have v30 : r 30 = 107644170831134536927 / 243343288463189657575723817850 := by rw [hrs 29, v29]; norm_num
have v31 : r 31 = 107644170831134536927 / 243343288463189657575723817850 := by rw [hrs 30, v30]; norm_num
have v32 : r 32 = 107644170831134536927 / 243343288463189657575723817850 := by rw [hrs 31, v31]; norm_num
have v33 : r 33 = 14598993650261743084714065641 / 69676764360476692711332185574552481050 := by rw [hrs 32, v32]; norm_num
have v34 : r 34 = 7961090884242287202286887174188286683 / 85502692624144962281478559794068509473752428650 := by rw [hrs 33, v33]; norm_num
have v35 : r 35 = 17089269107037109310175073431588929983696187113 / 489641691359023146408090293693780137366287632111847097650 := by rw [hrs 34, v34]; norm_num
have v36 : r 36 = 24775495057665137934850160116999839971296655500713733 / 4273294490391516376753649556370453526829302383904245353406731150 := by rw [hrs 35, v35]; norm_num
have v37 : r 37 = 24775495057665137934850160116999839971296655500713733 / 4273294490391516376753649556370453526829302383904245353406731150 := by rw [hrs 36, v36]; norm_num
have v38 : r 38 = 24775495057665137934850160116999839971296655500713733 / 4273294490391516376753649556370453526829302383904245353406731150 := by rw [hrs 37, v37]; norm_num
have v39 : r 39 = 845647244845372609119117317639626159048890492622691072083139023 / 391544748423291282081983403730543585794163711509479738425458531026506458150 := by rw [hrs 38, v38]; norm_num
have v40 : r 40 = 1279361336100174444251942992473714966534258700082741704514992885791523 / 3754190171139528729585651254462415212675896584673329663463798639720328923217380650 := by rw [hrs 39, v39]; norm_num
have v41 : r 41 = 1279361336100174444251942992473714966534258700082741704514992885791523 / 3754190171139528729585651254462415212675896584673329663463798639720328923217380650 := by rw [hrs 40, v40]; norm_num
have v42 : r 42 = 1279361336100174444251942992473714966534258700082741704514992885791523 / 3754190171139528729585651254462415212675896584673329663463798639720328923217380650 := by rw [hrs 41, v41]; norm_num
have v43 : r 43 = 2307178909358625844288230048113688514917493874182843861668184598259080687 / 20343956537405106185624644147931828037490683592344773446310324828644462434914985742350 := by rw [hrs 42, v42]; norm_num
have v44 : r 44 = 2307178909358625844288230048113688514917493874182843861668184598259080687 / 20343956537405106185624644147931828037490683592344773446310324828644462434914985742350 := by rw [hrs 43, v43]; norm_num
have v45 : r 45 = 659318159054952992368158389296038659826449069734600364727101743112098359598562611 / 11655908428123218204725844561756938739161153600678265505596657245523679800986195160837595468050 := by rw [hrs 44, v44]; norm_num
have v46 : r 46 = 728602171895038678636394825276913166726248096645486542004397068685941640433698111948589851 / 25888884487622534734603867774700751495820189468709549988355020113039400587330235326362886993608342757550 := by rw [hrs 45, v45]; norm_num
have v47 : r 47 = 8460645117916361525949041843570964695646901621569788945241573199933079840413055250334293685177039980221 / 607256096518192733364976633800564606357882531919006885021700723676812860062069999895812681580588233238576338844868550 := by rw [hrs 46, v46]; norm_num
have v48 : r 48 = 583473847243115429710805323201397105794687109693978440309296238195743045193725738895896654861024781126198971055118717 / 85463697812430478601160467988164408038970436424688174871843944772162618813142138992772085377175290216341013777227236169933007265850 := by rw [hrs 47, v47]; norm_num
have v49 : r 49 = 57235566419689740527216894644994090719061380449165398277406761889413767481516239955879524226149880396024414727845120310098331 / 17479494673046627672470862948133885139494627045732135374353110002317959629414713279514555065754621917880396537985539383414639696059681412050 := by rw [hrs 48, v48]; norm_num
have v50 : r 50 = 116072950999685541383889664443572968628785973521095383728800241565844348269673906801493179079294274435122845507376543935730052352256689133 / 77480950488343722797022987731006171783678220639000435235009231243407940099381827934169581918016008090643185870271101231402724248618403158229303693245650 := by rw [hrs 49, v49]; norm_num
have v51 : r 51 = 52009358972776708178754179196384591028396521395320498229273554009840029694048630162582390457279735168652989630775356150931336575678539518770484821183 / 85274481854256190162461282209750638404229496029888703103179320728362117630070146079717615316644475894677228969932350223380505975143341603386178767416794463169725650 := by rw [hrs 50, v50]; norm_num
have v52 : r 52 = 34703310191239350769791367194664875178207907367958832542389658785757420961031869707529629835487322095292587580834041950889210513131813649056401396910662146983 / 209287945738809026219275100016580785098653830240066914142002489661478086867667048653939453375339890321169299805069374587184442865964663479716191899209781729053151957374213150 := by rw [hrs 51, v51]; norm_num
have v53 : r 53 = 34703310191239350769791367194664875178207907367958832542389658785757420961031869707529629835487322095292587580834041950889210513131813649056401396910662146983 / 209287945738809026219275100016580785098653830240066914142002489661478086867667048653939453375339890321169299805069374587184442865964663479716191899209781729053151957374213150 := by rw [hrs 52, v52]; norm_num
have v54 : r 54 = 103291683952767491891750666081103226355445470584688441325011751615328556690820348361282592828209747923435398251461622534779356283796512611067700294596444193396392448262867003 / 1885098228884873624011666960437368710807715308673609950293344297722004703388546146422304622652660491593324418280896776831792432687454926388554749762781569931017735810002476605563665676231650 := by rw [hrs 53, v53]; norm_num
have v55 : r 55 = 103291683952767491891750666081103226355445470584688441325011751615328556690820348361282592828209747923435398251461622534779356283796512611067700294596444193396392448262867003 / 1885098228884873624011666960437368710807715308673609950293344297722004703388546146422304622652660491593324418280896776831792432687454926388554749762781569931017735810002476605563665676231650 := by rw [hrs 54, v54]; norm_num
have v56 : r 56 = 28938917471616433418063823334248580477925844332221809806946710850025199523666410189545280477180319867467850932655442170871209577637393520505272503891542587694137356662057229169799115843 / 1070296759211774725790722296265701945389278514404776283394742030382279204391468452707922952872717892265133839389903409221994041786988893799546129514616776566503136411715372889274746954488854107634141150 := by rw [hrs 55, v55]; norm_num
have v57 : r 57 = 728855957470306119334593881931744942956142754004476924984700530768600816655305995140906089684413857284101903609145096158189222185393049431628902589347323399187883947612398562037347430239561427101 / 55382379421561065182045979674407837221285399325700332325063054260807863800561242927602172086732743266112478175431395232227810531545303976647967939928233628940877491234355065569144896930081128892169042044460584550 := by rw [hrs 56, v56]; norm_num
have v58 : r 58 = 13530439290334195123461135883479018102160530020573828556310705205007657426531168222845267832154258915552077758695870547161451592553201757208235114669067033546506286268525644984209563061752893538537245727269 / 2174774510478498224736179492882261487661050920345209052654298823288346005246886234411414465360628354503363235912647440635882326083647002338444270460678806075426147442420032739736200222486882628185299642261392074115165321450 := by rw [hrs 57, v57]; norm_num
have v59 : r 59 = 575036365224142176549557972960792401892643933350466454371918100412412971297422931568155615545322194948506149669732040287690842251996221220639368584504554591045666926100230376653342614117168461627403099246222822910705766139 / 208945358400124104949235415244691686114962683800358894460826058310106658811443985405572795329331717950013243329535403617448660300734306322775707283805867223434719156807351560923670145333707376980063290573359754503462073691363759616778262450 := by rw [hrs 58, v58]; norm_num
have v60 : r 60 = 122540537298811081787554294908318876860372406152460299283777662198098217662773335223345710071119759659686279915472401339021892987080447397300047204812597448933144587150850904333062193701401976701479325018660830279102201614410150104123644243 / 120448798493643987670593566453438201063416656796404566564359731723408761251570315791261128143224656578079675899796472567165097293912530926952910833137360264577005092035542403362619104429371181816825044452427808354064179620507384745919782717533006498380163150 := by rw [hrs 59, v59]; norm_num
have v61 : r 61 = 481911530313702823199688566801587999878141309126864033454464576361934382525679879400612226733440039413542369946350682895603880716260765622402501592726925153711825200963655376896979987420389115951869457334063798859287989978009289894830407929161239 / 3212647812998803962430237159045270718043979792653966281224804280403324460226632701152727892046940583118736898378576353014395863368493431680806320096708778695840163263355610036175222527881665695855902618223979209467997912798034943739828425694465502089816707767539650 := by rw [hrs 60, v60]; norm_num
have v62 : r 62 = 481911530313702823199688566801587999878141309126864033454464576361934382525679879400612226733440039413542369946350682895603880716260765622402501592726925153711825200963655376896979987420389115951869457334063798859287989978009289894830407929161239 / 3212647812998803962430237159045270718043979792653966281224804280403324460226632701152727892046940583118736898378576353014395863368493431680806320096708778695840163263355610036175222527881665695855902618223979209467997912798034943739828425694465502089816707767539650 := by rw [hrs 61, v61]; norm_num
have v63 : r 63 = 481911530313702823199688566801587999878141309126864033454464576361934382525679879400612226733440039413542369946350682895603880716260765622402501592726925153711825200963655376896979987420389115951869457334063798859287989978009289894830407929161239 / 3212647812998803962430237159045270718043979792653966281224804280403324460226632701152727892046940583118736898378576353014395863368493431680806320096708778695840163263355610036175222527881665695855902618223979209467997912798034943739828425694465502089816707767539650 := by rw [hrs 62, v62]; norm_num
have v64 : r 64 = 8048763716019973698502388369119050162801369194007823389218812806080971929153589774583918578332999720638682917277694095491865889315713519158242374179229177270147051859294286358957245234130770334542150581649154454782167749492850889449860772858057703657648401 / 193553167709305267953039471956075321100700279238345312815503511435274760560763667152195609660494142061645655404022610538081841829773431029405700662478077997116082761037326028592789847426537440986931396746554714620619606818651759356704187703089196440734480775469225194021436850 := by rw [hrs 63, v63]; norm_num
have v65 : r 65 = 8048763716019973698502388369119050162801369194007823389218812806080971929153589774583918578332999720638682917277694095491865889315713519158242374179229177270147051859294286358957245234130770334542150581649154454782167749492850889449860772858057703657648401 / 193553167709305267953039471956075321100700279238345312815503511435274760560763667152195609660494142061645655404022610538081841829773431029405700662478077997116082761037326028592789847426537440986931396746554714620619606818651759356704187703089196440734480775469225194021436850 := by rw [hrs 64, v64]; norm_num
have v66 : r 66 = 407188854206838223647708076247283161846499777423034694492943360482135632116747857491287309186023039085039011547273157697294772044296151791058934478070156810174326798350402000053472771812951986905227286176145679892235130039050138032888616893913757526970900952284918205661 / 28122335288450643321298259765041266230974318006908246854900456191763861850619549099411034907572721724737166437423306356558371344379707144474817848022592079392437421413207179507314556794737474020122496148137670787743514852948411824098475027348717241770421924037313766742452154446717691790350 := by rw [hrs 65, v65]; norm_num
have v67 : r 67 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 := by rw [hrs 66, v66]; norm_num
have v68 : r 68 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 := by rw [hrs 67, v67]; norm_num
have v69 : r 69 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 := by rw [hrs 68, v68]; norm_num
have v70 : r 70 = 36416936899996286494876250791284057441414775720782902350472381134125269640665010033807751812323538341742929953861281345043176308525962665232378873405395939901956762657081963511118422851948338443279880053224782654113350430921639602001618224755399033580885950306755481814684409 / 39298685656451409539405292862604201215221900494895715411728140591038464063430919682949868989505365219860486385817639345475442725691745978124855482365882600992500508993822563579932000641545246207725558444834395774537754782292316702819866874242617099277581234666298966607470747214777790143979106650 := by rw [hrs 69, v69]; norm_num
have v71 : r 71 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 := by rw [hrs 70, v70]; norm_num
have v72 : r 72 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 := by rw [hrs 71, v71]; norm_num
have v73 : r 73 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 := by rw [hrs 72, v72]; norm_num
have v74 : r 74 = 75781634625181512332154888603935503653844851654310022122790228373597125904033677520149499577225428822197899678473159763355429415233224842126232689396951555003220929857037478345345104291189365324396370306451011705182949010511700880622103721475427473328170650772849717788901617214809 / 951580378718282909609046271045034121039645074900330092661071194406575511793583524179851958155201378207328030230993995810948989407478947393360135017637081960445057942302378239475216040066409310481423266186700745838841695723920053550232100306121316815379415172852731158680593654066737364213607431357539150 := by rw [hrs 73, v73]; norm_num
have v75 : r 75 = 159964742255280287252007403680852356718468955486655582796138215043268508523404698399092363050236460750020965043497268463261460813104623030344176518783847346908302141162051473749502547418078740588025473883244848090485920191077491746663073295302807911847290317196943416398797297243804402225308642529514099 / 5991615048287496872973786254379493828285679024998760976850704496994359646577100787089412393551004381083960434983220620346300807882132714002552937788602375656459552354649787559992629326866999071212873512973392403929715070563144240802326570360892832376505271838369324405361909504615297187691606917709989831007596911499462418150 := by rw [hrs 74, v74]; norm_num
have v76 : r 76 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 := by rw [hrs 75, v75]; norm_num
have v77 : r 77 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 := by rw [hrs 76, v76]; norm_num
have v78 : r 78 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 := by rw [hrs 77, v77]; norm_num
have v79 : r 79 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 := by rw [hrs 78, v78]; norm_num
have v80 : r 80 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 := by rw [hrs 79, v79]; norm_num
have v81 : r 81 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 := by rw [hrs 80, v80]; norm_num
have v82 : r 82 = 1457185579183271732997293635144955660542381201910852197291818914753871912261759652176631237672762620909416524522729139426828864159798337904019391416509905087339006570161976364493308993939278164368970136538400648203420348979789802632181799403040909111457842836442977968283125305656552692165791333804885010035246649 / 6382175048012301351238658667238457414666390726663188590860437672004815403862505619440762626067826902883963420293317006516362808580213727192779074292074559370855595155680146654766914341314842067073282938224126440512391892044712151091083633159871711794628541454514442541310235033066770604425908252229450194945353769661129095096104030618150 := by rw [hrs 81, v81]; norm_num
have v83 : r 83 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 := by rw [hrs 82, v82]; norm_num
have v84 : r 84 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 := by rw [hrs 83, v83]; norm_num
have v85 : r 85 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 := by rw [hrs 84, v84]; norm_num
have v86 : r 86 = 221447344855572750707723846640126382241402060985317043076944140293553485441285897005794353329071944217988680496087817399576299321393094702334823052374944308061561245741903532122206077659338787347011332059130369179330698085893971247952394535670317453965710608757164936837886574542777931635605123846856515438529202626878188816679662850699 / 10287434934456408954281533955019965557029168234862663621190353837770762386964547604572358719446707287462884513565473801606371394663304206570663043711741449405005738199129945253469026895405249374617778363867730047056015856807241259296596471955684048214778043205826930330600725124955380957602759025657766557026681569966721026455431855808412027397422439743860053150 := by rw [hrs 85, v85]; norm_num
have v87 : r 87 = 2282074496642673776260768825238797350444591093432047699080242255305205892697221899727430224539768138483840882757379412130118108590650658064506054831375799629136183685930304075867961412852921974736582118770738057838549640338377085026802986387405501468831461075878050587213266253369778685819799541124657252873155959941008808846879901517869328869456285957624995229 / 265317241810557507380526149530850180254452898359821411986845851562677563831912203833914503581009138564266606920502256299450743021984270794162590933028315745966580987541693744354898707749543166513580742193509746730032205826657540706189083618947955651725032930464089061027562381711879362817617142758055067187490721762435122970327338796192603808167802793568121892214293687744322005236076150 := by rw [hrs 86, v86]; norm_num
have v88 : r 88 = 23367331058921374616615207499262436035856746986047844280626339436870958291313779858280158825389623139014543875063122503853605095459172944543557922575453129251484013390961492319118333117986934520495895766587427989931367752620373401851764206656520615546375164359705563335484058837479235396890766007707872995694606945243518850940965289959275023803608491983782060389338553366599829 / 10924641221290394633676715177212711022334407879583031671968036680192101044070310606814717946527149436351707378686347555961869667410954701112777255058988460110773547723742724745629101249248549122926701508987033300471557533755647394952987986734020789236912876791862293318417134338752081063425186941945958230463654220910562360481283638476530381724103183465784872007702460747679783474225968644022518231618650 := by rw [hrs 87, v87]; norm_num
have v89 : r 89 = 23367331058921374616615207499262436035856746986047844280626339436870958291313779858280158825389623139014543875063122503853605095459172944543557922575453129251484013390961492319118333117986934520495895766587427989931367752620373401851764206656520615546375164359705563335484058837479235396890766007707872995694606945243518850940965289959275023803608491983782060389338553366599829 / 10924641221290394633676715177212711022334407879583031671968036680192101044070310606814717946527149436351707378686347555961869667410954701112777255058988460110773547723742724745629101249248549122926701508987033300471557533755647394952987986734020789236912876791862293318417134338752081063425186941945958230463654220910562360481283638476530381724103183465784872007702460747679783474225968644022518231618650 := by rw [hrs 88, v88]; norm_num
have v90 : r 90 = 3539036143247411942363317528160010236417878256559156557439946970859330270341139842034767600089174976756089489486873630374377741568860487924221017915515239226168163422567198170803806467131679016480182589590561479236094757769405184121295462056292942454224626240562626129537660001345182309413768264477884827351875112598111465376573853220171893799327698686816244141491348270598935682423159625338830785860369 / 6762025391331457939022650246359620955027430161278254949252380113744059778741616694439991289265407750129663538246610756564895329700142309618314734053731499737525673306378809301500714844366979576943751732134939213905622267379049847571441327374700154660524987518509706510342956483163140948966609646122655416369705305850263916330487471383579465953294031045973341623805221219194412667768502808686207913733319219244908727997517240970150 := by rw [hrs 89, v89]; norm_num
have v91 : r 91 = 3539036143247411942363317528160010236417878256559156557439946970859330270341139842034767600089174976756089489486873630374377741568860487924221017915515239226168163422567198170803806467131679016480182589590561479236094757769405184121295462056292942454224626240562626129537660001345182309413768264477884827351875112598111465376573853220171893799327698686816244141491348270598935682423159625338830785860369 / 6762025391331457939022650246359620955027430161278254949252380113744059778741616694439991289265407750129663538246610756564895329700142309618314734053731499737525673306378809301500714844366979576943751732134939213905622267379049847571441327374700154660524987518509706510342956483163140948966609646122655416369705305850263916330487471383579465953294031045973341623805221219194412667768502808686207913733319219244908727997517240970150 := by rw [hrs 90, v90]; norm_num
have v92 : r 92 = 1922797628928914421157211581250125666244367330545267684475844413272673032955536964797159579258485037740904420183280641420369636194569664263201931890792616436052065579772022975455932586311030203214564139485925604184330521617836531667769741236123389649790179236551407939259327559599285354366417122231020441547483478920007619216396378213134514079432509869564823812436258407770279069827839642858847030312365324818253992421000649 / 16094065175420312418976442914756120349395968539071838616061710926185427022760216874223822139247851367032545214029105992881776408910481938691597572180788857134642428800952435493681759530831486356432449149474485664195498245469778538982696896819808589647245843797423112414808704142631619009891595581387901743793037087126730343033959855448712939628479441427038758847089364734264650581323362592719606114734516547220985984427484054751638579260270936963170650 := by rw [hrs 91, v91]; norm_num
have v93 : r 93 = 1922797628928914421157211581250125666244367330545267684475844413272673032955536964797159579258485037740904420183280641420369636194569664263201931890792616436052065579772022975455932586311030203214564139485925604184330521617836531667769741236123389649790179236551407939259327559599285354366417122231020441547483478920007619216396378213134514079432509869564823812436258407770279069827839642858847030312365324818253992421000649 / 16094065175420312418976442914756120349395968539071838616061710926185427022760216874223822139247851367032545214029105992881776408910481938691597572180788857134642428800952435493681759530831486356432449149474485664195498245469778538982696896819808589647245843797423112414808704142631619009891595581387901743793037087126730343033959855448712939628479441427038758847089364734264650581323362592719606114734516547220985984427484054751638579260270936963170650 := by rw [hrs 92, v92]; norm_num
have v94 : r 94 = 421200028990351211773809617704358922232415859245126380838392897277152007549468876931735597216254130091947449673178431182242150304686934121878907617992778857740031039018795156230610394398106485709729510932310800119608672587637111828199133470925040115710902775360528392706820740420787097896335090198662810782741171033311656358975754686785155156891071370866234035701061764361908089577479531972349540475819773226492470317497299485147969744475771042971387 / 22769700200595762447252288874412593725714991138088344743316097712058365740967734456112561014662512467039386157196278487662525599644949768439108311893225253688001117962311959784992353509304780743163850890965897048053930436417283752757575669914781036279750856527698070883654581753619767223427706174560218009664532416566425408819434730731053356895154565357301382503564552964003245343140244800591166150664221084448146370389083787874983476753865658857743882047246280942843383017633450 := by rw [hrs 93, v93]; norm_num
have v95 : r 95 = 421200028990351211773809617704358922232415859245126380838392897277152007549468876931735597216254130091947449673178431182242150304686934121878907617992778857740031039018795156230610394398106485709729510932310800119608672587637111828199133470925040115710902775360528392706820740420787097896335090198662810782741171033311656358975754686785155156891071370866234035701061764361908089577479531972349540475819773226492470317497299485147969744475771042971387 / 22769700200595762447252288874412593725714991138088344743316097712058365740967734456112561014662512467039386157196278487662525599644949768439108311893225253688001117962311959784992353509304780743163850890965897048053930436417283752757575669914781036279750856527698070883654581753619767223427706174560218009664532416566425408819434730731053356895154565357301382503564552964003245343140244800591166150664221084448146370389083787874983476753865658857743882047246280942843383017633450 := by rw [hrs 94, v94]; norm_num
have v96 : r 96 = 421200028990351211773809617704358922232415859245126380838392897277152007549468876931735597216254130091947449673178431182242150304686934121878907617992778857740031039018795156230610394398106485709729510932310800119608672587637111828199133470925040115710902775360528392706820740420787097896335090198662810782741171033311656358975754686785155156891071370866234035701061764361908089577479531972349540475819773226492470317497299485147969744475771042971387 / 22769700200595762447252288874412593725714991138088344743316097712058365740967734456112561014662512467039386157196278487662525599644949768439108311893225253688001117962311959784992353509304780743163850890965897048053930436417283752757575669914781036279750856527698070883654581753619767223427706174560218009664532416566425408819434730731053356895154565357301382503564552964003245343140244800591166150664221084448146370389083787874983476753865658857743882047246280942843383017633450 := by rw [hrs 95, v95]; norm_num
have v97 : r 97 = 574683659394598440680245744935850408685320969178434055381507638912219027706457263497539495397985872063212051487654576573907024523037206353160129808073130288697853902815923856146182036139967811666691660954581277476389266212011915354440034074019071179564277357117516773760005707863747846985704496970625947286805232071970785213419754548992839986325860468381991906516105146277173556771139227849493495439903572908331020354143726017391984099768061770423737824163237 / 97793625488980793383841525097995356633150866423075026011643401043167545955664392559738215516093971615371914062901319299308197971622675735225668510019950386034267746106302367711924840458647632699533311903150850222631527454340090520555200350807747792647306842342068789914510889289340006372309735705309253730252115295152726061813735156041361879913960835120263301922293987302275308033968086664030093341531354455289673559369834215720816982156080181785549447491694337222118786069631398457505450 := by rw [hrs 96, v96]; norm_num
have v98 : r 98 = 574683659394598440680245744935850408685320969178434055381507638912219027706457263497539495397985872063212051487654576573907024523037206353160129808073130288697853902815923856146182036139967811666691660954581277476389266212011915354440034074019071179564277357117516773760005707863747846985704496970625947286805232071970785213419754548992839986325860468381991906516105146277173556771139227849493495439903572908331020354143726017391984099768061770423737824163237 / 97793625488980793383841525097995356633150866423075026011643401043167545955664392559738215516093971615371914062901319299308197971622675735225668510019950386034267746106302367711924840458647632699533311903150850222631527454340090520555200350807747792647306842342068789914510889289340006372309735705309253730252115295152726061813735156041361879913960835120263301922293987302275308033968086664030093341531354455289673559369834215720816982156080181785549447491694337222118786069631398457505450 := by rw [hrs 97, v97]; norm_num
have v99 : r 99 = 1161253982954115450632071110849528470792494251823669704195891048507909683961669550088715655436330185205983763927901688679489127521003965331376582880032423003281765596557449339474675004089201894144832757183875252874355250984054809052914829031112638493532250971491336405217204084079023968083739549128007221249451900079648014920892729225328437696698036636361730691160479552926955312903539482434838075758639303980691247610301230929503368330302600664849470782584066272028869839 / 426766797782349344100583430358846750964823536309783372046770841116704164267958590422457444493100456265031415212538945525323151306892367836417014838329016866995025124428017812577530045918933128526494194832182867616997302919275351402578931231623862459740463397183417231572130288594375862693574979236303859822646981398531145082686804466115213458533412355713050825517858157571983938938499020501789645999094570966141564893442241222299292590343811955066132768784809995353690988188981260498694410488921268650 := by rw [hrs 98, v98]; norm_num
have v100 : r 100 = 493194876819595682416230825422962914766142554534757606805596000406205047287947302235621696937995691438111870808133487161585734431117036904531160037728958452112516155227623049266632659898265889611070794228324109273048769645189389196373819538040191672739776835073585190189130130250621286217345831542364037295204530177468125642161555537278312899418846717150463420137601137323867684024867443402772128918887917464532087156288032289765368512689837500943156797171821259067456275051384307218945201 / 431367556096659183461813462034098034301924646541448507656611797171215848597996775821001858054438934523961038087543256221766158297120930142251581973321903116546795768085833633375811957742227290711439329146698525913668229877785142086467084198608809858488200226275994330891980275563548884837623422868106630147398229952130785101061543553632324695844746010940320668028940180071385716206994081607649537082973298037867775819070749780467398781681185348645683658246956216740413728849861746611819717559009474875848841639720437850 := by rw [hrs 99, v99]; norm_num
have v101 : r 101 = 167957767397664854045821899531172964829817499952431862669492433107247389252964034728062742778414655188479990722394436597415176502956620950223269873488898280121755560007365838515644187621752596426016075217895015258986489758362689583198372176424813015717638476275834951517147544720139124367157212985565141915856127464101183795558840083531566005572177496731179002611623496742650796159901063943304826312020030262330202382855279370234130468836156740490622182129566192916650902624234683151192394888233431307 / 473830918267472574175258513129986452743223015915862785528202489246551712618137127912249851741941297469648287545053699189791774687390521417468435642174794621396598061921250411544186059725798272912379009411412190496365336129355487964993794460406898705655108628177502890608412889247520649913971137714050675097727592659143286788688385544420998507797576313314888896792418201873055580877901172822953493363228138191107988774906502228997322398171417565290596353686393484628769683750302387214983797782848689486817493892324153198305635164250 := by rw [hrs 100, v100]; norm_num
exact ⟨v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20, v21, v22, v23, v24, v25, v26, v27, v28, v29, v30, v31, v32, v33, v34, v35, v36, v37, v38, v39, v40, v41, v42, v43, v44, v45, v46, v47, v48, v49, v50, v51, v52, v53, v54, v55, v56, v57, v58, v59, v60, v61, v62, v63, v64, v65, v66, v67, v68, v69, v70, v71, v72, v73, v74, v75, v76, v77, v78, v79, v80, v81, v82, v83, v84, v85, v86, v87, v88, v89, v90, v91, v92, v93, v94, v95, v96, v97, v98, v99, v100, v101⟩
private theorem range_1_25 (r : ℕ → ℝ) (h0 : r 0 = 1 / 2)
(hrs : ∀ m : ℕ, r (m + 1) = if (1 : ℝ) / ((2 : ℝ) ^ m - 1) ≤ r m then r m - 1 / ((2 : ℝ) ^ m - 1) else r m) :
∀ m : ℕ, 1 ≤ m → m ≤ 25 → r m < (1 : ℝ) / ((2 : ℝ) ^ m - 1) →
∃ n : ℕ, m < n ∧ n ≤ 3 * m + 2 ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - 1) := by
intro m hm1 hm2 hlt
obtain ⟨v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20, v21, v22, v23, v24, v25, v26, v27, v28, v29, v30, v31, v32, v33, v34, v35, v36, v37, v38, v39, v40, v41, v42, v43, v44, v45, v46, v47, v48, v49, v50, v51, v52, v53, v54, v55, v56, v57, v58, v59, v60, v61, v62, v63, v64, v65, v66, v67, v68, v69, v70, v71, v72, v73, v74, v75, v76, v77, v78, v79, v80, v81, v82, v83, v84, v85, v86, v87, v88, v89, v90, v91, v92, v93, v94, v95, v96, v97, v98, v99, v100, v101⟩ := walk_values r h0 hrs
interval_cases m
· exact ⟨4, by norm_num, by norm_num, by rw [v4]; norm_num⟩
· rw [v2] at hlt; norm_num at hlt
· rw [v3] at hlt; norm_num at hlt
· exact ⟨5, by norm_num, by norm_num, by rw [v5]; norm_num⟩
· exact ⟨8, by norm_num, by norm_num, by rw [v8]; norm_num⟩
· rw [v6] at hlt; norm_num at hlt
· rw [v7] at hlt; norm_num at hlt
· exact ⟨9, by norm_num, by norm_num, by rw [v9]; norm_num⟩
· exact ⟨10, by norm_num, by norm_num, by rw [v10]; norm_num⟩
· exact ⟨11, by norm_num, by norm_num, by rw [v11]; norm_num⟩
· exact ⟨12, by norm_num, by norm_num, by rw [v12]; norm_num⟩
· exact ⟨13, by norm_num, by norm_num, by rw [v13]; norm_num⟩
· exact ⟨15, by norm_num, by norm_num, by rw [v15]; norm_num⟩
· rw [v14] at hlt; norm_num at hlt
· exact ⟨16, by norm_num, by norm_num, by rw [v16]; norm_num⟩
· exact ⟨17, by norm_num, by norm_num, by rw [v17]; norm_num⟩
· exact ⟨18, by norm_num, by norm_num, by rw [v18]; norm_num⟩
· exact ⟨19, by norm_num, by norm_num, by rw [v19]; norm_num⟩
· exact ⟨22, by norm_num, by norm_num, by rw [v22]; norm_num⟩
· rw [v20] at hlt; norm_num at hlt
· rw [v21] at hlt; norm_num at hlt
· exact ⟨23, by norm_num, by norm_num, by rw [v23]; norm_num⟩
· exact ⟨24, by norm_num, by norm_num, by rw [v24]; norm_num⟩
· exact ⟨25, by norm_num, by norm_num, by rw [v25]; norm_num⟩
· exact ⟨28, by norm_num, by norm_num, by rw [v28]; norm_num⟩
private theorem range_26_50 (r : ℕ → ℝ) (h0 : r 0 = 1 / 2)
(hrs : ∀ m : ℕ, r (m + 1) = if (1 : ℝ) / ((2 : ℝ) ^ m - 1) ≤ r m then r m - 1 / ((2 : ℝ) ^ m - 1) else r m) :
∀ m : ℕ, 26 ≤ m → m ≤ 50 → r m < (1 : ℝ) / ((2 : ℝ) ^ m - 1) →
∃ n : ℕ, m < n ∧ n ≤ 3 * m + 2 ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - 1) := by
intro m hm1 hm2 hlt
obtain ⟨v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20, v21, v22, v23, v24, v25, v26, v27, v28, v29, v30, v31, v32, v33, v34, v35, v36, v37, v38, v39, v40, v41, v42, v43, v44, v45, v46, v47, v48, v49, v50, v51, v52, v53, v54, v55, v56, v57, v58, v59, v60, v61, v62, v63, v64, v65, v66, v67, v68, v69, v70, v71, v72, v73, v74, v75, v76, v77, v78, v79, v80, v81, v82, v83, v84, v85, v86, v87, v88, v89, v90, v91, v92, v93, v94, v95, v96, v97, v98, v99, v100, v101⟩ := walk_values r h0 hrs
interval_cases m
· rw [v26] at hlt; norm_num at hlt
· rw [v27] at hlt; norm_num at hlt
· exact ⟨29, by norm_num, by norm_num, by rw [v29]; norm_num⟩
· exact ⟨30, by norm_num, by norm_num, by rw [v30]; norm_num⟩
· exact ⟨31, by norm_num, by norm_num, by rw [v31]; norm_num⟩
· exact ⟨36, by norm_num, by norm_num, by rw [v36]; norm_num⟩
· rw [v32] at hlt; norm_num at hlt
· rw [v33] at hlt; norm_num at hlt
· rw [v34] at hlt; norm_num at hlt
· rw [v35] at hlt; norm_num at hlt
· exact ⟨37, by norm_num, by norm_num, by rw [v37]; norm_num⟩
· exact ⟨40, by norm_num, by norm_num, by rw [v40]; norm_num⟩
· rw [v38] at hlt; norm_num at hlt
· rw [v39] at hlt; norm_num at hlt
· exact ⟨41, by norm_num, by norm_num, by rw [v41]; norm_num⟩
· exact ⟨43, by norm_num, by norm_num, by rw [v43]; norm_num⟩
· rw [v42] at hlt; norm_num at hlt
· exact ⟨52, by norm_num, by norm_num, by rw [v52]; norm_num⟩
· rw [v44] at hlt; norm_num at hlt
· rw [v45] at hlt; norm_num at hlt
· rw [v46] at hlt; norm_num at hlt
· rw [v47] at hlt; norm_num at hlt
· rw [v48] at hlt; norm_num at hlt
· rw [v49] at hlt; norm_num at hlt
· rw [v50] at hlt; norm_num at hlt
private theorem range_51_75 (r : ℕ → ℝ) (h0 : r 0 = 1 / 2)
(hrs : ∀ m : ℕ, r (m + 1) = if (1 : ℝ) / ((2 : ℝ) ^ m - 1) ≤ r m then r m - 1 / ((2 : ℝ) ^ m - 1) else r m) :
∀ m : ℕ, 51 ≤ m → m ≤ 75 → r m < (1 : ℝ) / ((2 : ℝ) ^ m - 1) →
∃ n : ℕ, m < n ∧ n ≤ 3 * m + 2 ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - 1) := by
intro m hm1 hm2 hlt
obtain ⟨v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20, v21, v22, v23, v24, v25, v26, v27, v28, v29, v30, v31, v32, v33, v34, v35, v36, v37, v38, v39, v40, v41, v42, v43, v44, v45, v46, v47, v48, v49, v50, v51, v52, v53, v54, v55, v56, v57, v58, v59, v60, v61, v62, v63, v64, v65, v66, v67, v68, v69, v70, v71, v72, v73, v74, v75, v76, v77, v78, v79, v80, v81, v82, v83, v84, v85, v86, v87, v88, v89, v90, v91, v92, v93, v94, v95, v96, v97, v98, v99, v100, v101⟩ := walk_values r h0 hrs
interval_cases m
· rw [v51] at hlt; norm_num at hlt
· exact ⟨54, by norm_num, by norm_num, by rw [v54]; norm_num⟩
· rw [v53] at hlt; norm_num at hlt
· exact ⟨61, by norm_num, by norm_num, by rw [v61]; norm_num⟩
· rw [v55] at hlt; norm_num at hlt
· rw [v56] at hlt; norm_num at hlt
· rw [v57] at hlt; norm_num at hlt
· rw [v58] at hlt; norm_num at hlt
· rw [v59] at hlt; norm_num at hlt
· rw [v60] at hlt; norm_num at hlt
· exact ⟨62, by norm_num, by norm_num, by rw [v62]; norm_num⟩
· exact ⟨64, by norm_num, by norm_num, by rw [v64]; norm_num⟩
· rw [v63] at hlt; norm_num at hlt
· exact ⟨67, by norm_num, by norm_num, by rw [v67]; norm_num⟩
· rw [v65] at hlt; norm_num at hlt
· rw [v66] at hlt; norm_num at hlt
· exact ⟨68, by norm_num, by norm_num, by rw [v68]; norm_num⟩
· exact ⟨69, by norm_num, by norm_num, by rw [v69]; norm_num⟩
· exact ⟨71, by norm_num, by norm_num, by rw [v71]; norm_num⟩
· rw [v70] at hlt; norm_num at hlt
· exact ⟨72, by norm_num, by norm_num, by rw [v72]; norm_num⟩
· exact ⟨73, by norm_num, by norm_num, by rw [v73]; norm_num⟩
· exact ⟨76, by norm_num, by norm_num, by rw [v76]; norm_num⟩
· rw [v74] at hlt; norm_num at hlt
· rw [v75] at hlt; norm_num at hlt
private theorem range_76_100 (r : ℕ → ℝ) (h0 : r 0 = 1 / 2)
(hrs : ∀ m : ℕ, r (m + 1) = if (1 : ℝ) / ((2 : ℝ) ^ m - 1) ≤ r m then r m - 1 / ((2 : ℝ) ^ m - 1) else r m) :
∀ m : ℕ, 76 ≤ m → m ≤ 100 → r m < (1 : ℝ) / ((2 : ℝ) ^ m - 1) →
∃ n : ℕ, m < n ∧ n ≤ 3 * m + 2 ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - 1) := by
intro m hm1 hm2 hlt
obtain ⟨v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20, v21, v22, v23, v24, v25, v26, v27, v28, v29, v30, v31, v32, v33, v34, v35, v36, v37, v38, v39, v40, v41, v42, v43, v44, v45, v46, v47, v48, v49, v50, v51, v52, v53, v54, v55, v56, v57, v58, v59, v60, v61, v62, v63, v64, v65, v66, v67, v68, v69, v70, v71, v72, v73, v74, v75, v76, v77, v78, v79, v80, v81, v82, v83, v84, v85, v86, v87, v88, v89, v90, v91, v92, v93, v94, v95, v96, v97, v98, v99, v100, v101⟩ := walk_values r h0 hrs
interval_cases m
· exact ⟨77, by norm_num, by norm_num, by rw [v77]; norm_num⟩
· exact ⟨78, by norm_num, by norm_num, by rw [v78]; norm_num⟩
· exact ⟨79, by norm_num, by norm_num, by rw [v79]; norm_num⟩
· exact ⟨80, by norm_num, by norm_num, by rw [v80]; norm_num⟩
· exact ⟨81, by norm_num, by norm_num, by rw [v81]; norm_num⟩
· exact ⟨83, by norm_num, by norm_num, by rw [v83]; norm_num⟩
· rw [v82] at hlt; norm_num at hlt
· exact ⟨84, by norm_num, by norm_num, by rw [v84]; norm_num⟩
· exact ⟨85, by norm_num, by norm_num, by rw [v85]; norm_num⟩
· exact ⟨88, by norm_num, by norm_num, by rw [v88]; norm_num⟩
· rw [v86] at hlt; norm_num at hlt
· rw [v87] at hlt; norm_num at hlt
· exact ⟨90, by norm_num, by norm_num, by rw [v90]; norm_num⟩
· rw [v89] at hlt; norm_num at hlt
· exact ⟨92, by norm_num, by norm_num, by rw [v92]; norm_num⟩
· rw [v91] at hlt; norm_num at hlt
· exact ⟨94, by norm_num, by norm_num, by rw [v94]; norm_num⟩
· rw [v93] at hlt; norm_num at hlt
· exact ⟨95, by norm_num, by norm_num, by rw [v95]; norm_num⟩
· exact ⟨97, by norm_num, by norm_num, by rw [v97]; norm_num⟩
· rw [v96] at hlt; norm_num at hlt
· exact ⟨101, by norm_num, by norm_num, by rw [v101]; norm_num⟩
· rw [v98] at hlt; norm_num at hlt
· rw [v99] at hlt; norm_num at hlt
· rw [v100] at hlt; norm_num at hlt
theorem spec_a70fcca4__h4__h1__h2 : ∀ (r : ℕ → ℝ),
r (0 : ℕ) = (1 / 2 : ℝ) →
(∀ (m : ℕ),
r (m + (1 : ℕ)) =
if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) →
∀ (m : ℕ),
(1 : ℕ) ≤ m →
r m < (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) →
∃ (n : ℕ), m < n ∧ n ≤ (3 : ℕ) * m + (2 : ℕ) ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) := by
-- approach: the window statement is decided exactly for every skipped m ≤ 100 by computing the greedy walk of 1/2 to step 101 in the kernel (one `norm_num` per step); what remains is the same statement for m > 100
-- licence: CC-BY-4.0
intro r h0 hrs
-- label: after a skipped m > 100, another skip within (m, 3m+2]
-- claim: $m > 100 \wedge r_m < \frac{1}{2^m-1} \Rightarrow \exists n,\ m < n \le 3m+2 \wedge r_n < \frac{1}{2^n-1}$
-- The node's own statement restricted to m > 100: the tail of the ladder W(3m+2), where no mechanism is known.
-- The range 1 ≤ m ≤ 100 is closed below by exact computation of the walk (steps 1 to 101).
have htail : ∀ m : ℕ, 100 < m → r m < (1 : ℝ) / ((2 : ℝ) ^ m - 1) →
∃ n : ℕ, m < n ∧ n ≤ 3 * m + 2 ∧ r n < (1 : ℝ) / ((2 : ℝ) ^ n - 1) := by
sorry
intro m hm hlt
by_cases hN : m ≤ 100
· by_cases h25 : m ≤ 25
· exact range_1_25 r h0 hrs m (by omega) h25 hlt
by_cases h50 : m ≤ 50
· exact range_26_50 r h0 hrs m (by omega) h50 hlt
by_cases h75 : m ≤ 75
· exact range_51_75 r h0 hrs m (by omega) h75 hlt
exact range_76_100 r h0 hrs m (by omega) hN hlt
· exact htail m (by omega) hlt