BA000D

cf_approximation_derived_invariant_denominator_positive

Every actual derived nonempty-prefix invariant forces a positive denominator; this is proved, rather than postulated to make the convergent predicate non-vacuous.

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. ConvergentErrorInvariant(a,b,u,U,v,V) → ¬v = 0

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

Definition DAG

ConvergentErrorInvariant(a,b,u,U,v,V) · 1

Actual proof prerequisites

succ_ne_zero · checked external prerequisitemul_eq_one_components · checked external prerequisitemul_one · checked external prerequisitezero_add · checked external prerequisitelt_not_le · checked external prerequisite
Original expanded first-order statement 
forall a b u U v V. (exists cfba_error_positive_denominator cfba_previous_error_positive_denominator. (((((u * V + 1 = U * v) /\ ((a * v = b * u + cfba_error_positive_denominator) /\ (b * U = a * V + cfba_previous_error_positive_denominator)))) \/ (((U * v + 1 = u * V) /\ ((b * u = a * v + cfba_error_positive_denominator) /\ (a * V = b * U + cfba_previous_error_positive_denominator))))) /\ ((exists cfba_gap_positive_denominatordecrease. cfba_gap_positive_denominatordecrease + S (cfba_error_positive_denominator) = (cfba_previous_error_positive_denominator)) /\ (exists cfba_bound_positive_denominatorprevious_bound. cfba_bound_positive_denominatorprevious_bound + (cfba_previous_error_positive_denominator) = (b))))) -> ~(v = 0)

Complete tactic proof in conservative notation

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

51 script commands · 14 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.

01Fix variables and assumptionsL1–8

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 hi
  8. L8
    intro hv
02Separate the logical casesL9–14

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

  1. L9
    cases hi
  2. L10
    cases hi_witness
  3. L11
    cases hi_witness_witness
  4. L12
    cases hi_witness_witness_right
  5. L13
    cases hi_witness_witness_left
  6. L14
    cases hi_witness_witness_left_left
03Use earlier factsL15–16

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

  1. L15
    specialize succ_ne_zero (u * V)
  2. L16
    apply succ_ne_zero
04Calculate and transport equalitiesL17–19

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L17
    trans u * V + 1
  2. L18
    simp
  3. L19
    trans U * v
05Use earlier factsL20–20

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

  1. L20
    exact hi_witness_witness_left_left_left
06Calculate and transport equalitiesL21–22

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L21
    rewrite hv
  2. L22
    simp
07Separate the logical casesL23–24

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

  1. L23
    cases hi_witness_witness_left_right
  2. L24
    cases hi_witness_witness_left_right_right
08Establish hmL25–30

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

  1. L25
    have hm : u * V = 1
  2. L26
    trans U * v + 1
  3. L27
    symm
  4. L28
    exact hi_witness_witness_left_right_left
  5. L29
    rewrite hv
  6. L30
    simp
09Establish hoL31–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul eq one components.

  1. L31
    have ho : u = 1 /\ V = 1
  2. L32
    specialize mul_eq_one_components (u)
  3. L33
    specialize mul_eq_one_components (V)
  4. L34
    apply mul_eq_one_components
  5. L35
    exact hm
10Separate the logical casesL36–36

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

  1. L36
    cases ho
11Establish heL37–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul one.

  1. L37
    have he : b = x
  2. L38
    trans b * u
  3. L39
    rewrite ho_left
  4. L40
    symm
  5. L41
    apply mul_one
  6. L42
    trans a * v + x
  7. L43
    exact hi_witness_witness_left_right_right_left
  8. L44
    rewrite hv
  9. L45
    simp [zero_add]
  10. L46
    specialize lt_not_le (x)
12Use earlier factsL47–49

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

  1. L47
    specialize lt_not_le (x1)
  2. L48
    apply lt_not_le
  3. L49
    exact hi_witness_witness_right_left
13Calculate and transport equalitiesL50–50

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L50
    rewrite <- he
14Use earlier factsL51–51

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

  1. L51
    exact hi_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro u
  4. 0004intro U
  5. 0005intro v
  6. 0006intro V
  7. 0007intro hi
  8. 0008intro hv
  9. 0009cases hi
  10. 0010cases hi_witness
  11. 0011cases hi_witness_witness
  12. 0012cases hi_witness_witness_right
  13. 0013cases hi_witness_witness_left
  14. 0014cases hi_witness_witness_left_left
  15. 0015specialize succ_ne_zero (u * V)
  16. 0016apply succ_ne_zero
  17. 0017trans u * V + 1
  18. 0018simp
  19. 0019trans U * v
  20. 0020exact hi_witness_witness_left_left_left
  21. 0021rewrite hv
  22. 0022simp
  23. 0023cases hi_witness_witness_left_right
  24. 0024cases hi_witness_witness_left_right_right
  25. 0025have hm : u * V = 1
  26. 0026trans U * v + 1
  27. 0027symm
  28. 0028exact hi_witness_witness_left_right_left
  29. 0029rewrite hv
  30. 0030simp
  31. 0031have ho : u = 1 /\ V = 1
  32. 0032specialize mul_eq_one_components (u)
  33. 0033specialize mul_eq_one_components (V)
  34. 0034apply mul_eq_one_components
  35. 0035exact hm
  36. 0036cases ho
  37. 0037have he : b = x
  38. 0038trans b * u
  39. 0039rewrite ho_left
  40. 0040symm
  41. 0041apply mul_one
  42. 0042trans a * v + x
  43. 0043exact hi_witness_witness_left_right_right_left
  44. 0044rewrite hv
  45. 0045simp [zero_add]
  46. 0046specialize lt_not_le (x)
  47. 0047specialize lt_not_le (x1)
  48. 0048apply lt_not_le
  49. 0049exact hi_witness_witness_right_left
  50. 0050rewrite <- he
  51. 0051exact hi_witness_witness_right_right