BA0025

cf_approximation_alternating_identity_best_approximation

The actual determinant and signed-error invariant implies the full comparison with every smaller positive denominator, including signed candidate numerators and exact terminal error zero.

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. AlternatingConvergentIdentity(a,b,u,U,v,V,E,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) · 1AlternatingConvergentIdentity(a,b,u,U,v,V,E,F) · 1Le(a,b) · 2Lt(a,b) · 1

Actual proof prerequisites

cf_approximation_unimodular_best_approximation
Original expanded first-order statement 
forall a b u U v V E F rp rn t D. ((((u * V + 1 = U * v) /\ ((a * v = b * u + E) /\ (b * U = a * V + F)))) \/ (((U * v + 1 = u * V) /\ ((b * u = a * v + E) /\ (a * V = b * U + F))))) -> (exists cfba_bound_identity_comparison_errors. cfba_bound_identity_comparison_errors + (E) = (F)) -> ~(t = 0) -> (exists cfba_gap_identity_comparison_denominator. cfba_gap_identity_comparison_denominator + S (t) = (v)) -> (((a * t + b * rn) = (b * rp) + (D)) \/ ((b * rp) = (a * t + b * rn) + (D))) -> (exists cfba_bound_identity_comparison_result. cfba_bound_identity_comparison_result + (E) = (D))

Complete tactic proof in conservative notation

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

64 script commands · 16 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 (1)
cf approximation unimodular best approximation
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–17

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

  1. L11
    intro t
  2. L12
    intro D
  3. L13
    intro hi
  4. L14
    intro hEF
  5. L15
    intro ht
  6. L16
    intro hlt
  7. L17
    intro herror
03Separate the logical casesL18–20

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

  1. L18
    cases hi
  2. L19
    cases hi_left
  3. L20
    cases hi_left_right
04Use earlier factsL21–30

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

  1. L21
    specialize cf_approximation_unimodular_best_approximation (a)
  2. L22
    specialize cf_approximation_unimodular_best_approximation (b)
  3. L23
    specialize cf_approximation_unimodular_best_approximation (u)
  4. L24
    specialize cf_approximation_unimodular_best_approximation (U)
  5. L25
    specialize cf_approximation_unimodular_best_approximation (v)
  6. L26
    specialize cf_approximation_unimodular_best_approximation (V)
  7. L27
    specialize cf_approximation_unimodular_best_approximation (E)
  8. L28
    specialize cf_approximation_unimodular_best_approximation (F)
  9. L29
    specialize cf_approximation_unimodular_best_approximation (rp)
  10. L30
    specialize cf_approximation_unimodular_best_approximation (rn)
05Use earlier factsL31–33

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

  1. L31
    specialize cf_approximation_unimodular_best_approximation (t)
  2. L32
    specialize cf_approximation_unimodular_best_approximation (D)
  3. L33
    apply cf_approximation_unimodular_best_approximation
06Separate the logical casesL34–34

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

  1. L34
    left
07Use earlier factsL35–35

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

  1. L35
    exact hi_left_left
08Separate the logical casesL36–36

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

  1. L36
    left
09Use earlier factsL37–41

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

  1. L37
    exact hi_left_right
  2. L38
    exact hEF
  3. L39
    exact ht
  4. L40
    exact hlt
  5. L41
    exact herror
10Separate the logical casesL42–43

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

  1. L42
    cases hi_right
  2. L43
    cases hi_right_right
11Use earlier factsL44–53

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

  1. L44
    specialize cf_approximation_unimodular_best_approximation (a)
  2. L45
    specialize cf_approximation_unimodular_best_approximation (b)
  3. L46
    specialize cf_approximation_unimodular_best_approximation (u)
  4. L47
    specialize cf_approximation_unimodular_best_approximation (U)
  5. L48
    specialize cf_approximation_unimodular_best_approximation (v)
  6. L49
    specialize cf_approximation_unimodular_best_approximation (V)
  7. L50
    specialize cf_approximation_unimodular_best_approximation (E)
  8. L51
    specialize cf_approximation_unimodular_best_approximation (F)
  9. L52
    specialize cf_approximation_unimodular_best_approximation (rp)
  10. L53
    specialize cf_approximation_unimodular_best_approximation (rn)
12Use earlier factsL54–56

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

  1. L54
    specialize cf_approximation_unimodular_best_approximation (t)
  2. L55
    specialize cf_approximation_unimodular_best_approximation (D)
  3. L56
    apply cf_approximation_unimodular_best_approximation
13Separate the logical casesL57–57

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

  1. L57
    right
14Use earlier factsL58–58

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

  1. L58
    exact hi_right_left
15Separate the logical casesL59–59

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

  1. L59
    right
16Use earlier factsL60–64

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

  1. L60
    exact hi_right_right
  2. L61
    exact hEF
  3. L62
    exact ht
  4. L63
    exact hlt
  5. L64
    exact herror

Library-wide reading audit

Original defined command ledger · 64 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 hi
  14. 0014intro hEF
  15. 0015intro ht
  16. 0016intro hlt
  17. 0017intro herror
  18. 0018cases hi
  19. 0019cases hi_left
  20. 0020cases hi_left_right
  21. 0021specialize cf_approximation_unimodular_best_approximation (a)
  22. 0022specialize cf_approximation_unimodular_best_approximation (b)
  23. 0023specialize cf_approximation_unimodular_best_approximation (u)
  24. 0024specialize cf_approximation_unimodular_best_approximation (U)
  25. 0025specialize cf_approximation_unimodular_best_approximation (v)
  26. 0026specialize cf_approximation_unimodular_best_approximation (V)
  27. 0027specialize cf_approximation_unimodular_best_approximation (E)
  28. 0028specialize cf_approximation_unimodular_best_approximation (F)
  29. 0029specialize cf_approximation_unimodular_best_approximation (rp)
  30. 0030specialize cf_approximation_unimodular_best_approximation (rn)
  31. 0031specialize cf_approximation_unimodular_best_approximation (t)
  32. 0032specialize cf_approximation_unimodular_best_approximation (D)
  33. 0033apply cf_approximation_unimodular_best_approximation
  34. 0034left
  35. 0035exact hi_left_left
  36. 0036left
  37. 0037exact hi_left_right
  38. 0038exact hEF
  39. 0039exact ht
  40. 0040exact hlt
  41. 0041exact herror
  42. 0042cases hi_right
  43. 0043cases hi_right_right
  44. 0044specialize cf_approximation_unimodular_best_approximation (a)
  45. 0045specialize cf_approximation_unimodular_best_approximation (b)
  46. 0046specialize cf_approximation_unimodular_best_approximation (u)
  47. 0047specialize cf_approximation_unimodular_best_approximation (U)
  48. 0048specialize cf_approximation_unimodular_best_approximation (v)
  49. 0049specialize cf_approximation_unimodular_best_approximation (V)
  50. 0050specialize cf_approximation_unimodular_best_approximation (E)
  51. 0051specialize cf_approximation_unimodular_best_approximation (F)
  52. 0052specialize cf_approximation_unimodular_best_approximation (rp)
  53. 0053specialize cf_approximation_unimodular_best_approximation (rn)
  54. 0054specialize cf_approximation_unimodular_best_approximation (t)
  55. 0055specialize cf_approximation_unimodular_best_approximation (D)
  56. 0056apply cf_approximation_unimodular_best_approximation
  57. 0057right
  58. 0058exact hi_right_left
  59. 0059right
  60. 0060exact hi_right_right
  61. 0061exact hEF
  62. 0062exact ht
  63. 0063exact hlt
  64. 0064exact herror