BA000B

cf_approximation_first_recurrence_error_invariant

A genuine first Euclidean quotient applied to the actual identity matrix yields errors r<b and b, including quotient zero and remainder 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. ∀ q. ∀ r. ∀ u. ∀ U. ∀ v. ∀ V. ∀ p. ∀ P. ∀ n. ∀ N. a = b · q + r → Lt(r,b) → p = 1 → P = 0 → n = 0 → N = 1 → u = q · p + n → U = q · P + N → v = p → V = P → ConvergentErrorInvariant(a,b,u,U,v,V)

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

Definition DAG

AlternatingConvergentIdentity(a,b,u,U,v,V,E,F) · 1ConvergentErrorInvariant(a,b,u,U,v,V) · 1Lt(a,b) · 1

Actual proof prerequisites

cf_approximation_identity_entry_transportcf_approximation_empty_matrix_identitycf_approximation_prepend_identityle_refl · checked external prerequisite
Original expanded first-order statement 
forall a b q r u U v V p P n N. a = b * q + r -> (exists cfba_gap_first_remainder. cfba_gap_first_remainder + S (r) = (b)) -> p = 1 -> P = 0 -> n = 0 -> N = 1 -> u = q * p + n -> U = q * P + N -> v = p -> V = P -> (exists cfba_error_first_invariant cfba_previous_error_first_invariant. (((((u * V + 1 = U * v) /\ ((a * v = b * u + cfba_error_first_invariant) /\ (b * U = a * V + cfba_previous_error_first_invariant)))) \/ (((U * v + 1 = u * V) /\ ((b * u = a * v + cfba_error_first_invariant) /\ (a * V = b * U + cfba_previous_error_first_invariant))))) /\ ((exists cfba_gap_first_invariantdecrease. cfba_gap_first_invariantdecrease + S (cfba_error_first_invariant) = (cfba_previous_error_first_invariant)) /\ (exists cfba_bound_first_invariantprevious_bound. cfba_bound_first_invariantprevious_bound + (cfba_previous_error_first_invariant) = (b)))))

Complete tactic proof in conservative notation

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

80 script commands · 13 reading checkpoints · 1 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 (3)
cf approximation identity entry transportcf approximation empty matrix identitycf approximation prepend identity
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 p
  10. L10
    intro P
02Fix variables and assumptionsL11–20

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

  1. L11
    intro n
  2. L12
    intro N
  3. L13
    intro ha
  4. L14
    intro hr
  5. L15
    intro hp
  6. L16
    intro hP
  7. L17
    intro hn
  8. L18
    intro hN
  9. L19
    intro hu
  10. L20
    intro hU
03Fix variables and assumptionsL21–22

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

  1. L21
    intro hv
  2. L22
    intro hV
04Establish hiL23–32

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

  1. L23
    have hi : AlternatingConvergentIdentity(b,r,p,P,n,N,r,b)Definitions: AlternatingConvergentIdentity(b,r,p,P,n,N,r,b)Original native command in the exact edition
  2. L24
    specialize cf_approximation_identity_entry_transport (b)
  3. L25
    specialize cf_approximation_identity_entry_transport (r)
  4. L26
    specialize cf_approximation_identity_entry_transport (p)
  5. L27
    specialize cf_approximation_identity_entry_transport (P)
  6. L28
    specialize cf_approximation_identity_entry_transport (n)
  7. L29
    specialize cf_approximation_identity_entry_transport (N)
  8. L30
    specialize cf_approximation_identity_entry_transport (1)
  9. L31
    specialize cf_approximation_identity_entry_transport (0)
  10. L32
    specialize cf_approximation_identity_entry_transport (0)
05Use earlier factsL33–42

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

  1. L33
    specialize cf_approximation_identity_entry_transport (1)
  2. L34
    specialize cf_approximation_identity_entry_transport (r)
  3. L35
    specialize cf_approximation_identity_entry_transport (b)
  4. L36
    apply cf_approximation_identity_entry_transport
  5. L37
    exact hp
  6. L38
    exact hP
  7. L39
    exact hn
  8. L40
    exact hN
  9. L41
    specialize cf_approximation_empty_matrix_identity (b)
  10. L42
    specialize cf_approximation_empty_matrix_identity (r)
06Use earlier factsL43–43

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

  1. L43
    apply cf_approximation_empty_matrix_identity
07Construct an explicit witnessL44–45

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

  1. L44
    exists r
  2. L45
    exists b
08Separate the logical casesL46–46

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

  1. L46
    split
09Use earlier factsL47–56

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

  1. L47
    specialize cf_approximation_identity_entry_transport (a)
  2. L48
    specialize cf_approximation_identity_entry_transport (b)
  3. L49
    specialize cf_approximation_identity_entry_transport (u)
  4. L50
    specialize cf_approximation_identity_entry_transport (U)
  5. L51
    specialize cf_approximation_identity_entry_transport (v)
  6. L52
    specialize cf_approximation_identity_entry_transport (V)
  7. L53
    specialize cf_approximation_identity_entry_transport ((q * p + n))
  8. L54
    specialize cf_approximation_identity_entry_transport ((q * P + N))
  9. L55
    specialize cf_approximation_identity_entry_transport (p)
  10. L56
    specialize cf_approximation_identity_entry_transport (P)
