BA0025

cf_approximation_alternating_identity_best_approximation

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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.

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 expanded first-order arithmetic 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))

Constructive proof overview

Generated structural guide

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.

The unchanged tactic script uses 1 declared prerequisite and contains 64 exact native proof lines.

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

Proof neighborhood

Direct dependencies

BA0024 cf_approximation_unimodular_best_approximation

Direct dependents

BA0026 cf_approximation_derived_invariant_best_signed

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 exact 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