How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Regular Continued Fractions and Diophantine Approximation — Examples
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Foundations of the Real Numbers for Analysis
- Regular Continued Fractions and Diophantine Approximation
- Relations, Functions, and Quotients
- The ZFC Axioms and the Basic Set Constructions
2 · Summary
These worked examples keep the abstract statements concrete. They show the two finite expansions of a rational, the Euclidean-algorithm origin of the digits, the periodic expansions of familiar quadratic irrationals, and the way the approximation theorems control explicit rational approximants.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
A rational number has exactly two finite regular continued-fraction expansions
Example
The rational number has the two finite regular continued-fraction expansions and the normalized one is because its last digit is at least .
Facts & Assumptions
Given: The rational number .
Every rational number has a unique normalized finite regular continued fraction, and exactly one other finite expansion obtained by splitting the last digit into (Normalized finite regular continued fractions are unique).
Verification
Direct calculation gives. [given, algebra]
Likewise. [F1, step 1.1, algebra] so the same rational has two finite expansions. The last digit of is , so [F1] identifies it as the normalized one and shows there are no further finite expansions.
The continued fraction of 37/11 matches Euclid and Bezout
Example
For , the Euclidean divisions give the continued fraction and the penultimate convergents encode the Bezout relation
Facts & Assumptions
Given: The integers and .
For a rational number, the continued-fraction algorithm terminates and its digits are exactly the Euclidean quotient digits (The continued-fraction algorithm terminates exactly on rational numbers).
Bezout's identity characterizes as an integer linear combination of and (Bézout's identity: for integers not both zero, is the least positive element of ; in particular has an integer solution).
Verification
The Euclidean quotient digits are , so [F1] gives. [F1, given, algebra] Its convergents are
The penultimate convergent is , and. [F2, step 1.1, algebra] So is an explicit integer linear combination of and , which is exactly the Bezout identity for in the sense of [F2].
The continued fraction [1; overline 2] for sqrt(2)
Example
The continued fraction of is with convergents
Facts & Assumptions
Given: The real number .
Consecutive convergents satisfy (Determinant identity for consecutive convergents).
For an irrational number , the convergents alternate around and satisfy (Convergent error bound).
The complete-quotient algorithm chooses the unique integer part and then takes the reciprocal of the positive fractional part (Complete quotients in the continued-fraction algorithm).
If the complete-quotient algorithm does not terminate, its resulting infinite regular continued fraction converges to the original real number (The continued-fraction algorithm for real numbers).
For digits , the convergent numerators and denominators start from and satisfy and (Convergents of a regular continued fraction).
Verification
Since , [F3] gives . Then [F3, F4, given, algebra] so and . Moreover so every later complete quotient is again . Thus the algorithm never terminates and produces the digits ; by [F4] its continued fraction converges to the original number. Hence
Applying [F5] to the digits from step 1.1 gives [F5, step 1.1, algebra] so the convergents begin The same recurrence gives . For the displayed pairs one checks exactly as [F1] predicts.
The error formula [F2] now gives [F2, step 2.1, algebra] and similarly So the concrete convergents alternate around with the expected quality of approximation.
The continued fraction [3; overline 1,2,1,6] for sqrt(14)
Example
The complete quotients of cycle through the states so
Facts & Assumptions
Given: The real number .
The continued-fraction algorithm is deterministic: each complete quotient determines the digit and, when , the next complete quotient (Complete quotients in the continued-fraction algorithm).
Verification
Since , the first digit is . Then [given, algebra] and finally So the digits from onward are and then repeat.
Step 1.1 shows that . By the determinism in [F1], the same four digits therefore repeat from onward. Hence
The continued fraction [1; overline 1] for the golden ratio
Example
If then so is the positive root of , namely the golden ratio
Facts & Assumptions
Given: The purely periodic continued fraction .
Every eventually periodic regular continued fraction has quadratic- irrational value (Eventually periodic regular continued fractions are quadratic irrationals).
The value of an infinite regular continued fraction is the common limit of its convergents; for the increasing even subsequence starts at (Every infinite regular continued fraction converges to a unique real number).
Finite regular continued fractions are evaluated by the recursion (Finite and infinite regular continued fractions).
Verification
Let . By [F2], and , while [F3] gives and . Hence so taking limits in the recursion gives Multiplication by now gives whose positive solution is
The continued fraction is purely periodic, so [F1] says its value is a quadratic irrational. Step 1.1 exhibits the quadratic equation explicitly, and its positive root is the golden ratio .
The fractions 22/7, 333/106, and 355/113 as approximations to pi
Example
Among the classical fractions the best approximation to is , and it is already forced by Legendre's criterion.
Facts & Assumptions
Given: The real number and the three rational numbers above.
The number is irrational (Ivan Niven, "A simple proof that pi is irrational", Bulletin of the AMS 53 (1947), 509).
If is irrational and a reduced rational number satisfies , then it is a convergent of (Legendre's criterion for convergents).
A convergent of an irrational number is the best approximation among all rationals with smaller next denominator (Convergents are best rational approximations of the first kind).
Verification
Direct decimal comparison gives. [given, algebra] Moreover and , so . Thus is reduced and satisfies Legendre's criterion.
By [L1] and [F1], the fraction is a convergent of . Then [F2] says no. [L1, F1, F2, step 1.1] rational with denominator at most approximates more closely. Since and have denominators and , neither can beat .
The direct errors from step 1.1 also show that improves on. [step 1.1, algebra] , but that both are far worse than .
The constant 1/2 in Legendre's criterion cannot be replaced by 3/4
Statement refuted
For every irrational real number and every reduced rational number with , implies that is a convergent of .
Facts & Assumptions
Given: The irrational number and the rational number .
Legendre's criterion with the sharp constant says that forces to be a convergent (Legendre's criterion for convergents).
Convergents of an irrational satisfy the standard error bound (Convergent error bound).
Counterexample
The first few convergents of are. [given, algebra] so is not a convergent of .
Nevertheless. [given, algebra] Thus satisfies the displayed bound.
Step 1.1 and step 1.2 together refute the statement. In the light of [F1],. [F1, F2, step 1.1, step 1.2] this shows that the sharp constant in Legendre's criterion cannot simply be replaced by the larger constant .
A negative irrational has a regular continued fraction with positive later digits
Example
For the negative irrational , the continued-fraction algorithm gives The only negative digit is the initial one; every later digit is positive.
Facts & Assumptions
Given: The real number .
The complete-quotient algorithm chooses the unique integer part with , and whenever the next complete quotient exists it is (Complete quotients in the continued-fraction algorithm).
The continued-fraction algorithm reconstructs the original real number from its digits (The continued-fraction algorithm for real numbers).
Verification
Since , the first digit is . Then. [F1, given, algebra] so and .
One more step gives. [F1, F2, step 1.1, algebra] so every later digit is . Hence the digit string is and [F2] identifies its value with . In particular the negative sign is absorbed entirely into the first digit, while every later digit stays positive as required by [F1].