Continued fractions — flashcards

The number of division steps in the Euclidean algorithm is at most five times the number of decimal digits of the smaller argument; the worst case is consecutive Fibonacci numbers.

Anthyphairesis on a 1 by √2 rectangle never terminates, which is exactly the statement that √2 is not a ratio of integers.

Every convergent of the continued fraction of x is a best rational approximation of the second kind, and every such approximation is a convergent.

Asking what an irrational f means for the Chord(f) construction splits into two genuinely different questions, not one. (1) The value: for algebraic irrational f, the Gelfond–Schneider theorem characterizes Chord(f)=2sin(fπ) as transcendental. (2) The configuration: N points at an irrational rotation α (rather than N-th roots of unity) obey the three-distance theorem (Steinhaus) — at most three distinct gap lengths between consecutive points on the circle at any N, collapsing to exactly two precisely at the continued-fraction convergents of α. Verified directly for the golden ratio (whose continued fraction is all 1s): exactly two gap lengths at each Fibonacci count N=3,5,8,13,21,34.

Gabriel Lamé, 1844.

the Pythagorean school, c. 450 BC.

Joseph-Louis Lagrange, 1770.

irrational_sqrt_two — Mathlib.NumberTheory.Real.Irrational

GenContFract.convs — Mathlib.Algebra.ContinuedFractions.Basic

The continued fraction of x is the quotient sequence of the Euclidean algorithm run on x. Identical work; the CF keeps only the quotients and discards the remainders, which is exactly where the magnitude information lived.

Two representations that each throw away the same thing. Neither lets you read off how big a number is from a prefix of its expansion — the ordering information is simply not in the encoding.

An apparent fork that collapsed. Letting the root vary at each stage looks like a new family, but every canonical version is continued fractions conjugated by a logarithm — and the base of that logarithm turns out to be irrelevant, even numerically. Testing whether a fork is real is half the work of this lens.

Recorded as apparent: the resemblance is real, the mechanism is not shared.

A continued fraction is the run-length encoding of a geodesic — the forward itinerary of the Gauss map. The digits stop being digits and become a record of where a point went.

Euclid's algorithm consumes a pair and reduces it; the continued fraction it produces generates approximations outward. The same recursion read as destruction or as construction depending on which end you stand at.

Proposed cost that was not one. Both discard something about distance, but not the same something: p-adic expansions are positional and linear, continued fractions relative and recursive. The refutation forced a distinction worth more than the conjecture.

Recorded as refuted: this edge was drawn and then withdrawn.

Tested directly: nested radicals do have a series dual, via difference-of-squares telescoping, echoing continued fractions' own series representation. The pairing is real, but it isn't the same shape — it comes out all-positive rather than alternating, which is exactly what breaks optimality for nested radicals. A confirmed analogy that differs in a load-bearing way from the thing it was tested against.

`Mathlib.Algebra.ContinuedFractions.Basic` imports `Mathlib.Algebra.Field.Defs`. Read off Mathlib/Algebra/ContinuedFractions/Basic.html. No human asserted this edge.

Write a number as an integer plus one over an integer plus one over… Unlike decimal it has no fixed alphabet, which is what buys it base-independence and best-approximation.