BA0024

cf_approximation_unimodular_best_approximation

Complete signed-numerator comparison from a genuine unimodular pair and its opposite decreasing errors; these premises still need the actual continued-fraction alignment theorem.

Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable

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.

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.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ u. ∀ U. ∀ v. ∀ V. ∀ E. ∀ F. ∀ rp. ∀ rn. ∀ t. ∀ D. u · V + 1 = U · v ∨ U · v + 1 = u · V → a · v = b · u + E ∧ b · U = a · V + F ∨ b · u = a · v + E ∧ a · V = b · U + F → Le(E,F) → ¬t = 0 → Lt(t,v) → RationalApproximationError(a,b,rp,rn,t,D) → Le(E,D)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

RationalApproximationError(a,b,rp,rn,t,E) · 1Le(a,b) · 2Lt(a,b) · 1

Actual proof prerequisites

cf_approximation_small_denominator_signed_coordinatescf_approximation_subtractive_error_lower_boundcf_approximation_errors_exchange_columnsle_trans · checked external prerequisite
Original expanded first-order statement 
forall a b u U v V E F rp rn t D. (u * V + 1 = U * v \/ U * v + 1 = u * V) -> (((a * v = b * u + E) /\ (b * U = a * V + F)) \/ ((b * u = a * v + E) /\ (a * V = b * U + F))) -> (exists cfba_bound_comparison_errors. cfba_bound_comparison_errors + (E) = (F)) -> ~(t = 0) -> (exists cfba_gap_comparison_denominator. cfba_gap_comparison_denominator + S (t) = (v)) -> (((a * t + b * rn) = (b * rp) + (D)) \/ ((b * rp) = (a * t + b * rn) + (D))) -> (exists cfba_bound_comparison_result. cfba_bound_comparison_result + (E) = (D))

Complete tactic proof in conservative notation

All 87 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

87 script commands · 12 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
cf approximation small denominator signed coordinatescf approximation subtractive error lower boundcf approximation errors exchange columns
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro u
  4. L4
    intro U
  5. L5
    intro v
  6. L6
    intro V
  7. L7
    intro E
  8. L8
    intro F
  9. L9
    intro rp
  10. L10
    intro rn
02Fix variables and assumptionsL11–18

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro t
  2. L12
    intro D
  3. L13
    intro hd
  4. L14
    intro he
  5. L15
    intro hEF
  6. L16
    intro ht
  7. L17
    intro hlt
  8. L18
    intro herror
03Establish hcL19–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf approximation small denominator signed coordinates.

  1. L19
    have hc : exists c d. ((((~(c = 0)) /\ ((((rp) + (d) * (U) = (rn) + (c) * (u)) /\ ((t) + (d) * (V) = (0) + (c) * (v)))))) \/ (((~(d = 0)) /\ ((((rp) + (c) * (u) = (rn) + (d) * (U)) /\ ((t) + (c) * (v) = (0) + (d) * (V)))))))
  2. L20
    specialize cf_approximation_small_denominator_signed_coordinates (u)
  3. L21
    specialize cf_approximation_small_denominator_signed_coordinates (U)
  4. L22
    specialize cf_approximation_small_denominator_signed_coordinates (v)
  5. L23
    specialize cf_approximation_small_denominator_signed_coordinates (V)
  6. L24
    specialize cf_approximation_small_denominator_signed_coordinates (rp)
  7. L25
    specialize cf_approximation_small_denominator_signed_coordinates (rn)
  8. L26
    specialize cf_approximation_small_denominator_signed_coordinates (t)
  9. L27
    apply cf_approximation_small_denominator_signed_coordinates
  10. L28
    exact hd
04Use earlier factsL29–30

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L29
    exact ht
  2. L30
    exact hlt
05Separate the logical casesL31–34

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L31
    cases hc
  2. L32
    cases hc_witness
  3. L33
    cases hc_witness_witness
  4. L34
    cases hc_witness_witness_left
06Use earlier factsL35–44

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L35
    specialize cf_approximation_subtractive_error_lower_bound (a)
  2. L36
    specialize cf_approximation_subtractive_error_lower_bound (b)
  3. L37
    specialize cf_approximation_subtractive_error_lower_bound (u)
  4. L38
    specialize cf_approximation_subtractive_error_lower_bound (U)
  5. L39
    specialize cf_approximation_subtractive_error_lower_bound (v)
  6. L40
    specialize cf_approximation_subtractive_error_lower_bound (V)
  7. L41
    specialize cf_approximation_subtractive_error_lower_bound (E)
  8. L42
    specialize cf_approximation_subtractive_error_lower_bound (F)
  9. L43
    specialize cf_approximation_subtractive_error_lower_bound (rp)
  10. L44
    specialize cf_approximation_subtractive_error_lower_bound (rn)
