BA0021

cf_approximation_small_denominator_signed_coordinates

Every candidate with positive denominator below the current one lies in one of the two opposite-sign coordinate sectors; no sign case is omitted.

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

∀ u. ∀ U. ∀ v. ∀ V. ∀ rp. ∀ rn. ∀ t. u · V + 1 = U · v ∨ U · v + 1 = u · V → ¬t = 0 → Lt(t,v) → ∃ x. ∃ y. ¬x = 0 ∧ (rp + y · U = rn + x · u ∧ t + y · V = 0 + x · v) ∨ ¬y = 0 ∧ (rp + x · u = rn + y · U ∧ t + x · v = 0 + y · V)

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

Definition DAG

Lt(a,b) · 1

Actual proof prerequisites

cf_approximation_unimodular_signed_basiscf_approximation_small_positive_sum_current_zerocf_approximation_positive_difference_coefficient_nonzerocf_approximation_zero_current_sum_as_differenceadd_eq_zero_left · checked external prerequisite
Original expanded first-order statement 
forall u U v V rp rn t. (u * V + 1 = U * v \/ U * v + 1 = u * V) -> ~(t = 0) -> (exists cfba_gap_small_denominator. cfba_gap_small_denominator + S (t) = (v)) -> 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)))))))

Complete tactic proof in conservative notation

All 103 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

103 script commands · 23 reading checkpoints · 3 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 (4)
cf approximation unimodular signed basiscf approximation small positive sum current zerocf approximation zero current sum as differencecf approximation positive difference coefficient nonzero
01Fix variables and assumptionsL1–10

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

  1. L1
    intro u
  2. L2
    intro U
  3. L3
    intro v
  4. L4
    intro V
  5. L5
    intro rp
  6. L6
    intro rn
  7. L7
    intro t
  8. L8
    intro hd
  9. L9
    intro ht
  10. L10
    intro hlt
02Establish hbL11–20

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

  1. L11
    have hb : exists c d. (((((rp) = (rn) + ((c) * (u) + (d) * (U))) /\ ((t) = (0) + ((c) * (v) + (d) * (V))))) \/ (((((rp) + (d) * (U) = (rn) + (c) * (u)) /\ ((t) + (d) * (V) = (0) + (c) * (v)))) \/ (((((rp) + (c) * (u) = (rn) + (d) * (U)) /\ ((t) + (c) * (v) = (0) + (d) * (V)))) \/ ((((rp) + ((c) * (u) + (d) * (U)) = (rn)) /\ ((t) + ((c) * (v) + (d) * (V)) = (0)))))))
  2. L12
    specialize cf_approximation_unimodular_signed_basis (u)
  3. L13
    specialize cf_approximation_unimodular_signed_basis (U)
  4. L14
    specialize cf_approximation_unimodular_signed_basis (v)
  5. L15
    specialize cf_approximation_unimodular_signed_basis (V)
  6. L16
    specialize cf_approximation_unimodular_signed_basis (rp)
  7. L17
    specialize cf_approximation_unimodular_signed_basis (rn)
  8. L18
    specialize cf_approximation_unimodular_signed_basis (t)
  9. L19
    apply cf_approximation_unimodular_signed_basis
  10. L20
    exact hd
03Separate the logical casesL21–24

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

  1. L21
    cases hb
  2. L22
    cases hb_witness
  3. L23
    cases hb_witness_witness
  4. L24
    cases hb_witness_witness_left
04Establish hcL25–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf approximation small positive sum current zero.

  1. L25
    have hc : x = 0
  2. L26
    specialize cf_approximation_small_positive_sum_current_zero (t)
  3. L27
    specialize cf_approximation_small_positive_sum_current_zero (v)
  4. L28
    specialize cf_approximation_small_positive_sum_current_zero (V)
  5. L29
    specialize cf_approximation_small_positive_sum_current_zero (x)
  6. L30
    specialize cf_approximation_small_positive_sum_current_zero (x1)
  7. L31
    apply cf_approximation_small_positive_sum_current_zero
  8. L32
    exact hb_witness_witness_left_right
  9. L33
    exact hlt
