BA0006

cf_approximation_prepend_identity

A quotient prepended to both actual convergents transports both error magnitudes and the alternating determinant.

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. ∀ q. ∀ r. ∀ u. ∀ U. ∀ v. ∀ V. ∀ E. ∀ F. a = b · q + r → AlternatingConvergentIdentity(b,r,u,U,v,V,E,F) → AlternatingConvergentIdentity(a,b,q · u + v,q · U + V,u,U,E,F)

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

Definition DAG

AlternatingConvergentIdentity(a,b,u,U,v,V,E,F) · 2

Actual proof prerequisites

cf_approximation_prepend_determinant_forwardcf_approximation_prepend_determinant_backwardcf_approximation_prepend_error_forwardcf_approximation_prepend_error_backward
Original expanded first-order statement 
forall a b q r u U v V E F. a = b * q + r -> ((((u * V + 1 = U * v) /\ ((b * v = r * u + E) /\ (r * U = b * V + F)))) \/ (((U * v + 1 = u * V) /\ ((r * u = b * v + E) /\ (b * V = r * U + F))))) -> (((((q * u + v) * U + 1 = (q * U + V) * u) /\ ((a * u = b * (q * u + v) + E) /\ (b * (q * U + V) = a * U + F)))) \/ ((((q * U + V) * u + 1 = (q * u + v) * U) /\ ((b * (q * u + v) = a * u + E) /\ (a * U = b * (q * U + V) + F)))))

Complete tactic proof in conservative notation

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

77 script commands · 12 reading checkpoints · 0 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 prepend determinant forwardcf approximation prepend error forwardcf approximation prepend error backwardcf approximation prepend determinant backward
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 q
  4. L4
    intro r
  5. L5
    intro u
  6. L6
    intro U
  7. L7
    intro v
  8. L8
    intro V
  9. L9
    intro E
  10. L10
    intro F
02Fix variables and assumptionsL11–12

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

  1. L11
    intro ha
  2. L12
    intro h
03Separate the logical casesL13–17

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

  1. L13
    cases h
  2. L14
    cases h_left
  3. L15
    cases h_left_right
  4. L16
    right
  5. L17
    split
04Use earlier factsL18–24

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

  1. L18
    specialize cf_approximation_prepend_determinant_forward (u)
  2. L19
    specialize cf_approximation_prepend_determinant_forward (U)
  3. L20
    specialize cf_approximation_prepend_determinant_forward (v)
  4. L21
    specialize cf_approximation_prepend_determinant_forward (V)
  5. L22
    specialize cf_approximation_prepend_determinant_forward (q)
  6. L23
    apply cf_approximation_prepend_determinant_forward
  7. L24
    exact h_left_left
05Separate the logical casesL25–25

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

  1. L25
    split
06Use earlier factsL26–35

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

  1. L26
    specialize cf_approximation_prepend_error_forward (a)
  2. L27
    specialize cf_approximation_prepend_error_forward (b)
  3. L28
    specialize cf_approximation_prepend_error_forward (q)
  4. L29
    specialize cf_approximation_prepend_error_forward (r)
  5. L30
    specialize cf_approximation_prepend_error_forward (u)
  6. L31
    specialize cf_approximation_prepend_error_forward (v)
  7. L32
    specialize cf_approximation_prepend_error_forward (E)
  8. L33
    apply cf_approximation_prepend_error_forward
  9. L34
    exact ha
  10. L35
    exact h_left_right_left
07Use earlier factsL36–45

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

  1. L36
    specialize cf_approximation_prepend_error_backward (a)
  2. L37
    specialize cf_approximation_prepend_error_backward (b)
  3. L38
    specialize cf_approximation_prepend_error_backward (q)
  4. L39
    specialize cf_approximation_prepend_error_backward (r)
  5. L40
    specialize cf_approximation_prepend_error_backward (U)
  6. L41
    specialize cf_approximation_prepend_error_backward (V)
  7. L42
    specialize cf_approximation_prepend_error_backward (F)
  8. L43
    apply cf_approximation_prepend_error_backward
  9. L44
    exact ha
  10. L45
    exact h_left_right_right
08Separate the logical casesL46–49

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

  1. L46
    cases h_right
  2. L47
    cases h_right_right
  3. L48
    left
  4. L49
    split
09Use earlier factsL50–56

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

  1. L50
    specialize cf_approximation_prepend_determinant_backward (u)
  2. L51
    specialize cf_approximation_prepend_determinant_backward (U)
  3. L52
    specialize cf_approximation_prepend_determinant_backward (v)
  4. L53
    specialize cf_approximation_prepend_determinant_backward (V)
  5. L54
    specialize cf_approximation_prepend_determinant_backward (q)
  6. L55
    apply cf_approximation_prepend_determinant_backward
  7. L56
    exact h_right_left
10Separate the logical casesL57–57

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

  1. L57
    split