07Use earlier factsL45–53

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L45
    specialize cf_approximation_subtractive_error_lower_bound (t)
  2. L46
    specialize cf_approximation_subtractive_error_lower_bound (D)
  3. L47
    specialize cf_approximation_subtractive_error_lower_bound (x)
  4. L48
    specialize cf_approximation_subtractive_error_lower_bound (x1)
  5. L49
    apply cf_approximation_subtractive_error_lower_bound
  6. L50
    exact he
  7. L51
    exact hc_witness_witness_left_right
  8. L52
    exact hc_witness_witness_left_left
  9. L53
    exact herror
08Separate the logical casesL54–54

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L54
    cases hc_witness_witness_right
09Use earlier factsL55–64

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L55
    specialize le_trans (E)
  2. L56
    specialize le_trans (F)
  3. L57
    specialize le_trans (D)
  4. L58
    apply le_trans
  5. L59
    exact hEF
  6. L60
    specialize cf_approximation_subtractive_error_lower_bound (a)
  7. L61
    specialize cf_approximation_subtractive_error_lower_bound (b)
  8. L62
    specialize cf_approximation_subtractive_error_lower_bound (U)
  9. L63
    specialize cf_approximation_subtractive_error_lower_bound (u)
  10. L64
    specialize cf_approximation_subtractive_error_lower_bound (V)
10Use earlier factsL65–74

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L65
    specialize cf_approximation_subtractive_error_lower_bound (v)
  2. L66
    specialize cf_approximation_subtractive_error_lower_bound (F)
  3. L67
    specialize cf_approximation_subtractive_error_lower_bound (E)
  4. L68
    specialize cf_approximation_subtractive_error_lower_bound (rp)
  5. L69
    specialize cf_approximation_subtractive_error_lower_bound (rn)
  6. L70
    specialize cf_approximation_subtractive_error_lower_bound (t)
  7. L71
    specialize cf_approximation_subtractive_error_lower_bound (D)
  8. L72
    specialize cf_approximation_subtractive_error_lower_bound (x1)
  9. L73
    specialize cf_approximation_subtractive_error_lower_bound (x)
  10. L74
    apply cf_approximation_subtractive_error_lower_bound
11Use earlier factsL75–84

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L75
    specialize cf_approximation_errors_exchange_columns (a)
  2. L76
    specialize cf_approximation_errors_exchange_columns (b)
  3. L77
    specialize cf_approximation_errors_exchange_columns (u)
  4. L78
    specialize cf_approximation_errors_exchange_columns (U)
  5. L79
    specialize cf_approximation_errors_exchange_columns (v)
  6. L80
    specialize cf_approximation_errors_exchange_columns (V)
  7. L81
    specialize cf_approximation_errors_exchange_columns (E)
  8. L82
    specialize cf_approximation_errors_exchange_columns (F)
  9. L83
    apply cf_approximation_errors_exchange_columns
  10. L84
    exact he
12Use earlier factsL85–87

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L85
    exact hc_witness_witness_right_right
  2. L86
    exact hc_witness_witness_right_left
  3. L87
    exact herror

Library-wide reading audit