05Establish hnL34–43

Establish this local claim before using it. It is not an additional assumption.

  1. L34
    have hn : (((rp) + (0) * (u) = (rn) + (x1) * (U)) /\ ((t) + (0) * (v) = (0) + (x1) * (V)))
  2. L35
    specialize cf_approximation_zero_current_sum_as_difference (u)
  3. L36
    specialize cf_approximation_zero_current_sum_as_difference (U)
  4. L37
    specialize cf_approximation_zero_current_sum_as_difference (v)
  5. L38
    specialize cf_approximation_zero_current_sum_as_difference (V)
  6. L39
    specialize cf_approximation_zero_current_sum_as_difference (rp)
  7. L40
    specialize cf_approximation_zero_current_sum_as_difference (rn)
  8. L41
    specialize cf_approximation_zero_current_sum_as_difference (t)
  9. L42
    specialize cf_approximation_zero_current_sum_as_difference (x)
  10. L43
    specialize cf_approximation_zero_current_sum_as_difference (x1)
06Use earlier factsL44–46

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

  1. L44
    apply cf_approximation_zero_current_sum_as_difference
  2. L45
    exact hb_witness_witness_left
  3. L46
    exact hc
07Separate the logical casesL47–47

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

  1. L47
    cases hn
08Construct an explicit witnessL48–49

Supply the displayed value, then prove that it has the required property.

  1. L48
    exists 0
  2. L49
    exists x1
09Separate the logical casesL50–51

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

  1. L50
    right
  2. L51
    split
10Fix variables and assumptionsL52–52

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

  1. L52
    intro hzero
11Use earlier factsL53–62

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

  1. L53
    specialize cf_approximation_positive_difference_coefficient_nonzero (t)
  2. L54
    specialize cf_approximation_positive_difference_coefficient_nonzero (V)
  3. L55
    specialize cf_approximation_positive_difference_coefficient_nonzero (v)
  4. L56
    specialize cf_approximation_positive_difference_coefficient_nonzero (x1)
  5. L57
    specialize cf_approximation_positive_difference_coefficient_nonzero (0)
  6. L58
    apply cf_approximation_positive_difference_coefficient_nonzero
  7. L59
    exact ht
  8. L60
    exact hn_right
  9. L61
    exact hzero
  10. L62
    exact hn
12Separate the logical casesL63–64

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

  1. L63
    cases hb_witness_witness_right
  2. L64
    cases hb_witness_witness_right_left
13Construct an explicit witnessL65–66

Supply the displayed value, then prove that it has the required property.

  1. L65
    exists x
  2. L66
    exists x1
14Separate the logical casesL67–68

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

  1. L67
    left
  2. L68
    split
15Fix variables and assumptionsL69–69

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

  1. L69
    intro hzero
16Use earlier factsL70–79

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

  1. L70
    specialize cf_approximation_positive_difference_coefficient_nonzero (t)
  2. L71
    specialize cf_approximation_positive_difference_coefficient_nonzero (v)
  3. L72
    specialize cf_approximation_positive_difference_coefficient_nonzero (V)
  4. L73
    specialize cf_approximation_positive_difference_coefficient_nonzero (x)
  5. L74
    specialize cf_approximation_positive_difference_coefficient_nonzero (x1)
  6. L75
    apply cf_approximation_positive_difference_coefficient_nonzero
  7. L76
    exact ht
  8. L77
    exact hb_witness_witness_right_left_right
  9. L78
    exact hzero
  10. L79
    exact hb_witness_witness_right_left
17Separate the logical casesL80–81

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

  1. L80
    cases hb_witness_witness_right_right
  2. L81
    cases hb_witness_witness_right_right_left
18Construct an explicit witnessL82–83

