BA0026

cf_approximation_derived_invariant_best_signed

The derived invariant compares the actual, uniquely determined convergent error with every signed candidate's actual 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. ∀ rp. ∀ rn. ∀ t. ∀ C. ∀ D. ConvergentErrorInvariant(a,b,u,U,v,V) → ¬t = 0 → Lt(t,v) → NaturalAbsDifference(a · v,b · u,C) → RationalApproximationError(a,b,rp,rn,t,D) → Le(C,D)

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

Definition DAG

NaturalAbsDifference(p,n,D) · 1RationalApproximationError(a,b,rp,rn,t,E) · 1ConvergentErrorInvariant(a,b,u,U,v,V) · 1Le(a,b) · 1Lt(a,b) · 1

Actual proof prerequisites

matrix_lattice_absolute_difference_functional · checked external prerequisitecf_approximation_identity_current_absolute_errorcf_approximation_alternating_identity_best_approximationlt_to_le · checked external prerequisite
Original expanded first-order statement 
forall a b u U v V rp rn t C D. (exists cfba_error_derived_comparison cfba_previous_error_derived_comparison. (((((u * V + 1 = U * v) /\ ((a * v = b * u + cfba_error_derived_comparison) /\ (b * U = a * V + cfba_previous_error_derived_comparison)))) \/ (((U * v + 1 = u * V) /\ ((b * u = a * v + cfba_error_derived_comparison) /\ (a * V = b * U + cfba_previous_error_derived_comparison))))) /\ ((exists cfba_gap_derived_comparisondecrease. cfba_gap_derived_comparisondecrease + S (cfba_error_derived_comparison) = (cfba_previous_error_derived_comparison)) /\ (exists cfba_bound_derived_comparisonprevious_bound. cfba_bound_derived_comparisonprevious_bound + (cfba_previous_error_derived_comparison) = (b))))) -> ~(t = 0) -> (exists cfba_gap_derived_comparison_denominator. cfba_gap_derived_comparison_denominator + S (t) = (v)) -> (((a * v) = (b * u) + (C)) \/ ((b * u) = (a * v) + (C))) -> (((a * t + b * rn) = (b * rp) + (D)) \/ ((b * rp) = (a * t + b * rn) + (D))) -> (exists cfba_bound_derived_comparison_result. cfba_bound_derived_comparison_result + (C) = (D))

Complete tactic proof in conservative notation

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

59 script commands · 9 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 identity current absolute errorcf approximation alternating identity best approximation
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 rp
  8. L8
    intro rn
  9. L9
    intro t
  10. L10
    intro C
02Fix variables and assumptionsL11–16

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

  1. L11
    intro D
  2. L12
    intro hi
  3. L13
    intro ht
  4. L14
    intro hlt
  5. L15
    intro hc
  6. L16
    intro hd
03Separate the logical casesL17–20

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

  1. L17
    cases hi
  2. L18
    cases hi_witness
  3. L19
    cases hi_witness_witness
  4. L20
    cases hi_witness_witness_right
04Establish heqL21–30

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

  1. L21
    have heq : C = x
  2. L22
    specialize matrix_lattice_absolute_difference_functional (a * v)
  3. L23
    specialize matrix_lattice_absolute_difference_functional (b * u)
  4. L24
    specialize matrix_lattice_absolute_difference_functional (C)
  5. L25
    specialize matrix_lattice_absolute_difference_functional (x)
  6. L26
    apply matrix_lattice_absolute_difference_functional
  7. L27
    exact hc
  8. L28
    specialize cf_approximation_identity_current_absolute_error (a)
  9. L29
    specialize cf_approximation_identity_current_absolute_error (b)
  10. L30
    specialize cf_approximation_identity_current_absolute_error (u)
05Use earlier factsL31–37

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

  1. L31
    specialize cf_approximation_identity_current_absolute_error (U)
  2. L32
    specialize cf_approximation_identity_current_absolute_error (v)
  3. L33
    specialize cf_approximation_identity_current_absolute_error (V)
  4. L34
    specialize cf_approximation_identity_current_absolute_error (x)
  5. L35
    specialize cf_approximation_identity_current_absolute_error (x1)
  6. L36
    apply cf_approximation_identity_current_absolute_error
  7. L37
    exact hi_witness_witness_left
06Calculate and transport equalitiesL38–38

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

  1. L38
    rewrite heq
