BA000C

cf_approximation_prepend_recurrence_error_invariant

Actual quotient recurrence transports the derived determinant and decreasing errors while retaining the previous-error bound by the input denominator.

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) → u = q · p + n → U = q · P + N → v = p → V = P → ConvergentErrorInvariant(b,r,p,P,n,N) → ConvergentErrorInvariant(a,b,u,U,v,V)

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

Definition DAG

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

Actual proof prerequisites

cf_approximation_identity_entry_transportcf_approximation_prepend_identityle_trans · checked external prerequisitelt_to_le · 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_prepend_remainder. cfba_gap_prepend_remainder + S (r) = (b)) -> u = q * p + n -> U = q * P + N -> v = p -> V = P -> (exists cfba_error_prepend_source cfba_previous_error_prepend_source. (((((p * N + 1 = P * n) /\ ((b * n = r * p + cfba_error_prepend_source) /\ (r * P = b * N + cfba_previous_error_prepend_source)))) \/ (((P * n + 1 = p * N) /\ ((r * p = b * n + cfba_error_prepend_source) /\ (b * N = r * P + cfba_previous_error_prepend_source))))) /\ ((exists cfba_gap_prepend_sourcedecrease. cfba_gap_prepend_sourcedecrease + S (cfba_error_prepend_source) = (cfba_previous_error_prepend_source)) /\ (exists cfba_bound_prepend_sourceprevious_bound. cfba_bound_prepend_sourceprevious_bound + (cfba_previous_error_prepend_source) = (r))))) -> (exists cfba_error_prepend_result cfba_previous_error_prepend_result. (((((u * V + 1 = U * v) /\ ((a * v = b * u + cfba_error_prepend_result) /\ (b * U = a * V + cfba_previous_error_prepend_result)))) \/ (((U * v + 1 = u * V) /\ ((b * u = a * v + cfba_error_prepend_result) /\ (a * V = b * U + cfba_previous_error_prepend_result))))) /\ ((exists cfba_gap_prepend_resultdecrease. cfba_gap_prepend_resultdecrease + S (cfba_error_prepend_result) = (cfba_previous_error_prepend_result)) /\ (exists cfba_bound_prepend_resultprevious_bound. cfba_bound_prepend_resultprevious_bound + (cfba_previous_error_prepend_result) = (b)))))

Complete tactic proof in conservative notation

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

67 script commands · 10 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 (2)
cf approximation identity entry transportcf 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–19

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 hu
  6. L16
    intro hU
  7. L17
    intro hv
  8. L18
    intro hV
  9. L19
    intro hi
03Separate the logical casesL20–23

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

  1. L20
    cases hi
  2. L21
    cases hi_witness
  3. L22
    cases hi_witness_witness
  4. L23
    cases hi_witness_witness_right
04Construct an explicit witnessL24–25

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

  1. L24
    exists x
  2. L25
    exists x1
05Separate the logical casesL26–26

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

  1. L26
    split
06Use earlier factsL27–36

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

  1. L27
    specialize cf_approximation_identity_entry_transport (a)
  2. L28
    specialize cf_approximation_identity_entry_transport (b)
  3. L29
    specialize cf_approximation_identity_entry_transport (u)
  4. L30
    specialize cf_approximation_identity_entry_transport (U)
  5. L31
    specialize cf_approximation_identity_entry_transport (v)
  6. L32
    specialize cf_approximation_identity_entry_transport (V)
  7. L33
    specialize cf_approximation_identity_entry_transport ((q * p + n))
  8. L34
    specialize cf_approximation_identity_entry_transport ((q * P + N))
  9. L35
    specialize cf_approximation_identity_entry_transport (p)
  10. L36
    specialize cf_approximation_identity_entry_transport (P)
07Use earlier factsL37–46

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

  1. L37
    specialize cf_approximation_identity_entry_transport (x)
  2. L38
    specialize cf_approximation_identity_entry_transport (x1)
  3. L39
    apply cf_approximation_identity_entry_transport
  4. L40
    exact hu
  5. L41
    exact hU
  6. L42
    exact hv
  7. L43
    exact hV
  8. L44
    specialize cf_approximation_prepend_identity (a)
  9. L45
    specialize cf_approximation_prepend_identity (b)
  10. L46
    specialize cf_approximation_prepend_identity (q)