Supply the displayed value, then prove that it has the required property.

  1. L82
    exists x
  2. L83
    exists x1
19Separate the logical casesL84–85

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

  1. L84
    right
  2. L85
    split
20Fix variables and assumptionsL86–86

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

  1. L86
    intro hzero
21Use earlier factsL87–96

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

  1. L87
    specialize cf_approximation_positive_difference_coefficient_nonzero (t)
  2. L88
    specialize cf_approximation_positive_difference_coefficient_nonzero (V)
  3. L89
    specialize cf_approximation_positive_difference_coefficient_nonzero (v)
  4. L90
    specialize cf_approximation_positive_difference_coefficient_nonzero (x1)
  5. L91
    specialize cf_approximation_positive_difference_coefficient_nonzero (x)
  6. L92
    apply cf_approximation_positive_difference_coefficient_nonzero
  7. L93
    exact ht
  8. L94
    exact hb_witness_witness_right_right_left_right
  9. L95
    exact hzero
  10. L96
    exact hb_witness_witness_right_right_left
22Separate the logical casesL97–98

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

  1. L97
    cases hb_witness_witness_right_right_right
  2. L98
    exfalso
23Use earlier factsL99–103

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

  1. L99
    apply ht
  2. L100
    specialize add_eq_zero_left (t)
  3. L101
    specialize add_eq_zero_left (x * v + x1 * V)
  4. L102
    apply add_eq_zero_left
  5. L103
    exact hb_witness_witness_right_right_right_right

Library-wide reading audit

