BA0023

cf_approximation_subtractive_error_lower_bound

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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.

Exact expanded first-order arithmetic 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))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 55 exact native proof lines.

Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

BA0011 cf_approximation_subtract_previous_absolute_error matrix_lattice_absolute_difference_functional Alpha theorem; checked-use authorized BA001D cf_approximation_positive_coefficient_bound zero_add Stable theorem; checked-use authorized

Direct dependents

BA0024 cf_approximation_unimodular_best_approximation

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 : ((a * t + b * rn) = (b * rp) + (c * E + d * F)) \/ ((b * rp) = (a * t + b * rn) + (c * E + d * F))
  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 exact 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 : ((a * t + b * rn) = (b * rp) + (c * E + d * F)) \/ ((b * rp) = (a * t + b * rn) + (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