08Use earlier factsL47–56

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

  1. L47
    specialize cf_approximation_prepend_identity (r)
  2. L48
    specialize cf_approximation_prepend_identity (p)
  3. L49
    specialize cf_approximation_prepend_identity (P)
  4. L50
    specialize cf_approximation_prepend_identity (n)
  5. L51
    specialize cf_approximation_prepend_identity (N)
  6. L52
    specialize cf_approximation_prepend_identity (x)
  7. L53
    specialize cf_approximation_prepend_identity (x1)
  8. L54
    apply cf_approximation_prepend_identity
  9. L55
    exact ha
  10. L56
    exact hi_witness_witness_left
09Separate the logical casesL57–57

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

  1. L57
    split
10Use earlier factsL58–67

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

  1. L58
    exact hi_witness_witness_right_left
  2. L59
    specialize le_trans (x1)
  3. L60
    specialize le_trans (r)
  4. L61
    specialize le_trans (b)
  5. L62
    apply le_trans
  6. L63
    exact hi_witness_witness_right_right
  7. L64
    specialize lt_to_le (r)
  8. L65
    specialize lt_to_le (b)
  9. L66
    apply lt_to_le
  10. L67
    exact hr

Library-wide reading audit

Original defined command ledger · 67 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 hu
  16. 0016intro hU
  17. 0017intro hv
  18. 0018intro hV
  19. 0019intro hi
  20. 0020cases hi
  21. 0021cases hi_witness
  22. 0022cases hi_witness_witness
  23. 0023cases hi_witness_witness_right
  24. 0024exists x
  25. 0025exists x1
  26. 0026split
  27. 0027specialize cf_approximation_identity_entry_transport (a)
  28. 0028specialize cf_approximation_identity_entry_transport (b)
  29. 0029specialize cf_approximation_identity_entry_transport (u)
  30. 0030specialize cf_approximation_identity_entry_transport (U)
  31. 0031specialize cf_approximation_identity_entry_transport (v)
  32. 0032specialize cf_approximation_identity_entry_transport (V)
  33. 0033specialize cf_approximation_identity_entry_transport ((q * p + n))
  34. 0034specialize cf_approximation_identity_entry_transport ((q * P + N))
  35. 0035specialize cf_approximation_identity_entry_transport (p)
  36. 0036specialize cf_approximation_identity_entry_transport (P)
  37. 0037specialize cf_approximation_identity_entry_transport (x)
  38. 0038specialize cf_approximation_identity_entry_transport (x1)
  39. 0039apply cf_approximation_identity_entry_transport
  40. 0040exact hu
  41. 0041exact hU
  42. 0042exact hv
  43. 0043exact hV
  44. 0044specialize cf_approximation_prepend_identity (a)
  45. 0045specialize cf_approximation_prepend_identity (b)
  46. 0046specialize cf_approximation_prepend_identity (q)
  47. 0047specialize cf_approximation_prepend_identity (r)
  48. 0048specialize cf_approximation_prepend_identity (p)
  49. 0049specialize cf_approximation_prepend_identity (P)
  50. 0050specialize cf_approximation_prepend_identity (n)
  51. 0051specialize cf_approximation_prepend_identity (N)
  52. 0052specialize cf_approximation_prepend_identity (x)
  53. 0053specialize cf_approximation_prepend_identity (x1)
  54. 0054apply cf_approximation_prepend_identity
  55. 0055exact ha
  56. 0056exact hi_witness_witness_left
  57. 0057split
  58. 0058exact hi_witness_witness_right_left
  59. 0059specialize le_trans (x1)
  60. 0060specialize le_trans (r)
  61. 0061specialize le_trans (b)
  62. 0062apply le_trans
  63. 0063exact hi_witness_witness_right_right
  64. 0064specialize lt_to_le (r)
  65. 0065specialize lt_to_le (b)
  66. 0066apply lt_to_le
  67. 0067exact hr