10Use earlier factsL57–66

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

  1. L57
    specialize cf_approximation_identity_entry_transport (r)
  2. L58
    specialize cf_approximation_identity_entry_transport (b)
  3. L59
    apply cf_approximation_identity_entry_transport
  4. L60
    exact hu
  5. L61
    exact hU
  6. L62
    exact hv
  7. L63
    exact hV
  8. L64
    specialize cf_approximation_prepend_identity (a)
  9. L65
    specialize cf_approximation_prepend_identity (b)
  10. L66
    specialize cf_approximation_prepend_identity (q)
11Use earlier factsL67–76

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

  1. L67
    specialize cf_approximation_prepend_identity (r)
  2. L68
    specialize cf_approximation_prepend_identity (p)
  3. L69
    specialize cf_approximation_prepend_identity (P)
  4. L70
    specialize cf_approximation_prepend_identity (n)
  5. L71
    specialize cf_approximation_prepend_identity (N)
  6. L72
    specialize cf_approximation_prepend_identity (r)
  7. L73
    specialize cf_approximation_prepend_identity (b)
  8. L74
    apply cf_approximation_prepend_identity
  9. L75
    exact ha
  10. L76
    exact hi
12Separate the logical casesL77–77

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

  1. L77
    split
13Use earlier factsL78–80

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

  1. L78
    exact hr
  2. L79
    specialize le_refl (b)
  3. L80
    apply le_refl

Library-wide reading audit

Original defined command ledger · 80 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 p
  10. 0010intro P
  11. 0011intro n
  12. 0012intro N
  13. 0013intro ha
  14. 0014intro hr
  15. 0015intro hp
  16. 0016intro hP
  17. 0017intro hn
  18. 0018intro hN
  19. 0019intro hu
  20. 0020intro hU
  21. 0021intro hv
  22. 0022intro hV
  23. 0023have hi : AlternatingConvergentIdentity(b,r,p,P,n,N,r,b)
  24. 0024specialize cf_approximation_identity_entry_transport (b)
  25. 0025specialize cf_approximation_identity_entry_transport (r)
  26. 0026specialize cf_approximation_identity_entry_transport (p)
  27. 0027specialize cf_approximation_identity_entry_transport (P)
  28. 0028specialize cf_approximation_identity_entry_transport (n)
  29. 0029specialize cf_approximation_identity_entry_transport (N)
  30. 0030specialize cf_approximation_identity_entry_transport (1)
  31. 0031specialize cf_approximation_identity_entry_transport (0)
  32. 0032specialize cf_approximation_identity_entry_transport (0)
  33. 0033specialize cf_approximation_identity_entry_transport (1)
  34. 0034specialize cf_approximation_identity_entry_transport (r)
  35. 0035specialize cf_approximation_identity_entry_transport (b)
  36. 0036apply cf_approximation_identity_entry_transport
  37. 0037exact hp
  38. 0038exact hP
  39. 0039exact hn
  40. 0040exact hN
  41. 0041specialize cf_approximation_empty_matrix_identity (b)
  42. 0042specialize cf_approximation_empty_matrix_identity (r)
  43. 0043apply cf_approximation_empty_matrix_identity
  44. 0044exists r
  45. 0045exists b
  46. 0046split
  47. 0047specialize cf_approximation_identity_entry_transport (a)
  48. 0048specialize cf_approximation_identity_entry_transport (b)
  49. 0049specialize cf_approximation_identity_entry_transport (u)
  50. 0050specialize cf_approximation_identity_entry_transport (U)
  51. 0051specialize cf_approximation_identity_entry_transport (v)
  52. 0052specialize cf_approximation_identity_entry_transport (V)
  53. 0053specialize cf_approximation_identity_entry_transport ((q * p + n))
  54. 0054specialize cf_approximation_identity_entry_transport ((q * P + N))
  55. 0055specialize cf_approximation_identity_entry_transport (p)
  56. 0056specialize cf_approximation_identity_entry_transport (P)
  57. 0057specialize cf_approximation_identity_entry_transport (r)
  58. 0058specialize cf_approximation_identity_entry_transport (b)
  59. 0059apply cf_approximation_identity_entry_transport
  60. 0060exact hu
  61. 0061exact hU
  62. 0062exact hv
  63. 0063exact hV
  64. 0064specialize cf_approximation_prepend_identity (a)
  65. 0065specialize cf_approximation_prepend_identity (b)
  66. 0066specialize cf_approximation_prepend_identity (q)
  67. 0067specialize cf_approximation_prepend_identity (r)
  68. 0068specialize cf_approximation_prepend_identity (p)
  69. 0069specialize cf_approximation_prepend_identity (P)
  70. 0070specialize cf_approximation_prepend_identity (n)
  71. 0071specialize cf_approximation_prepend_identity (N)
  72. 0072specialize cf_approximation_prepend_identity (r)
  73. 0073specialize cf_approximation_prepend_identity (b)
  74. 0074apply cf_approximation_prepend_identity
  75. 0075exact ha
  76. 0076exact hi
  77. 0077split
  78. 0078exact hr
  79. 0079specialize le_refl (b)
  80. 0080apply le_refl