Original defined command ledger · 87 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro u
  4. 0004intro U
  5. 0005intro v
  6. 0006intro V
  7. 0007intro E
  8. 0008intro F
  9. 0009intro rp
  10. 0010intro rn
  11. 0011intro t
  12. 0012intro D
  13. 0013intro hd
  14. 0014intro he
  15. 0015intro hEF
  16. 0016intro ht
  17. 0017intro hlt
  18. 0018intro herror
  19. 0019have hc : exists c d. ((((~(c = 0)) /\ ((((rp) + (d) * (U) = (rn) + (c) * (u)) /\ ((t) + (d) * (V) = (0) + (c) * (v)))))) \/ (((~(d = 0)) /\ ((((rp) + (c) * (u) = (rn) + (d) * (U)) /\ ((t) + (c) * (v) = (0) + (d) * (V)))))))
  20. 0020specialize cf_approximation_small_denominator_signed_coordinates (u)
  21. 0021specialize cf_approximation_small_denominator_signed_coordinates (U)
  22. 0022specialize cf_approximation_small_denominator_signed_coordinates (v)
  23. 0023specialize cf_approximation_small_denominator_signed_coordinates (V)
  24. 0024specialize cf_approximation_small_denominator_signed_coordinates (rp)
  25. 0025specialize cf_approximation_small_denominator_signed_coordinates (rn)
  26. 0026specialize cf_approximation_small_denominator_signed_coordinates (t)
  27. 0027apply cf_approximation_small_denominator_signed_coordinates
  28. 0028exact hd
  29. 0029exact ht
  30. 0030exact hlt
  31. 0031cases hc
  32. 0032cases hc_witness
  33. 0033cases hc_witness_witness
  34. 0034cases hc_witness_witness_left
  35. 0035specialize cf_approximation_subtractive_error_lower_bound (a)
  36. 0036specialize cf_approximation_subtractive_error_lower_bound (b)
  37. 0037specialize cf_approximation_subtractive_error_lower_bound (u)
  38. 0038specialize cf_approximation_subtractive_error_lower_bound (U)
  39. 0039specialize cf_approximation_subtractive_error_lower_bound (v)
  40. 0040specialize cf_approximation_subtractive_error_lower_bound (V)
  41. 0041specialize cf_approximation_subtractive_error_lower_bound (E)
  42. 0042specialize cf_approximation_subtractive_error_lower_bound (F)
  43. 0043specialize cf_approximation_subtractive_error_lower_bound (rp)
  44. 0044specialize cf_approximation_subtractive_error_lower_bound (rn)
  45. 0045specialize cf_approximation_subtractive_error_lower_bound (t)
  46. 0046specialize cf_approximation_subtractive_error_lower_bound (D)
  47. 0047specialize cf_approximation_subtractive_error_lower_bound (x)
  48. 0048specialize cf_approximation_subtractive_error_lower_bound (x1)
  49. 0049apply cf_approximation_subtractive_error_lower_bound
  50. 0050exact he
  51. 0051exact hc_witness_witness_left_right
  52. 0052exact hc_witness_witness_left_left
  53. 0053exact herror
  54. 0054cases hc_witness_witness_right
  55. 0055specialize le_trans (E)
  56. 0056specialize le_trans (F)
  57. 0057specialize le_trans (D)
  58. 0058apply le_trans
  59. 0059exact hEF
  60. 0060specialize cf_approximation_subtractive_error_lower_bound (a)
  61. 0061specialize cf_approximation_subtractive_error_lower_bound (b)
  62. 0062specialize cf_approximation_subtractive_error_lower_bound (U)
  63. 0063specialize cf_approximation_subtractive_error_lower_bound (u)
  64. 0064specialize cf_approximation_subtractive_error_lower_bound (V)
  65. 0065specialize cf_approximation_subtractive_error_lower_bound (v)
  66. 0066specialize cf_approximation_subtractive_error_lower_bound (F)
  67. 0067specialize cf_approximation_subtractive_error_lower_bound (E)
  68. 0068specialize cf_approximation_subtractive_error_lower_bound (rp)
  69. 0069specialize cf_approximation_subtractive_error_lower_bound (rn)
  70. 0070specialize cf_approximation_subtractive_error_lower_bound (t)
  71. 0071specialize cf_approximation_subtractive_error_lower_bound (D)
  72. 0072specialize cf_approximation_subtractive_error_lower_bound (x1)
  73. 0073specialize cf_approximation_subtractive_error_lower_bound (x)
  74. 0074apply cf_approximation_subtractive_error_lower_bound
  75. 0075specialize cf_approximation_errors_exchange_columns (a)
  76. 0076specialize cf_approximation_errors_exchange_columns (b)
  77. 0077specialize cf_approximation_errors_exchange_columns (u)
  78. 0078specialize cf_approximation_errors_exchange_columns (U)
  79. 0079specialize cf_approximation_errors_exchange_columns (v)
  80. 0080specialize cf_approximation_errors_exchange_columns (V)
  81. 0081specialize cf_approximation_errors_exchange_columns (E)
  82. 0082specialize cf_approximation_errors_exchange_columns (F)
  83. 0083apply cf_approximation_errors_exchange_columns
  84. 0084exact he
  85. 0085exact hc_witness_witness_right_right
  86. 0086exact hc_witness_witness_right_left
  87. 0087exact herror