BA0030

cf_convergent_state_code_injective

The conservatively shared state code determines every actual quotient-list and matrix coordinate uniquely.

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

∀ s. ∀ u. ∀ U. ∀ v. ∀ V. ∀ t. ∀ a. ∀ b. ∀ c. ∀ d. ∀ z. ConvergentMatrixCode(s,u,U,v,V,z) → ConvergentMatrixCode(t,a,b,c,d,z) → s = t ∧ (u = a ∧ (U = b ∧ (v = c ∧ V = d)))

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

Definition DAG

ConvergentMatrixCode(s,u,U,v,V,z) · 2

Actual proof prerequisites

pair_code_injective · checked external prerequisite
Original expanded first-order statement 
forall s u U v V t a b c d z. (exists cfc_left_code_unique_one cfc_right_code_unique_one cfc_matrix_code_unique_one. ((cfc_left_code_unique_one = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_code_unique_one = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_code_unique_one = ((cfc_left_code_unique_one) + (cfc_right_code_unique_one)) * S ((cfc_left_code_unique_one) + (cfc_right_code_unique_one)) + ((cfc_right_code_unique_one) + (cfc_right_code_unique_one))) /\ ((z) = ((s) + (cfc_matrix_code_unique_one)) * S ((s) + (cfc_matrix_code_unique_one)) + ((cfc_matrix_code_unique_one) + (cfc_matrix_code_unique_one))))))) -> (exists cfc_left_code_unique_two cfc_right_code_unique_two cfc_matrix_code_unique_two. ((cfc_left_code_unique_two = ((a) + (b)) * S ((a) + (b)) + ((b) + (b))) /\ ((cfc_right_code_unique_two = ((c) + (d)) * S ((c) + (d)) + ((d) + (d))) /\ ((cfc_matrix_code_unique_two = ((cfc_left_code_unique_two) + (cfc_right_code_unique_two)) * S ((cfc_left_code_unique_two) + (cfc_right_code_unique_two)) + ((cfc_right_code_unique_two) + (cfc_right_code_unique_two))) /\ ((z) = ((t) + (cfc_matrix_code_unique_two)) * S ((t) + (cfc_matrix_code_unique_two)) + ((cfc_matrix_code_unique_two) + (cfc_matrix_code_unique_two))))))) -> ((s = t) /\ ((u = a) /\ ((U = b) /\ ((v = c) /\ (V = d)))))

Complete tactic proof in conservative notation

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

77 script commands · 20 reading checkpoints · 4 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro s
  2. L2
    intro u
  3. L3
    intro U
  4. L4
    intro v
  5. L5
    intro V
  6. L6
    intro t
  7. L7
    intro a
  8. L8
    intro b
  9. L9
    intro c
  10. L10
    intro d
02Fix variables and assumptionsL11–13

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

  1. L11
    intro z
  2. L12
    intro h1
  3. L13
    intro h2
03Separate the logical casesL14–23

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

  1. L14
    cases h1
  2. L15
    cases h1_witness
  3. L16
    cases h1_witness_witness
  4. L17
    cases h2
  5. L18
    cases h2_witness
  6. L19
    cases h2_witness_witness
  7. L20
    cases h1_witness_witness_witness
  8. L21
    cases h1_witness_witness_witness_right
  9. L22
    cases h1_witness_witness_witness_right_right
  10. L23
    cases h2_witness_witness_witness
04Separate the logical casesL24–25

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

  1. L24
    cases h2_witness_witness_witness_right
  2. L25
    cases h2_witness_witness_witness_right_right
05Establish hoL26–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair code injective.

  1. L26
    have ho : s = t /\ x2 = x5
  2. L27
    specialize pair_code_injective (z)
  3. L28
    specialize pair_code_injective (s)
  4. L29
    specialize pair_code_injective (x2)
  5. L30
    specialize pair_code_injective (t)
  6. L31
    specialize pair_code_injective (x5)
  7. L32
    apply pair_code_injective
  8. L33
    exact h1_witness_witness_witness_right_right_right
  9. L34
    exact h2_witness_witness_witness_right_right_right
06Separate the logical casesL35–35

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

  1. L35
    cases ho
07Establish hmL36–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair code injective.

  1. L36
    have hm : x = x3 /\ x1 = x4
  2. L37
    specialize pair_code_injective (x2)
  3. L38
    specialize pair_code_injective (x)
  4. L39
    specialize pair_code_injective (x1)
  5. L40
    specialize pair_code_injective (x3)
  6. L41
    specialize pair_code_injective (x4)
  7. L42
    apply pair_code_injective
  8. L43
    exact h1_witness_witness_witness_right_right_left
  9. L44
    trans x5
  10. L45
    exact ho_right
08Use earlier factsL46–46

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

  1. L46
    exact h2_witness_witness_witness_right_right_left
09Separate the logical casesL47–47

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

  1. L47
    cases hm