07Use earlier factsL39–48

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

  1. L39
    specialize cf_approximation_alternating_identity_best_approximation (a)
  2. L40
    specialize cf_approximation_alternating_identity_best_approximation (b)
  3. L41
    specialize cf_approximation_alternating_identity_best_approximation (u)
  4. L42
    specialize cf_approximation_alternating_identity_best_approximation (U)
  5. L43
    specialize cf_approximation_alternating_identity_best_approximation (v)
  6. L44
    specialize cf_approximation_alternating_identity_best_approximation (V)
  7. L45
    specialize cf_approximation_alternating_identity_best_approximation (x)
  8. L46
    specialize cf_approximation_alternating_identity_best_approximation (x1)
  9. L47
    specialize cf_approximation_alternating_identity_best_approximation (rp)
  10. L48
    specialize cf_approximation_alternating_identity_best_approximation (rn)
08Use earlier factsL49–58

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

  1. L49
    specialize cf_approximation_alternating_identity_best_approximation (t)
  2. L50
    specialize cf_approximation_alternating_identity_best_approximation (D)
  3. L51
    apply cf_approximation_alternating_identity_best_approximation
  4. L52
    exact hi_witness_witness_left
  5. L53
    specialize lt_to_le (x)
  6. L54
    specialize lt_to_le (x1)
  7. L55
    apply lt_to_le
  8. L56
    exact hi_witness_witness_right_left
  9. L57
    exact ht
  10. L58
    exact hlt
09Use earlier factsL59–59

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

  1. L59
    exact hd

Library-wide reading audit

Original defined command ledger · 59 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro u
  4. 0004intro U
  5. 0005intro v
  6. 0006intro V
  7. 0007intro rp
  8. 0008intro rn
  9. 0009intro t
  10. 0010intro C
  11. 0011intro D
  12. 0012intro hi
  13. 0013intro ht
  14. 0014intro hlt
  15. 0015intro hc
  16. 0016intro hd
  17. 0017cases hi
  18. 0018cases hi_witness
  19. 0019cases hi_witness_witness
  20. 0020cases hi_witness_witness_right
  21. 0021have heq : C = x
  22. 0022specialize matrix_lattice_absolute_difference_functional (a * v)
  23. 0023specialize matrix_lattice_absolute_difference_functional (b * u)
  24. 0024specialize matrix_lattice_absolute_difference_functional (C)
  25. 0025specialize matrix_lattice_absolute_difference_functional (x)
  26. 0026apply matrix_lattice_absolute_difference_functional
  27. 0027exact hc
  28. 0028specialize cf_approximation_identity_current_absolute_error (a)
  29. 0029specialize cf_approximation_identity_current_absolute_error (b)
  30. 0030specialize cf_approximation_identity_current_absolute_error (u)
  31. 0031specialize cf_approximation_identity_current_absolute_error (U)
  32. 0032specialize cf_approximation_identity_current_absolute_error (v)
  33. 0033specialize cf_approximation_identity_current_absolute_error (V)
  34. 0034specialize cf_approximation_identity_current_absolute_error (x)
  35. 0035specialize cf_approximation_identity_current_absolute_error (x1)
  36. 0036apply cf_approximation_identity_current_absolute_error
  37. 0037exact hi_witness_witness_left
  38. 0038rewrite heq
  39. 0039specialize cf_approximation_alternating_identity_best_approximation (a)
  40. 0040specialize cf_approximation_alternating_identity_best_approximation (b)
  41. 0041specialize cf_approximation_alternating_identity_best_approximation (u)
  42. 0042specialize cf_approximation_alternating_identity_best_approximation (U)
  43. 0043specialize cf_approximation_alternating_identity_best_approximation (v)
  44. 0044specialize cf_approximation_alternating_identity_best_approximation (V)
  45. 0045specialize cf_approximation_alternating_identity_best_approximation (x)
  46. 0046specialize cf_approximation_alternating_identity_best_approximation (x1)
  47. 0047specialize cf_approximation_alternating_identity_best_approximation (rp)
  48. 0048specialize cf_approximation_alternating_identity_best_approximation (rn)
  49. 0049specialize cf_approximation_alternating_identity_best_approximation (t)
  50. 0050specialize cf_approximation_alternating_identity_best_approximation (D)
  51. 0051apply cf_approximation_alternating_identity_best_approximation
  52. 0052exact hi_witness_witness_left
  53. 0053specialize lt_to_le (x)
  54. 0054specialize lt_to_le (x1)
  55. 0055apply lt_to_le
  56. 0056exact hi_witness_witness_right_left
  57. 0057exact ht
  58. 0058exact hlt
  59. 0059exact hd