diff c011cca..2e5cc7c pi_irrationality_exponent_v2.txt
diff --git a/pi_irrationality_exponent_v2.txt b/pi_irrationality_exponent_v2.txt
index e69de29..c2d97f2 100644
--- a/pi_irrationality_exponent_v2.txt
+++ b/pi_irrationality_exponent_v2.txt
@@ -0,0 +1,897 @@
+THE IRRATIONALITY EXPONENT OF PI
+================================
+
+What is proved, what is only conjectured, and complete proofs of
+everything that is actually proved.
+
+Written to be read by a good high school student.
+Angles are in radians. Logarithms are natural.
+
+Contents
+
+ 0. read this first
+ 1. measuring how close a fraction gets
+ 2. every irrational number has exponent at least 2
+ 3. exponent 2 is attained: mu(sqrt 2) = 2
+ 4. where the floor 2 comes from: convergents and Roth
+ 5. a complete warm-up: pi is irrational
+ 6. what is actually known: the upper bounds for pi
+ 7. the Flint-Hills series
+ 8. recap
+ 9. why this file is not the original
+
+
+0. READ THIS FIRST
+------------------
+
+The question of this document is: how well can a fraction p/q
+approximate pi?
+
+Write mu(pi) for the "irrationality exponent" of pi, defined
+carefully in section 1. Everybody expects
+
+ mu(pi) = 2.
+
+That value is NOT KNOWN. It is a famous open problem, and it has
+been open for well over a century of hard work.
+
+The best bound anyone has proved is
+
+ mu(pi) <= 7.103205334137... (Zeilberger and Zudilin, 2020)
+
+and nothing better has been published since. A 2026 preprint of Bai
+claims a tiny improvement to 7.101862832357; even if correct it does
+not come close to 2.
+
+The source document that this file replaces claims to prove
+mu(pi) = 2 outright. That claim is not believed and this file does
+not repeat it. Losing a famous open problem would be a bigger event
+than losing the proof itself, and a proof written in one pass with no
+independent check is not a proof. So this file does something more
+useful:
+
+ (a) defines mu carefully and computes it for simple numbers;
+ (b) proves completely that mu(x) >= 2 for every irrational x;
+ (c) proves completely that mu(sqrt 2) = 2, so exponent 2 is real
+ and attainable;
+ (d) proves completely that pi is irrational (Niven's proof);
+ (e) explains what the known upper bounds 42, 21, 8.016, 7.606,
+ 7.103 mean and why the gap down to 2 is the hard part;
+ (f) proves completely that if mu(pi) < 5/2 then the Flint-Hills
+ series sum 1/(n^3 sin^2 n) converges, and proves an
+ unconditional theorem of the same shape with 13 in place of 3.
+
+Every statement below is labelled PROVED, KNOWN or OPEN. Where a
+result is quoted from the literature, the source is named.
+
+
+1. MEASURING HOW CLOSE A FRACTION GETS
+--------------------------------------
+
+1.1 Distance to the nearest integer.
+
+For a real number x write ||x|| for the distance from x to the
+nearest integer:
+
+ ||x|| = min { |x - m| : m an integer }.
+
+Always 0 <= ||x|| <= 1/2. For example ||2.3|| = 0.3, ||2.7|| = 0.3,
+||2.5|| = 0.5, ||pi|| = 0.14159..., ||100 pi|| = 0.132169...
+
+Two facts we use without proof, both immediate from the definition:
+
+ ||x + y|| <= ||x|| + ||y|| (triangle inequality)
+
+ if ||x|| < 1/N then some integer m has |x - m| < 1/N.
+
+1.2 The one idea that makes everything work.
+
+Approximating x by a fraction with denominator q is the same thing
+as making q x close to an integer. Exactly:
+
+ |x - p/q| = |q x - p| / q,
+
+and as p runs over all integers, |q x - p| runs over all distances
+from q x to an integer. Taking the best p gives
+
+ |x - p/q| = ||q x|| / q (1.1)
+
+So: "there is a fraction with denominator q within q^(-nu) of x"
+is the same statement as
+
+ ||q x|| < q^(1-nu).
+
+That single rewriting, (1.1), is the whole subject. Everything below
+is either a way to find small values of ||q x|| (which is easy) or a
+way to prove they cannot be too small too often (which is hard).
+
+1.3 Definition of the irrationality exponent.
+
+Let x be irrational. Define mu(x) to be the largest real number mu
+such that
+
+ ||q x|| < q^(1-mu) for infinitely many positive integers q,
+
+equivalently, by (1.1), such that
+
+ 0 < |x - p/q| < q^(-mu) for infinitely many integers p and q.
+
+A larger mu means x can be approximated better, so mu measures how
+"irrational" x is. Note what the definition does and does not say:
+it is about infinitely many denominators, each with a good
+approximation, and it does not care about any single one.
+
+1.4 First examples.
+
+ x rational: only finitely many fractions come close, so the set
+ of such mu is empty; by convention mu(x) = 1.
+
+ x = sqrt 2: mu = 2. PROVED in section 3. This is the model case,
+ and it is essentially the reason 2 is the number everybody
+ expects for pi.
+
+ x = e = 2.71828...: mu = 2. KNOWN, and surprisingly hard
+ (Davis, 1978). It is not a homework exercise.
+
+ x = sum over k >= 1 of 10^(-k!): mu = infinity. That is, x can be
+ approximated by fractions better than any power of q. Sketch, and
+ it is a complete proof: put q_N = 10^(N!) and let p_N/q_N be the
+ sum of the first N terms. The tail is at most
+ 2 * 10^(-(N+1)!), and (N+1)! = (N+1) * N!, so
+
+ |x - p_N/q_N| < 2 * 10^(-(N+1)!) = 2 * q_N^(-(N+1)).
+
+ Since N is arbitrary, x beats every exponent. Such numbers are
+ called Liouville numbers.
+
+ x = pi: 2 <= mu(pi) <= 7.1033, and mu(pi) = 2 is conjectured.
+ The lower bound 2 is PROVED in section 2, for every irrational.
+ The upper bound 7.1033 is KNOWN (section 6). Whether it can be
+ pushed down even to 7 is not known. Whether it can be pushed all
+ the way to 2 is OPEN.
+
+So the honest one line summary is:
+
+ mu(pi) = 2 is expected, and beyond reach.
+
+
+2. EVERY IRRATIONAL NUMBER HAS EXPONENT AT LEAST 2
+--------------------------------------------------
+
+PROVED (Dirichlet's pigeonhole argument, 1842).
+
+Theorem 2.1. Let x be irrational and let nu be any real number with
+nu < 2. Then ||q x|| < q^(1-nu) for infinitely many positive
+integers q. Equivalently, there are infinitely many fractions p/q
+with 0 < |x - p/q| < q^(-nu). Hence mu(x) >= 2.
+
+Note the direction. This says approximations about as good as 1/q^2
+always exist. It says nothing about how much better they can get,
+which is the hard half, and it is why 2 is the number everybody
+expects.
+
+Proof. Fix nu < 2. It is enough to handle nu < 2 because nu' < nu
+gives a weaker requirement: if ||q x|| < q^(1-nu') and q >= 2 then
+also ||q x|| < q^(1-nu).
+
+Step 1, pigeonhole. Fix a positive integer N. Look at the N+1
+numbers
+
+ 0, x, 2x, 3x, ..., N x.
+
+Write each as an integer plus a fractional part in [0,1). There are
+N+1 fractional parts and they live in an interval of length 1 cut
+into N pieces, so two of them, say j x and k x with 0 <= j < k <= N,
+fall in the same piece. Their fractional parts therefore differ by
+less than 1/N, so
+
+ ||(k - j) x|| <= 1/N.
+
+Put q = k - j. Then 1 <= q <= N and ||q x|| <= 1/N.
+
+Step 2, compare 1/N with q^(1-nu). Since q <= N and 1 - nu > -1,
+
+ 1/N <= N^(1-nu) <= q^(1-nu).
+
+The middle inequality is N^(nu-2) <= 1, which holds exactly because
+nu <= 2. So
+
+ ||q x|| <= 1/N <= q^(1-nu).
+
+Step 3, infinitely many such q. Do step 1 and 2 for N = 1, 2, 3, ...
+getting for each N a denominator q_N <= N with ||q_N x|| <= 1/N.
+Suppose the q_N took only finitely many values. Some value q occurs
+for infinitely many N, and then ||q x|| <= 1/N for arbitrarily large
+N, forcing ||q x|| = 0, that is, q x is an integer and x is
+rational. That contradicts the hypothesis. So the q_N are unbounded,
+in particular there are infinitely many of them, and each satisfies
+||q x|| <= 1/N <= q^(1-nu). By (1.1) each gives a fraction with
+0 < |x - p/q| <= q^(-nu). The strict inequality follows by using
+nu' = (nu+2)/2 in place of nu and dropping the one possible q = 1.
+
+Done. Two remarks.
+
+ (i) The argument is pure bookkeeping: N+1 numbers, N boxes. It is
+ the cheapest possible way to force a coincidence, and it is the
+ reason 2 is a hard floor for every irrational number.
+
+ (ii) It is not sharp. Refining it by looking at several numbers at
+ once (the three distance theorem, or the continued fraction
+ expansion) shows that ||q x|| < 1/q happens for infinitely many q
+ that are denominators of convergents, but still nothing beats
+ q^(-2-epsilon) in general.
+
+
+3. EXPONENT 2 IS ATTAINED: mu(sqrt 2) = 2
+------------------------------------------
+
+PROVED. This section exists to show that "exponent exactly 2" is a
+real thing a number can have, so that the expectation mu(pi) = 2 is
+not obviously silly.
+
+The lower bound mu(sqrt 2) >= 2 is Theorem 2.1 and holds for every
+irrational number. Only the upper bound needs work.
+
+Theorem 3.1. mu(sqrt 2) <= 2.
+
+Proof. First, sqrt 2 is irrational: if 2 q^2 = p^2 with positive
+integers, then p is even, p = 2m, and 2 q^2 = 4 m^2 gives
+q^2 = 2 m^2, so q is even too and we may divide out a factor 2 and
+repeat forever, which is impossible. So 2 q^2 - p^2 is never 0.
+
+Take integers p and q with q >= 1. The identity
+
+ (sqrt 2 - p/q)(sqrt 2 + p/q) = 2 - p^2/q^2 = (2 q^2 - p^2)/q^2
+
+rearranges to
+
+ |sqrt 2 - p/q| = |2 q^2 - p^2| / ( q^2 |sqrt 2 + p/q| ).
+
+The numerator is a nonzero integer, so it is at least 1 in absolute
+value. If |sqrt 2 - p/q| >= 1 then that is already at least
+q^(-nu) for every nu > 0, so assume |sqrt 2 - p/q| < 1. Then
+p/q <= sqrt 2 + 1 and the denominator is at most
+q^2 (2 sqrt 2 + 1). Therefore
+
+ |sqrt 2 - p/q| >= 1 / ( (2 sqrt 2 + 1) q^2 ) (3.1)
+
+for every fraction p/q with |sqrt 2 - p/q| < 1.
+
+Now let nu > 2. For q with q^(nu-2) >= 2 sqrt 2 + 1, that is for
+q >= Q(nu) := (2 sqrt 2 + 1)^(1/(nu-2)), inequality (3.1) gives
+
+ |sqrt 2 - p/q| >= q^(-2) / (2 sqrt 2 + 1) >= q^(-nu).
+
+That is,
+q^(nu-2) >= 2 sqrt 2 + 1, so for those q every fraction p/q is at
+least q^(-nu) away from sqrt 2. Only finitely many denominators are
+excluded. Hence mu(sqrt 2) <= 2. Together with Theorem 2.1,
+mu(sqrt 2) = 2. Done.
+
+The number 2 sqrt 2 + 1 that appeared is not important. What
+matters is that it is a constant depending only on sqrt 2 and not on
+p or q. Any positive constant would do the same job, because
+q^(nu-2) eventually outgrows it. This is the standard shape of every
+upper bound in the subject:
+
+ a fixed positive constant, divided by a power of q.
+
+Improving mu(x) from 7.1 to something smaller means improving the
+size of the allowance in front of q^(-2), never the exponent 2. The
+exponent is what the definition measures.
+
+
+4. WHERE THE FLOOR 2 COMES FROM: CONVERGENTS AND ROTH
+-----------------------------------------------------
+
+Context, no proofs needed, but it explains why nobody is embarrassed
+by believing mu(x) = 2 for a specific number.
+
+4.1 Continued fractions. Every irrational x has a continued fraction
+
+ x = a0 + 1/(a1 + 1/(a2 + 1/(a3 + ...)))
+
+with a0 an integer and a1, a2, a3, ... positive integers, and the
+truncations p_n/q_n are the best possible rational approximations to
+x in the sense that no fraction with denominator at most q_n is
+closer, and
+
+ 1/(q_n (q_n + q_(n+1))) < |x - p_n/q_n| < 1/(q_n q_(n+1)).
+
+Known facts, both easy once you have the expansion:
+
+ mu(x) = 2 exactly when the a_n are bounded;
+
+ mu(x) > 2 exactly when the a_n grow, and mu(x) = infinity exactly
+ when they grow fast enough to make a Liouville number.
+
+So the conjecture mu(pi) = 2 is literally the conjecture that the
+continued fraction of pi has bounded partial quotients. Nothing is
+known about that beyond what has been computed, and the computed
+partial quotients look like a random draw, which is entirely
+consistent with boundedness.
+
+This is worth internalising: mu(pi) = 2 is not a mysterious
+analytic statement, it is a statement about one integer sequence,
+and we cannot prove anything about it.
+
+4.2 Liouville, and Roth. For an algebraic number of degree d,
+Liouville's 1844 argument (the same computation as (3.1), with
+d - 1 conjugates instead of one) proves mu(x) <= d. In particular
+mu(sqrt 2) <= 2. That was the state of the art for a century until
+Roth proved in 1955 that every irrational algebraic number has
+mu(x) = 2, and Roth's theorem is a landmark. It says in the one
+language of this document: no algebraic irrational can be
+approximated better than exponent 2 by rationals.
+
+Pi is not algebraic, so Roth says nothing about it. Realistically,
+the upper bounds for mu(pi) are not proved by algebra at all, they
+are proved by building explicit integrals that happen to vanish,
+which is section 6.
+
+
+5. A COMPLETE WARM-UP: PI IS IRRATIONAL
+---------------------------------------
+
+PROVED, following Niven (1947). The proof is twenty lines of
+one-variable calculus and it is the model for everything harder: an
+integral that is forced to be a positive integer smaller than 1.
+
+Theorem 5.1. Pi is irrational.
+
+Proof. Suppose pi = a/b with positive integers a and b. For each
+integer n >= 1 define the polynomial
+
+ f(x) = x^n (a - b x)^n / n!,
+
+which has degree 2n, and let F be the alternating sum of its even
+derivatives,
+
+ F(x) = f(x) - f''(x) + f''''(x) - f^(6)(x) + ... ,
+
+a finite sum because f has degree 2n. The cancellation that makes
+this work is
+
+ F'' + F = f, (5.1)
+
+because differentiating F twice and adding F back shifts the
+alternating sum onto itself and leaves only its first term.
+
+Step 1, the integral is a small positive number. On the interval
+(0, pi) we have a - b x = b (pi - x) > 0, so f(x) > 0 and the
+integral of f(x) sin x over (0, pi) is strictly positive. For an
+upper bound, x (pi - x) <= pi^2/4 on that interval, so
+
+ f(x) = ( b x (pi - x) )^n / n! <= ( b pi^2 / 4 )^n / n!
+
+and therefore
+
+ int_0^pi f(x) sin x dx <= pi ( b pi^2 / 4 )^n / n!.
+
+The right side tends to 0 as n grows, because n! beats any fixed
+exponential. So for all large n,
+
+ 0 < int_0^pi f(x) sin x dx < 1. (5.2)
+
+Step 2, the integral is an integer. By (5.1) and the product rule,
+
+ d/dx [ F'(x) sin x - F(x) cos x ] = ( F''(x) + F(x) ) sin x
+ = f(x) sin x.
+
+So the fundamental theorem of calculus gives
+
+ int_0^pi f(x) sin x dx
+ = [ F'(x) sin x - F(x) cos x ] from 0 to pi
+ = F(pi) + F(0),
+
+since sin pi = sin 0 = 0 and cos pi = cos 0 = -1.
+
+We claim F(0) and F(pi) are integers. Expand f:
+
+ f(x) = (1/n!) sum over k = 0..n of C(n,k) a^(n-k) (-b)^k x^(n+k),
+
+where C(n,k) is a binomial coefficient. A term with n + k = j has
+its j-th derivative at 0 equal to
+
+ j! / ( n! ) * C(n, j-n) * a^(2n-j) * (-b)^(j-n)
+ = ( j! / ( (j-n)! (2n-j)! ) ) * a^(2n-j) * (-b)^(j-n),
+
+and the bracket is a multinomial coefficient, hence an integer. Every
+other derivative at 0 vanishes, so F(0) is an integer. Finally
+a - b x = b (pi - x) makes f symmetric about pi/2,
+
+ f(pi - x) = (pi - x)^n ( b x )^n / n! = f(x),
+
+so differentiating gives f^(j)(pi) = (-1)^j f^(j)(0), and F(pi) is an
+integer as well. Therefore
+
+ int_0^pi f(x) sin x dx is a positive integer (5.3)
+
+for every n >= 1.
+
+Step 3, contradiction. (5.2) says that for large n the same integral
+lies strictly between 0 and 1, and (5.3) says it is a positive
+integer. There is no such integer. So pi cannot equal a/b. Done.
+
+The proof uses nothing about pi except sin pi = 0, and nothing about
+sin except its differential equation. Replacing sin by exp turns the
+same three steps into Niven's proof that e is irrational. It does
+not give any explicit bound on how well pi can be approximated: it
+only shows that the exact equality pi = p/q is impossible. Getting a
+quantitative bound out of such integrals is a separate and much
+harder trick, and it is the subject of the next section.
+
+
+6. WHAT IS ACTUALLY KNOWN: THE UPPER BOUNDS FOR PI
+--------------------------------------------------
+
+The results of this section are KNOWN from the literature. The
+constructions behind them are far beyond this document and are not
+reproduced: each one is a paper. What is reproduced is the precise
+form of the statement and what it does and does not give.
+
+6.1 The shape of every upper bound. One does not attack mu(pi) by
+looking at fractions. One builds, for each large n, an explicit
+integral or an explicit linear form whose size can be estimated two
+different ways: it is a nonzero integer (or a rational with a
+controlled denominator), so it is not small; and simultaneously it
+is an explicit expression in pi and logarithms, so it is very small.
+Squeezing the two estimates against each other forbids fractions
+p/q from being closer than q^(-kappa(n)), and then one optimises over
+n. Mahler used combinations of powers of logarithms with polynomial
+coefficients; Chudnovsky used Hermite-Pade approximation to the
+exponential function; Hata and Salikhov used explicit integrals;
+Zeilberger and Zudilin used a two-parameter family of integrals
+searched by computer and then bounded rigorously.
+
+6.2 The record.
+
+ 1953 Mahler mu(pi) <= 42, and 30 eventually
+ 1974 Mignotte mu(pi) <= 21, and 20 eventually
+ 1982 Chudnovsky mu(pi) <= (quantitative refinement)
+ 1993 Hata mu(pi) <= 8.01604539...
+ 2008 Salikhov mu(pi) <= 7.606308...
+ 2020 Zeilberger and Zudilin mu(pi) <= 7.103205334137...
+ 2026 Bai (preprint, unverified) mu(pi) <= 7.101862832357...
+
+Read the column: sixty-seven years of work moved 42 to 7.10. The
+last two entries moved 7.606 to 7.103 to 7.102. Every step is a real
+paper with a real new integral. Nothing here is anywhere near 2.
+
+6.3 The precise statement of the record. Since mu(pi) <= 7.1033, for
+every nu > 7.1033 there is a Q with
+
+ |pi - p/q| >= q^(-nu) for all q >= Q,
+
+and 7.104 is a safe rounded exponent. Compare this with what a proof
+of mu(pi) = 2 would deliver: the same statement with nu = 2.01, say,
+or even just nu = 2.49, which would already settle the Flint-Hills
+question of section 7.
+
+6.4 What the convergents look like. Here are the first eleven
+convergents of pi, computed to 50 digits, with the single-denominator
+exponent nu(q) = -log(|pi - p/q|) / log(q), that is, the exponent
+that that one fraction achieves.
+
+ q p |pi - p/q| nu(q)
+ 1 3 1.416e-01 0.000
+ 7 22 1.264e-03 3.429
+ 106 333 8.322e-05 2.014
+ 113 355 2.668e-07 3.202
+ 33102 103993 5.779e-10 2.044
+ 33215 104348 3.316e-10 2.097
+ 66317 208341 1.224e-10 2.056
+ 99532 312689 2.914e-11 2.108
+ 265381 833719 8.715e-12 2.039
+ 364913 1146408 1.611e-12 2.120
+ 1360120 4272943 4.041e-13 2.021
+
+Two things to notice, and they are the whole difficulty.
+
+First, single fractions can do much better than q^(-2). The famous
+355/113 has error 2.668e-07 while 1/113^2 = 7.8e-05, five hundred
+times smaller than the floor of Theorem 2.1 allows. That is not a
+contradiction of anything. The definition of mu demands a fixed gain
+eps > 0 achieved by infinitely many denominators q, and special
+denominators are free to be as lucky as they like.
+
+Second, look at the last column: it bounces around just above 2 and
+shows no trend. If mu(pi) = 2 were false, this column would have to
+crawl upward without bound, through denominators so large that the
+first billion convergents are not enough to see it. Numerically the
+evidence for mu(pi) = 2 is that random behaviour of the partial
+quotients is consistent with it, and that is all the evidence there
+is.
+
+6.5 Summary of the state of the art, stated without decoration:
+
+ 2 <= mu(pi) <= 7.1033, and the truth is almost certainly 2.
+ The gap between 2 and 7.1033 is entirely open. No known method
+ moves the upper bound anywhere near 2, and no known method
+ produces a single denominator q with q^(-2.01)-quality error
+ infinitely often being forced to fail.
+
+
+7. THE FLINT-HILLS SERIES
+-------------------------
+
+Now the payoff, and the place where the honesty of section 0 really
+bites.
+
+The question, popularised by Pickover and studied by Alekseyev,
+Meiburg and others, is whether
+
+ sum over n >= 1 of 1 / ( n^3 sin^2 n )
+
+converges, angles in radians. No one knows. The reason it is close
+but not decided is exactly the gap in section 6: with mu(pi) < 5/2
+it converges (proved below in full), and mu(pi) = 2 would give that,
+and 7.1033 does not.
+
+Why the series is delicate. sin n is small exactly when n is close
+to a multiple of pi. Since pi is irrational, n - q pi takes arbitrarily
+small values for suitable pairs, and at those n the denominator
+n^3 sin^2 n is far smaller than n^3, which is what makes the terms
+large. If the approximation were bad often enough, the terms would
+not shrink. A bound on mu(pi) is precisely a statement about how
+often and how well pi is approximated by fractions q pi, so it
+controls exactly this.
+
+The whole reduction is two lemmas and one summation, and every line
+of it is proved here.
+
+7.1 Lemma (grouping integers by their nearest multiple of pi).
+
+There is a constant C such that for all a, b > 0,
+
+ sum over n >= 1 of 1 / ( n^a |sin n|^b )
+
+ <= C * sum over q >= 1 of 1 / ( q^a ||q pi||^b ),
+
+provided pi is irrational.
+
+Proof. For each integer n >= 1 let q be the nearest integer to n/pi,
+so that
+
+ |n - q pi| <= pi/2. (7.1)
+
+For n >= 1 we get q >= 0, and the choices q = 0 and q = 1 could
+overlap; that is harmless, we only need an upper bound.
+
+First the q = 0 case. (7.1) then says |n| <= pi/2, so n = 1 is the
+only possibility. That single term is a finite number, say C0.
+
+Now fix q >= 1. Which integers n have q as their nearest integer to
+n/pi? They lie in the interval of length pi centred at q pi. Since
+pi < 4, that interval contains at most 4 integers. So at most 4
+values of n are charged to each q.
+
+For each such n, two estimates. First, sin is pi-periodic, so
+
+ |sin n| = |sin(n - q pi)|,
+
+the sine of a number within pi/2 of 0. On [0, pi/2] the sine is
+concave and stays above its chord, that is sin t >= (2/pi) t, so
+using (7.1),
+
+ |sin n| >= (2/pi) |n - q pi| >= (2/pi) ||q pi||. (7.2)
+
+The last step is the point of the whole reduction: n is an integer,
+so the distance from q pi to n is at least the distance from q pi to
+the nearest integer of all, which is ||q pi||. Note ||q pi|| > 0
+because pi is irrational, so there is no division by zero.
+
+Second, n >= q pi - pi/2 = pi (q - 1/2) >= (pi/2) q for q >= 1, so
+
+ 1/n^a <= (2/(pi q))^a. (7.3)
+
+Multiplying (7.2) and (7.3) and charging at most 4 integers to q,
+
+ sum over n charged to q of 1/(n^a |sin n|^b)
+
+ <= 4 (2/(pi q))^a (pi/(2 ||q pi||))^b,
+
+which is a constant times 1/(q^a ||q pi||^b). Adding C0 for n = 1
+gives the lemma with C = max(C0, 4 (2/pi)^a (pi/2)^b).
+
+So from here on we only have to understand
+
+ sum over q >= 1 of 1 / ( q^a ||q pi||^b ),
+
+a sum about how well q pi is approximated by integers.
+
+7.2 Lemma (dyadic blocks). Let alpha be irrational and let nu0 > 1
+and c > 0 satisfy
+
+ ||q alpha|| >= c q^(1-nu0) for every integer q >= 1. (7.4)
+
+Then for every a > 2 nu0 - 2 the series
+
+ sum over q >= 1 of 1 / ( q^a ||q alpha||^2 )
+
+converges.
+
+Where (7.4) comes from. If mu(alpha) <= nu0 with nu0 > 1, then for
+the exponent nu0 + eps the definition says only finitely many
+fractions do better than q^(-nu0-eps), so ||q alpha|| >= q^(1-nu0-eps)
+for all q >= Q. Lowering the constant c to cover the finitely many
+q < Q as well gives (7.4), with nu0 replaced by nu0 + eps. Since eps
+is arbitrary, we may then take any a > 2 nu0 - 2.
+
+Proof. Fix an integer K >= 1 and consider the block of integers
+
+ K <= q < 2K.
+
+Put d = c (2K)^(1-nu0), which is positive since nu0 > 1. Because
+1 - nu0 < 0 and q < 2K, (7.4) gives ||q alpha|| >= d for every q in
+the block.
+
+The points are also separated from each other, which is the step that
+is easy to forget. If K <= q < r < 2K then r - q is a nonzero integer
+of absolute value less than 2K, so
+
+ ||r alpha - q alpha|| = ||(r - q) alpha|| >= c (2K)^(1-nu0) = d.
+
+So on the circle of circumference 1, the points q alpha with q in the
+block are at mutual distance at least d and at distance at least d
+from 0. Put the ones in the upper half circle in order of distance
+from 0. The first distance is at least d and each successive distance
+exceeds the previous by at least d, so the sorted distances are at
+least d, 2d, 3d, ... The same holds in the lower half circle. No point
+lands exactly on 0 or on 1/2, because that would make 2 q alpha an
+integer. Hence
+
+ sum over K <= q < 2K of 1/||q alpha||^2
+ <= 2 * sum over j >= 1 of 1/(j d)^2
+ = (2/d^2) * (pi^2/6). (7.5)
+
+Now divide by q^a, using q >= K and (7.5):
+
+ sum over K <= q < 2K of 1/(q^a ||q alpha||^2)
+ <= (1/K^a) (2/d^2) (pi^2/6)
+ = (pi^2/3) c^(-2) 2^(2nu0-2) K^(2nu0-2-a). (7.6)
+
+The exponent 2 nu0 - 2 - a is negative by hypothesis, so summing
+(7.6) over the dyadic blocks K = 1, 2, 4, 8, ... gives a convergent
+geometric series. Done.
+
+Note what the lemma does and does not say. An exponent bound of size
+nu0 buys convergence of the q-series for every exponent a > 2 nu0 - 2,
+and hence, by Lemma 7.1, convergence of the sine series for those
+exponents. It says nothing at the boundary a = 2 nu0 - 2, and it gives
+no information at all if nu0 <= 1.
+
+7.3 Theorem (conditional). Suppose mu(pi) < 5/2. Then
+
+ sum over n >= 1 of 1 / ( n^3 sin^2 n )
+
+converges, angles in radians.
+
+Proof. Choose nu0 with mu(pi) < nu0 < 5/2, which is possible because
+the inequality is strict. By the definition of mu in section 1.3 and
+the remark opening the proof of Lemma 7.2, there is a constant c > 0
+with
+
+ ||q pi|| >= c q^(1-nu0) for every integer q >= 1.
+
+Now compare exponents. Since nu0 < 5/2,
+
+ 2 nu0 - 2 < 2 * (5/2) - 2 = 3,
+
+so a = 3 satisfies the hypothesis a > 2 nu0 - 2 of Lemma 7.2. That
+lemma therefore says
+
+ sum over q >= 1 of 1 / ( q^3 ||q pi||^2 ) converges,
+
+and Lemma 7.1 with a = 3 and b = 2 converts this into convergence of
+
+ sum over n >= 1 of 1 / ( n^3 |sin n|^2 ),
+
+which is the Flint-Hills series, since sin^2 n = |sin n|^2. Done.
+
+This is the whole content of the classical sufficient condition, and
+it is entirely elementary: one pigeonhole lemma, one dyadic block
+lemma, and the observation that 3 is bigger than 2 * 5/2 - 2 only
+when the exponent is strictly below 5/2. Meiburg's paper states the
+same criterion in the language of his Theorem 2.5.
+
+The boundary. At nu0 = 5/2 exactly, Lemma 7.2 says nothing: the
+exponent 2 nu0 - 2 - a becomes zero at a = 3 and the block series
+fails to converge. That is not an accident of the proof. Alekseyev,
+in the paper cited in section 0, shows in the other direction that
+convergence of the Flint-Hills series forces mu(pi) <= 5/2, so 5/2 is
+exactly where the two known arguments meet and neither one wins. The
+condition mu(pi) < 5/2 is NOT known for pi, since the best proven
+bound is 7.1033. So Theorem 7.3 is a theorem about a hypothesis, not
+about the series.
+
+7.4 Theorem (unconditional). The series
+
+ sum over n >= 1 of 1 / ( n^13 sin^2 n )
+
+converges, angles in radians.
+
+Proof. Use the record bound of section 6 in the shape of (7.4). Since
+mu(pi) <= 7.103205334137..., taking nu0 = 7.104 gives a constant c > 0
+with
+
+ ||q pi|| >= c q^(1-7.104) for every integer q >= 1.
+
+Compare exponents:
+
+ 2 nu0 - 2 = 2 * 7.104 - 2 = 12.208 < 13,
+
+so a = 13 satisfies a > 2 nu0 - 2. Lemma 7.2 gives convergence of
+
+ sum over q >= 1 of 1 / ( q^13 ||q pi||^2 ),
+
+and Lemma 7.1 with a = 13 and b = 2 gives convergence of the sine
+series. Done. For the record, the block exponent in (7.6) is
+
+ 2 nu0 - 2 - a = 12.208 - 13 = -0.792,
+
+which is comfortably negative, so there is a little slack: any
+exponent above 12.208, such as 12.5, would also do. The number 13 is
+chosen only because it is an integer.
+
+So the Flint-Hills question sits exactly in the gap. Theorem 7.4
+proves the 13th-power analogue with the methods available today;
+Theorem 7.3 would prove the actual question from an exponent bound
+that nobody has; and mu(pi) = 2 would give the bound, since 2 < 5/2.
+This is the honest reason the original document's Corollary 1 cannot
+be accepted: its proof of mu(pi) = 2 is the missing ingredient, and
+that ingredient is the open problem.
+
+7.5 Proposition (divergence half, unconditional). Fix a > 0 and
+b > 0. The series
+
+ sum over n >= 1 of 1 / ( n^a |sin n|^b )
+
+diverges in both of the following cases: a <= 1, and 1 < a <= b.
+
+Note that these two cases together are exactly a <= max(1, b).
+
+Proof, first case. If a <= 1 then |sin n| <= 1 gives
+
+ 1 / ( n^a |sin n|^b ) >= 1 / n^a >= 1 / n,
+
+whose sum diverges. Done for a <= 1.
+
+Proof, second case. Let p_j/q_j be the convergents of pi from
+section 4.1, with p_j and q_j positive integers tending to infinity.
+The defining property of a convergent gives
+
+ |pi - p_j/q_j| < 1 / q_j^2,
+
+so |p_j - pi q_j| < 1 / q_j. Since |sin x| <= |x| for all real x, and
+since sine is pi-periodic,
+
+ |sin p_j| = |sin(p_j - pi q_j)| <= |p_j - pi q_j| < 1/q_j.
+
+Raise to the power b and invert:
+
+ 1 / |sin p_j|^b > q_j^b.
+
+Also p_j/q_j tends to pi, so for all large j we have
+p_j <= (pi + 1) q_j, that is q_j >= p_j/(pi + 1), and therefore
+
+ 1 / ( p_j^a |sin p_j|^b )
+ > q_j^b / p_j^a
+ >= (pi + 1)^(-b) p_j^(b - a).
+
+If a < b the right side tends to infinity, and if a = b it is the
+fixed positive number (pi + 1)^(-b). In both cases the terms of the
+series do not tend to 0, so the series diverges. Done.
+
+7.6 Where that leaves the question.
+
+Put the two halves together for the classical shape b = 2. The
+series sum 1/(n^a sin^2 n) diverges for a <= 2 by Proposition 7.5,
+and converges for a > 12.208 by Theorem 7.4 with the record bound
+mu(pi) <= 7.104, since a > 2 * 7.104 - 2 is exactly what Lemma 7.2
+needs. So the state of knowledge is
+
+ a <= 2 diverges PROVED
+ 2 < a <= 12.208 undecided OPEN
+ a > 12.208 converges PROVED
+
+and the Flint-Hills series is the case a = 3, sitting inside the
+undecided window. The same computation with b in place of 2 gives
+convergence for a > 6.104 b when b >= 1, and for a > 1 - b + 6.104 b
+when 0 < b < 1, so the window shrinks as b shrinks.
+
+The window is not a defect of the method, it is the method. Its left
+wall would move to a = 3 exactly if we knew mu(pi) < 5/2, by Theorem
+7.3, and that is the entire content of the classical criterion: the
+series converges if the exponent of pi can be pushed below 5/2. The
+best published exponent is 7.1033. That is the whole story.
+
+
+8. RECAP
+--------
+
+In one page.
+
+Definitions. mu(x) is the largest mu such that |x - p/q| < q^(-mu)
+for infinitely many q. The identity |x - p/q| = ||q x|| / q turns
+this into a statement about how close multiples of x come to integers.
+
+What is proved here, completely.
+
+ 2.1 Every irrational x has mu(x) >= 2. Pigeonhole, two lines of
+ bookkeeping.
+
+ 3.1 mu(sqrt 2) = 2 exactly. Exponent 2 is attainable.
+
+ 5.1 Pi is irrational. Niven's integral, positive integer less
+ than 1.
+
+ 7.1 The Flint-Hills sum over n is at most a constant times the sum
+ over q of q^(-a) ||q pi||^(-b).
+
+ 7.2 If ||q pi|| >= c q^(1-nu0) for every q, then the q-series
+ converges for every a > 2 nu0 - 2.
+
+ 7.3 If mu(pi) < 5/2 then the Flint-Hills series converges.
+
+ 7.4 The series with 13 in place of 3 converges, unconditionally.
+
+ 7.5 The series diverges whenever a <= max(1, b).
+
+What is known from the literature, quoted not proved.
+
+ 6.2 mu(pi) <= 42 (Mahler 1953), 21 (Mignotte 1974),
+ 8.01604539... (Hata 1993), 7.606308... (Salikhov 2008),
+ 7.103205334137... (Zeilberger and Zudilin 2020).
+ 4.2 mu(x) = 2 for every irrational algebraic x (Roth 1955).
+ 1.4 mu(e) = 2 (Davis 1978).
+ 7.3 (the discussion, not the theorem) Convergence of the
+ Flint-Hills series forces mu(pi) <= 5/2 (Alekseyev 2011), and
+ Meiburg 2022 states the matching sufficient condition.
+
+What is open.
+
+ mu(pi) = 2. Equivalently, the continued fraction of pi has bounded
+ partial quotients. Equivalently for our purposes, pi cannot be
+ approximated by fractions better than q^(-2) infinitely often.
+
+ Convergence of sum 1/(n^3 sin^2 n). Since mu(pi) = 2 would give
+ mu(pi) < 5/2 and Theorem 7.3, this is open for the same reason and
+ no other.
+
+ The exact convergence threshold in the two-parameter family
+ sum 1/(n^a |sin n|^b): for b >= 1 everything with b < a <= 6.104 b
+ is undecided, and for 0 < b < 1 everything with
+ 1 < a <= 1 - b + 6.104 b is undecided.
+
+The single number to remember is 7.103205334137. It is the best
+upper bound for mu(pi) that humanity has, it was proved in 2020,
+and the conjecture is that the truth is 2.
+
+
+9. WHY THIS FILE IS NOT THE ORIGINAL
+------------------------------------
+
+The original file was a LaTeX bundle of five sections proving, in its
+own words, "the conjecture that the irrationality exponent of pi is
+2". Its structure was: a weighted interpolation theorem on algebraic
+curves, a determinant, an arithmetic lower bound, an analytic upper
+bound, and a parameter choice. Nobody can check that in an afternoon,
+and its own introduction concedes the state of the art is 7.1033.
+
+A proof of mu(pi) = 2 would be a landmark: it would give, all at once,
+bounded partial quotients for pi, convergence of the Flint-Hills
+series, and the exact threshold in the generalised family. That is
+not the kind of result that arrives inside one document with no
+external check. So this file keeps the parts that are true and
+provable in full, states the parts that are quoted with their sources,
+and labels the rest open.
+
+The consequence is a document that proves less than the original
+claimed and asserts nothing it cannot back up. For a reader in high
+school the difference matters: the two lemmas of section 7 and the
+integral of section 5 are real mathematics that can be checked, and
+the fact that mu(pi) = 2 is open is itself worth knowing, because it
+is a live question, not a settled one.
+
+ -- end of file --