Actual quotient traces · determinant identities · signed competitors · Constructive arithmetic

Convergents and best approximation

ContinuedFraction(a,b,s) ∧ Convergent(s,i,u,v) ⇒ |av−bu|≤|at−br| whenever 0<t<v

Compute every convergent from the finite quotient history and prove best approximation of the second kind.

Open the definition-aware map Read the final theorem See campaign milestone G072

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact certificate

Fully expanded arithmetic

Inspect all 4003 native tactic lines and 247 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem BA0053 and follow only the lemmas and conservative definitions supporting continued_fraction_convergent_best_approximation.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G072 milestone → theorem and definition dependencies.
Major independently established statements: BA0046 continued_fraction_initial_zero_over_one · BA004D continued_fraction_convergent_exists_unique_at_history_index · BA0050 continued_fraction_adjacent_convergent_determinant · BA0051 continued_fraction_convergent_coprime · BA004A continued_fraction_has_exact_terminal_convergent · BA0052 continued_fraction_convergent_best_approximation_signed · BA0053 continued_fraction_convergent_best_approximation.
Independently verified Alpha v34 checked-use theorem family: 83 dependency-curried kernel-checked theorem bodies · 247 proof prerequisites · 18 linked definitions · 21 definition-dependency arrows · 4003 exact tactic lines · first admitted v29 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 566 bundle nodes; SHA-256 4fcb3cd45e83448776abb9e33692496a7acfa98a051cae15761826a0b15fda44.
Exact mathematical boundary: The initial 0/1 convergent is included: u is natural, not necessarily positive. Comparison denominators are strictly smaller and positive. Signed competitors are represented by an arbitrary difference rp−rn. Approximation inequalities are proved from the trace, never stored as assumptions in Convergent.