BA0011

cf_approximation_subtract_previous_absolute_error

The actual absolute error of a signed numerator difference is the nonnegative sum of the two error contributions.

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. ∀ c. ∀ d. a · v = b · u + E ∧ b · U = a · V + F ∨ b · u = a · v + E ∧ a · V = b · U + F → rp + d · U = rn + c · u ∧ t + d · V = c · v → RationalApproximationError(a,b,rp,rn,t,c · E + d · F)

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

Definition DAG

RationalApproximationError(a,b,rp,rn,t,E) · 1

Actual proof prerequisites

cf_approximation_opposite_errors_linear_absolutecf_approximation_subtract_previous_error_balancematrix_lattice_absolute_difference_integer_transport · checked external prerequisite
Original expanded first-order statement 
forall a b u U v V E F rp rn t c d. (((a * v = b * u + E) /\ (b * U = a * V + F)) \/ ((b * u = a * v + E) /\ (a * V = b * U + F))) -> (((rp + d * U = rn + c * u) /\ (t + d * V = c * v))) -> (((a * t + b * rn) = (b * rp) + (c * E + d * F)) \/ ((b * rp) = (a * t + b * rn) + (c * E + d * F)))

Complete tactic proof in conservative notation

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

49 script commands · 7 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 (2)
cf approximation subtract previous error balancecf approximation opposite errors linear absolute
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–15

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

  1. L11
    intro t
  2. L12
    intro c
  3. L13
    intro d
  4. L14
    intro he
  5. L15
    intro hc
03Establish hbL16–25

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

  1. L16
    have hb : (a * t + b * rn) + (c * (b * u) + d * (a * V)) = (c * (a * v) + d * (b * U)) + (b * rp)
  2. L17
    specialize cf_approximation_subtract_previous_error_balance (a)
  3. L18
    specialize cf_approximation_subtract_previous_error_balance (b)
  4. L19
    specialize cf_approximation_subtract_previous_error_balance (u)
  5. L20
    specialize cf_approximation_subtract_previous_error_balance (U)
  6. L21
    specialize cf_approximation_subtract_previous_error_balance (v)
  7. L22
    specialize cf_approximation_subtract_previous_error_balance (V)
  8. L23
    specialize cf_approximation_subtract_previous_error_balance (rp)
  9. L24
    specialize cf_approximation_subtract_previous_error_balance (rn)
  10. L25
    specialize cf_approximation_subtract_previous_error_balance (t)
04Use earlier factsL26–35

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

  1. L26
    specialize cf_approximation_subtract_previous_error_balance (c)
  2. L27
    specialize cf_approximation_subtract_previous_error_balance (d)
  3. L28
    apply cf_approximation_subtract_previous_error_balance
  4. L29
    exact hc
  5. L30
    specialize matrix_lattice_absolute_difference_integer_transport (c * (a * v) + d * (b * U))
  6. L31
    specialize matrix_lattice_absolute_difference_integer_transport (c * (b * u) + d * (a * V))
  7. L32
    specialize matrix_lattice_absolute_difference_integer_transport (a * t + b * rn)
  8. L33
    specialize matrix_lattice_absolute_difference_integer_transport (b * rp)
  9. L34
    specialize matrix_lattice_absolute_difference_integer_transport (c * E + d * F)
  10. L35
    apply matrix_lattice_absolute_difference_integer_transport
05Calculate and transport equalitiesL36–36

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

  1. L36
    symm
06Use earlier factsL37–46

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

  1. L37
    exact hb
  2. L38
    specialize cf_approximation_opposite_errors_linear_absolute (a)
  3. L39
    specialize cf_approximation_opposite_errors_linear_absolute (b)
  4. L40
    specialize cf_approximation_opposite_errors_linear_absolute (u)
  5. L41
    specialize cf_approximation_opposite_errors_linear_absolute (U)
  6. L42
    specialize cf_approximation_opposite_errors_linear_absolute (v)
  7. L43
    specialize cf_approximation_opposite_errors_linear_absolute (V)
  8. L44
    specialize cf_approximation_opposite_errors_linear_absolute (E)
  9. L45
    specialize cf_approximation_opposite_errors_linear_absolute (F)
  10. L46
    specialize cf_approximation_opposite_errors_linear_absolute (c)
07Use earlier factsL47–49

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

  1. L47
    specialize cf_approximation_opposite_errors_linear_absolute (d)
  2. L48
    apply cf_approximation_opposite_errors_linear_absolute
  3. L49
    exact he

Library-wide reading audit

Original defined command ledger · 49 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 c
  13. 0013intro d
  14. 0014intro he
  15. 0015intro hc
  16. 0016have hb : (a * t + b * rn) + (c * (b * u) + d * (a * V)) = (c * (a * v) + d * (b * U)) + (b * rp)
  17. 0017specialize cf_approximation_subtract_previous_error_balance (a)
  18. 0018specialize cf_approximation_subtract_previous_error_balance (b)
  19. 0019specialize cf_approximation_subtract_previous_error_balance (u)
  20. 0020specialize cf_approximation_subtract_previous_error_balance (U)
  21. 0021specialize cf_approximation_subtract_previous_error_balance (v)
  22. 0022specialize cf_approximation_subtract_previous_error_balance (V)
  23. 0023specialize cf_approximation_subtract_previous_error_balance (rp)
  24. 0024specialize cf_approximation_subtract_previous_error_balance (rn)
  25. 0025specialize cf_approximation_subtract_previous_error_balance (t)
  26. 0026specialize cf_approximation_subtract_previous_error_balance (c)
  27. 0027specialize cf_approximation_subtract_previous_error_balance (d)
  28. 0028apply cf_approximation_subtract_previous_error_balance
  29. 0029exact hc
  30. 0030specialize matrix_lattice_absolute_difference_integer_transport (c * (a * v) + d * (b * U))
  31. 0031specialize matrix_lattice_absolute_difference_integer_transport (c * (b * u) + d * (a * V))
  32. 0032specialize matrix_lattice_absolute_difference_integer_transport (a * t + b * rn)
  33. 0033specialize matrix_lattice_absolute_difference_integer_transport (b * rp)
  34. 0034specialize matrix_lattice_absolute_difference_integer_transport (c * E + d * F)
  35. 0035apply matrix_lattice_absolute_difference_integer_transport
  36. 0036symm
  37. 0037exact hb
  38. 0038specialize cf_approximation_opposite_errors_linear_absolute (a)
  39. 0039specialize cf_approximation_opposite_errors_linear_absolute (b)
  40. 0040specialize cf_approximation_opposite_errors_linear_absolute (u)
  41. 0041specialize cf_approximation_opposite_errors_linear_absolute (U)
  42. 0042specialize cf_approximation_opposite_errors_linear_absolute (v)
  43. 0043specialize cf_approximation_opposite_errors_linear_absolute (V)
  44. 0044specialize cf_approximation_opposite_errors_linear_absolute (E)
  45. 0045specialize cf_approximation_opposite_errors_linear_absolute (F)
  46. 0046specialize cf_approximation_opposite_errors_linear_absolute (c)
  47. 0047specialize cf_approximation_opposite_errors_linear_absolute (d)
  48. 0048apply cf_approximation_opposite_errors_linear_absolute
  49. 0049exact he