10Establish hlL48–57

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair code injective.

  1. L48
    have hl : u = a /\ U = b
  2. L49
    specialize pair_code_injective (x)
  3. L50
    specialize pair_code_injective (u)
  4. L51
    specialize pair_code_injective (U)
  5. L52
    specialize pair_code_injective (a)
  6. L53
    specialize pair_code_injective (b)
  7. L54
    apply pair_code_injective
  8. L55
    exact h1_witness_witness_witness_left
  9. L56
    trans x3
  10. L57
    exact hm_left
11Use earlier factsL58–58

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

  1. L58
    exact h2_witness_witness_witness_left
12Separate the logical casesL59–59

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

  1. L59
    cases hl
13Establish hrL60–69

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair code injective.

  1. L60
    have hr : v = c /\ V = d
  2. L61
    specialize pair_code_injective (x1)
  3. L62
    specialize pair_code_injective (v)
  4. L63
    specialize pair_code_injective (V)
  5. L64
    specialize pair_code_injective (c)
  6. L65
    specialize pair_code_injective (d)
  7. L66
    apply pair_code_injective
  8. L67
    exact h1_witness_witness_witness_right_left
  9. L68
    trans x4
  10. L69
    exact hm_right
14Use earlier factsL70–70

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

  1. L70
    exact h2_witness_witness_witness_right_left
15Separate the logical casesL71–71

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

  1. L71
    split
16Use earlier factsL72–72

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

  1. L72
    exact ho_left
17Separate the logical casesL73–73

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

  1. L73
    split
18Use earlier factsL74–74

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

  1. L74
    exact hl_left
19Separate the logical casesL75–75

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

  1. L75
    split
20Use earlier factsL76–77

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

  1. L76
    exact hl_right
  2. L77
    exact hr

Library-wide reading audit

Original defined command ledger · 77 lines
  1. 0001intro s
  2. 0002intro u
  3. 0003intro U
  4. 0004intro v
  5. 0005intro V
  6. 0006intro t
  7. 0007intro a
  8. 0008intro b
  9. 0009intro c
  10. 0010intro d
  11. 0011intro z
  12. 0012intro h1
  13. 0013intro h2
  14. 0014cases h1
  15. 0015cases h1_witness
  16. 0016cases h1_witness_witness
  17. 0017cases h2
  18. 0018cases h2_witness
  19. 0019cases h2_witness_witness
  20. 0020cases h1_witness_witness_witness
  21. 0021cases h1_witness_witness_witness_right
  22. 0022cases h1_witness_witness_witness_right_right
  23. 0023cases h2_witness_witness_witness
  24. 0024cases h2_witness_witness_witness_right
  25. 0025cases h2_witness_witness_witness_right_right
  26. 0026have ho : s = t /\ x2 = x5
  27. 0027specialize pair_code_injective (z)
  28. 0028specialize pair_code_injective (s)
  29. 0029specialize pair_code_injective (x2)
  30. 0030specialize pair_code_injective (t)
  31. 0031specialize pair_code_injective (x5)
  32. 0032apply pair_code_injective
  33. 0033exact h1_witness_witness_witness_right_right_right
  34. 0034exact h2_witness_witness_witness_right_right_right
  35. 0035cases ho
  36. 0036have hm : x = x3 /\ x1 = x4
  37. 0037specialize pair_code_injective (x2)
  38. 0038specialize pair_code_injective (x)
  39. 0039specialize pair_code_injective (x1)
  40. 0040specialize pair_code_injective (x3)
  41. 0041specialize pair_code_injective (x4)
  42. 0042apply pair_code_injective
  43. 0043exact h1_witness_witness_witness_right_right_left
  44. 0044trans x5
  45. 0045exact ho_right
  46. 0046exact h2_witness_witness_witness_right_right_left
  47. 0047cases hm
  48. 0048have hl : u = a /\ U = b
  49. 0049specialize pair_code_injective (x)
  50. 0050specialize pair_code_injective (u)
  51. 0051specialize pair_code_injective (U)
  52. 0052specialize pair_code_injective (a)
  53. 0053specialize pair_code_injective (b)
  54. 0054apply pair_code_injective
  55. 0055exact h1_witness_witness_witness_left
  56. 0056trans x3
  57. 0057exact hm_left
  58. 0058exact h2_witness_witness_witness_left
  59. 0059cases hl
  60. 0060have hr : v = c /\ V = d
  61. 0061specialize pair_code_injective (x1)
  62. 0062specialize pair_code_injective (v)
  63. 0063specialize pair_code_injective (V)
  64. 0064specialize pair_code_injective (c)
  65. 0065specialize pair_code_injective (d)
  66. 0066apply pair_code_injective
  67. 0067exact h1_witness_witness_witness_right_left
  68. 0068trans x4
  69. 0069exact hm_right
  70. 0070exact h2_witness_witness_witness_right_left
  71. 0071split
  72. 0072exact ho_left
  73. 0073split
  74. 0074exact hl_left
  75. 0075split
  76. 0076exact hl_right
  77. 0077exact hr