BA0023

cf_approximation_subtractive_error_lower_bound

In either subtractive sector, a nonzero current coefficient gives the sharp lower bound for the actual absolute error.

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. ∀ D. ∀ 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 = 0 + c · v → ¬c = 0 → RationalApproximationError(a,b,rp,rn,t,D) → Le(E,D)

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

Definition DAG

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

Actual proof prerequisites

cf_approximation_subtract_previous_absolute_errormatrix_lattice_absolute_difference_functional · checked external prerequisitecf_approximation_positive_coefficient_boundzero_add · checked external prerequisite
Original expanded first-order statement 
forall a b u U v V E F rp rn t D 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) = (0) + (c) * (v)))) -> ~(c = 0) -> (((a * t + b * rn) = (b * rp) + (D)) \/ ((b * rp) = (a * t + b * rn) + (D))) -> (exists cfba_bound_subtractive_bound. cfba_bound_subtractive_bound + (E) = (D))

Complete tactic proof in conservative notation

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

55 script commands · 11 reading checkpoints · 2 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 absolute errorcf approximation positive coefficient bound
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–18

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

  1. L11
    intro t
  2. L12
    intro D
  3. L13
    intro c
  4. L14
    intro d
  5. L15
    intro he
  6. L16
    intro hc
  7. L17
    intro hcpositive
  8. L18
    intro herror
03Separate the logical casesL19–19

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

  1. L19
    cases hc
04Establish hmL20–29

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

  1. L20
    have hm : RationalApproximationError(a,b,rp,rn,t,c · E + d · F)Definitions: RationalApproximationError(a,b,rp,rn,t,c · E + d · F)Original native command in the exact edition
  2. L21
    specialize cf_approximation_subtract_previous_absolute_error (a)
  3. L22
    specialize cf_approximation_subtract_previous_absolute_error (b)
  4. L23
    specialize cf_approximation_subtract_previous_absolute_error (u)
  5. L24
    specialize cf_approximation_subtract_previous_absolute_error (U)
  6. L25
    specialize cf_approximation_subtract_previous_absolute_error (v)
  7. L26
    specialize cf_approximation_subtract_previous_absolute_error (V)
  8. L27
    specialize cf_approximation_subtract_previous_absolute_error (E)
  9. L28
    specialize cf_approximation_subtract_previous_absolute_error (F)
  10. L29
    specialize cf_approximation_subtract_previous_absolute_error (rp)
05Use earlier factsL30–35

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

  1. L30
    specialize cf_approximation_subtract_previous_absolute_error (rn)
  2. L31
    specialize cf_approximation_subtract_previous_absolute_error (t)
  3. L32
    specialize cf_approximation_subtract_previous_absolute_error (c)
  4. L33
    specialize cf_approximation_subtract_previous_absolute_error (d)
  5. L34
    apply cf_approximation_subtract_previous_absolute_error
  6. L35
    exact he
06Separate the logical casesL36–36

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

  1. L36
    split
07Use earlier factsL37–37

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

  1. L37
    exact hc_left
08Calculate and transport equalitiesL38–38

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

  1. L38
    trans 0 + c * v
09Use earlier factsL39–40

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

  1. L39
    exact hc_right
  2. L40
    apply zero_add
10Establish hDL41–50

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix lattice absolute difference functional.

  1. L41
    have hD : D = c * E + d * F
  2. L42
    specialize matrix_lattice_absolute_difference_functional (a * t + b * rn)
  3. L43
    specialize matrix_lattice_absolute_difference_functional (b * rp)
  4. L44
    specialize matrix_lattice_absolute_difference_functional (D)
  5. L45
    specialize matrix_lattice_absolute_difference_functional (c * E + d * F)
  6. L46
    apply matrix_lattice_absolute_difference_functional
  7. L47
    exact herror
  8. L48
    exact hm
  9. L49
    rewrite hD
  10. L50
    specialize cf_approximation_positive_coefficient_bound (E)
11Use earlier factsL51–55

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

  1. L51
    specialize cf_approximation_positive_coefficient_bound (F)
  2. L52
    specialize cf_approximation_positive_coefficient_bound (c)
  3. L53
    specialize cf_approximation_positive_coefficient_bound (d)
  4. L54
    apply cf_approximation_positive_coefficient_bound
  5. L55
    exact hcpositive

Library-wide reading audit

Original defined command ledger · 55 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 c
  14. 0014intro d
  15. 0015intro he
  16. 0016intro hc
  17. 0017intro hcpositive
  18. 0018intro herror
  19. 0019cases hc
  20. 0020have hm : RationalApproximationError(a,b,rp,rn,t,c · E + d · F)
  21. 0021specialize cf_approximation_subtract_previous_absolute_error (a)
  22. 0022specialize cf_approximation_subtract_previous_absolute_error (b)
  23. 0023specialize cf_approximation_subtract_previous_absolute_error (u)
  24. 0024specialize cf_approximation_subtract_previous_absolute_error (U)
  25. 0025specialize cf_approximation_subtract_previous_absolute_error (v)
  26. 0026specialize cf_approximation_subtract_previous_absolute_error (V)
  27. 0027specialize cf_approximation_subtract_previous_absolute_error (E)
  28. 0028specialize cf_approximation_subtract_previous_absolute_error (F)
  29. 0029specialize cf_approximation_subtract_previous_absolute_error (rp)
  30. 0030specialize cf_approximation_subtract_previous_absolute_error (rn)
  31. 0031specialize cf_approximation_subtract_previous_absolute_error (t)
  32. 0032specialize cf_approximation_subtract_previous_absolute_error (c)
  33. 0033specialize cf_approximation_subtract_previous_absolute_error (d)
  34. 0034apply cf_approximation_subtract_previous_absolute_error
  35. 0035exact he
  36. 0036split
  37. 0037exact hc_left
  38. 0038trans 0 + c * v
  39. 0039exact hc_right
  40. 0040apply zero_add
  41. 0041have hD : D = c * E + d * F
  42. 0042specialize matrix_lattice_absolute_difference_functional (a * t + b * rn)
  43. 0043specialize matrix_lattice_absolute_difference_functional (b * rp)
  44. 0044specialize matrix_lattice_absolute_difference_functional (D)
  45. 0045specialize matrix_lattice_absolute_difference_functional (c * E + d * F)
  46. 0046apply matrix_lattice_absolute_difference_functional
  47. 0047exact herror
  48. 0048exact hm
  49. 0049rewrite hD
  50. 0050specialize cf_approximation_positive_coefficient_bound (E)
  51. 0051specialize cf_approximation_positive_coefficient_bound (F)
  52. 0052specialize cf_approximation_positive_coefficient_bound (c)
  53. 0053specialize cf_approximation_positive_coefficient_bound (d)
  54. 0054apply cf_approximation_positive_coefficient_bound
  55. 0055exact hcpositive