Original defined command ledger · 103 lines
  1. 0001intro u
  2. 0002intro U
  3. 0003intro v
  4. 0004intro V
  5. 0005intro rp
  6. 0006intro rn
  7. 0007intro t
  8. 0008intro hd
  9. 0009intro ht
  10. 0010intro hlt
  11. 0011have hb : exists c d. (((((rp) = (rn) + ((c) * (u) + (d) * (U))) /\ ((t) = (0) + ((c) * (v) + (d) * (V))))) \/ (((((rp) + (d) * (U) = (rn) + (c) * (u)) /\ ((t) + (d) * (V) = (0) + (c) * (v)))) \/ (((((rp) + (c) * (u) = (rn) + (d) * (U)) /\ ((t) + (c) * (v) = (0) + (d) * (V)))) \/ ((((rp) + ((c) * (u) + (d) * (U)) = (rn)) /\ ((t) + ((c) * (v) + (d) * (V)) = (0)))))))
  12. 0012specialize cf_approximation_unimodular_signed_basis (u)
  13. 0013specialize cf_approximation_unimodular_signed_basis (U)
  14. 0014specialize cf_approximation_unimodular_signed_basis (v)
  15. 0015specialize cf_approximation_unimodular_signed_basis (V)
  16. 0016specialize cf_approximation_unimodular_signed_basis (rp)
  17. 0017specialize cf_approximation_unimodular_signed_basis (rn)
  18. 0018specialize cf_approximation_unimodular_signed_basis (t)
  19. 0019apply cf_approximation_unimodular_signed_basis
  20. 0020exact hd
  21. 0021cases hb
  22. 0022cases hb_witness
  23. 0023cases hb_witness_witness
  24. 0024cases hb_witness_witness_left
  25. 0025have hc : x = 0
  26. 0026specialize cf_approximation_small_positive_sum_current_zero (t)
  27. 0027specialize cf_approximation_small_positive_sum_current_zero (v)
  28. 0028specialize cf_approximation_small_positive_sum_current_zero (V)
  29. 0029specialize cf_approximation_small_positive_sum_current_zero (x)
  30. 0030specialize cf_approximation_small_positive_sum_current_zero (x1)
  31. 0031apply cf_approximation_small_positive_sum_current_zero
  32. 0032exact hb_witness_witness_left_right
  33. 0033exact hlt
  34. 0034have hn : (((rp) + (0) * (u) = (rn) + (x1) * (U)) /\ ((t) + (0) * (v) = (0) + (x1) * (V)))
  35. 0035specialize cf_approximation_zero_current_sum_as_difference (u)
  36. 0036specialize cf_approximation_zero_current_sum_as_difference (U)
  37. 0037specialize cf_approximation_zero_current_sum_as_difference (v)
  38. 0038specialize cf_approximation_zero_current_sum_as_difference (V)
  39. 0039specialize cf_approximation_zero_current_sum_as_difference (rp)
  40. 0040specialize cf_approximation_zero_current_sum_as_difference (rn)
  41. 0041specialize cf_approximation_zero_current_sum_as_difference (t)
  42. 0042specialize cf_approximation_zero_current_sum_as_difference (x)
  43. 0043specialize cf_approximation_zero_current_sum_as_difference (x1)
  44. 0044apply cf_approximation_zero_current_sum_as_difference
  45. 0045exact hb_witness_witness_left
  46. 0046exact hc
  47. 0047cases hn
  48. 0048exists 0
  49. 0049exists x1
  50. 0050right
  51. 0051split
  52. 0052intro hzero
  53. 0053specialize cf_approximation_positive_difference_coefficient_nonzero (t)
  54. 0054specialize cf_approximation_positive_difference_coefficient_nonzero (V)
  55. 0055specialize cf_approximation_positive_difference_coefficient_nonzero (v)
  56. 0056specialize cf_approximation_positive_difference_coefficient_nonzero (x1)
  57. 0057specialize cf_approximation_positive_difference_coefficient_nonzero (0)
  58. 0058apply cf_approximation_positive_difference_coefficient_nonzero
  59. 0059exact ht
  60. 0060exact hn_right
  61. 0061exact hzero
  62. 0062exact hn
  63. 0063cases hb_witness_witness_right
  64. 0064cases hb_witness_witness_right_left
  65. 0065exists x
  66. 0066exists x1
  67. 0067left
  68. 0068split
  69. 0069intro hzero
  70. 0070specialize cf_approximation_positive_difference_coefficient_nonzero (t)
  71. 0071specialize cf_approximation_positive_difference_coefficient_nonzero (v)
  72. 0072specialize cf_approximation_positive_difference_coefficient_nonzero (V)
  73. 0073specialize cf_approximation_positive_difference_coefficient_nonzero (x)
  74. 0074specialize cf_approximation_positive_difference_coefficient_nonzero (x1)
  75. 0075apply cf_approximation_positive_difference_coefficient_nonzero
  76. 0076exact ht
  77. 0077exact hb_witness_witness_right_left_right
  78. 0078exact hzero
  79. 0079exact hb_witness_witness_right_left
  80. 0080cases hb_witness_witness_right_right
  81. 0081cases hb_witness_witness_right_right_left
  82. 0082exists x
  83. 0083exists x1
  84. 0084right
  85. 0085split
  86. 0086intro hzero
  87. 0087specialize cf_approximation_positive_difference_coefficient_nonzero (t)
  88. 0088specialize cf_approximation_positive_difference_coefficient_nonzero (V)
  89. 0089specialize cf_approximation_positive_difference_coefficient_nonzero (v)
  90. 0090specialize cf_approximation_positive_difference_coefficient_nonzero (x1)
  91. 0091specialize cf_approximation_positive_difference_coefficient_nonzero (x)
  92. 0092apply cf_approximation_positive_difference_coefficient_nonzero
  93. 0093exact ht
  94. 0094exact hb_witness_witness_right_right_left_right
  95. 0095exact hzero
  96. 0096exact hb_witness_witness_right_right_left
  97. 0097cases hb_witness_witness_right_right_right
  98. 0098exfalso
  99. 0099apply ht
  100. 0100specialize add_eq_zero_left (t)
  101. 0101specialize add_eq_zero_left (x * v + x1 * V)
  102. 0102apply add_eq_zero_left
  103. 0103exact hb_witness_witness_right_right_right_right