11Use earlier factsL58–67

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

  1. L58
    specialize cf_approximation_prepend_error_backward (a)
  2. L59
    specialize cf_approximation_prepend_error_backward (b)
  3. L60
    specialize cf_approximation_prepend_error_backward (q)
  4. L61
    specialize cf_approximation_prepend_error_backward (r)
  5. L62
    specialize cf_approximation_prepend_error_backward (u)
  6. L63
    specialize cf_approximation_prepend_error_backward (v)
  7. L64
    specialize cf_approximation_prepend_error_backward (E)
  8. L65
    apply cf_approximation_prepend_error_backward
  9. L66
    exact ha
  10. L67
    exact h_right_right_left
12Use earlier factsL68–77

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

  1. L68
    specialize cf_approximation_prepend_error_forward (a)
  2. L69
    specialize cf_approximation_prepend_error_forward (b)
  3. L70
    specialize cf_approximation_prepend_error_forward (q)
  4. L71
    specialize cf_approximation_prepend_error_forward (r)
  5. L72
    specialize cf_approximation_prepend_error_forward (U)
  6. L73
    specialize cf_approximation_prepend_error_forward (V)
  7. L74
    specialize cf_approximation_prepend_error_forward (F)
  8. L75
    apply cf_approximation_prepend_error_forward
  9. L76
    exact ha
  10. L77
    exact h_right_right_right

Library-wide reading audit

Original defined command ledger · 77 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro q
  4. 0004intro r
  5. 0005intro u
  6. 0006intro U
  7. 0007intro v
  8. 0008intro V
  9. 0009intro E
  10. 0010intro F
  11. 0011intro ha
  12. 0012intro h
  13. 0013cases h
  14. 0014cases h_left
  15. 0015cases h_left_right
  16. 0016right
  17. 0017split
  18. 0018specialize cf_approximation_prepend_determinant_forward (u)
  19. 0019specialize cf_approximation_prepend_determinant_forward (U)
  20. 0020specialize cf_approximation_prepend_determinant_forward (v)
  21. 0021specialize cf_approximation_prepend_determinant_forward (V)
  22. 0022specialize cf_approximation_prepend_determinant_forward (q)
  23. 0023apply cf_approximation_prepend_determinant_forward
  24. 0024exact h_left_left
  25. 0025split
  26. 0026specialize cf_approximation_prepend_error_forward (a)
  27. 0027specialize cf_approximation_prepend_error_forward (b)
  28. 0028specialize cf_approximation_prepend_error_forward (q)
  29. 0029specialize cf_approximation_prepend_error_forward (r)
  30. 0030specialize cf_approximation_prepend_error_forward (u)
  31. 0031specialize cf_approximation_prepend_error_forward (v)
  32. 0032specialize cf_approximation_prepend_error_forward (E)
  33. 0033apply cf_approximation_prepend_error_forward
  34. 0034exact ha
  35. 0035exact h_left_right_left
  36. 0036specialize cf_approximation_prepend_error_backward (a)
  37. 0037specialize cf_approximation_prepend_error_backward (b)
  38. 0038specialize cf_approximation_prepend_error_backward (q)
  39. 0039specialize cf_approximation_prepend_error_backward (r)
  40. 0040specialize cf_approximation_prepend_error_backward (U)
  41. 0041specialize cf_approximation_prepend_error_backward (V)
  42. 0042specialize cf_approximation_prepend_error_backward (F)
  43. 0043apply cf_approximation_prepend_error_backward
  44. 0044exact ha
  45. 0045exact h_left_right_right
  46. 0046cases h_right
  47. 0047cases h_right_right
  48. 0048left
  49. 0049split
  50. 0050specialize cf_approximation_prepend_determinant_backward (u)
  51. 0051specialize cf_approximation_prepend_determinant_backward (U)
  52. 0052specialize cf_approximation_prepend_determinant_backward (v)
  53. 0053specialize cf_approximation_prepend_determinant_backward (V)
  54. 0054specialize cf_approximation_prepend_determinant_backward (q)
  55. 0055apply cf_approximation_prepend_determinant_backward
  56. 0056exact h_right_left
  57. 0057split
  58. 0058specialize cf_approximation_prepend_error_backward (a)
  59. 0059specialize cf_approximation_prepend_error_backward (b)
  60. 0060specialize cf_approximation_prepend_error_backward (q)
  61. 0061specialize cf_approximation_prepend_error_backward (r)
  62. 0062specialize cf_approximation_prepend_error_backward (u)
  63. 0063specialize cf_approximation_prepend_error_backward (v)
  64. 0064specialize cf_approximation_prepend_error_backward (E)
  65. 0065apply cf_approximation_prepend_error_backward
  66. 0066exact ha
  67. 0067exact h_right_right_left
  68. 0068specialize cf_approximation_prepend_error_forward (a)
  69. 0069specialize cf_approximation_prepend_error_forward (b)
  70. 0070specialize cf_approximation_prepend_error_forward (q)
  71. 0071specialize cf_approximation_prepend_error_forward (r)
  72. 0072specialize cf_approximation_prepend_error_forward (U)
  73. 0073specialize cf_approximation_prepend_error_forward (V)
  74. 0074specialize cf_approximation_prepend_error_forward (F)
  75. 0075apply cf_approximation_prepend_error_forward
  76. 0076exact ha
  77. 0077exact h_right_right_right