BA0031

cf_convergent_matrix_state_unique

Every beta index of the genuine convergent computation has unique decoded quotient-list and matrix entries.

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

∀ h. ∀ e. ∀ j. ∀ s. ∀ u. ∀ U. ∀ v. ∀ V. ∀ t. ∀ a. ∀ b. ∀ c. ∀ d. ConvergentMatrixAt(h,e,j,s,u,U,v,V) → ConvergentMatrixAt(h,e,j,t,a,b,c,d) → s = t ∧ (u = a ∧ (U = b ∧ (v = c ∧ V = d)))

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

Definition DAG

ConvergentMatrixAt(h,e,j,s,u,U,v,V) · 2

Actual proof prerequisites

beta_at_unique · checked external prerequisitecf_convergent_state_code_injective
Original expanded first-order statement 
forall h e j s u U v V t a b c d. (exists cfc_state_at_unique_one. ((exists cfc_left_at_unique_onecode cfc_right_at_unique_onecode cfc_matrix_at_unique_onecode. ((cfc_left_at_unique_onecode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_at_unique_onecode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_at_unique_onecode = ((cfc_left_at_unique_onecode) + (cfc_right_at_unique_onecode)) * S ((cfc_left_at_unique_onecode) + (cfc_right_at_unique_onecode)) + ((cfc_right_at_unique_onecode) + (cfc_right_at_unique_onecode))) /\ ((cfc_state_at_unique_one) = ((s) + (cfc_matrix_at_unique_onecode)) * S ((s) + (cfc_matrix_at_unique_onecode)) + ((cfc_matrix_at_unique_onecode) + (cfc_matrix_at_unique_onecode))))))) /\ (((exists ff_h_at_unique_oneentry. ff_h_at_unique_oneentry + S (cfc_state_at_unique_one) = S ((S (j)) * e)) /\ exists ff_q_at_unique_oneentry. h = ff_q_at_unique_oneentry * S ((S (j)) * e) + (cfc_state_at_unique_one))))) -> (exists cfc_state_at_unique_two. ((exists cfc_left_at_unique_twocode cfc_right_at_unique_twocode cfc_matrix_at_unique_twocode. ((cfc_left_at_unique_twocode = ((a) + (b)) * S ((a) + (b)) + ((b) + (b))) /\ ((cfc_right_at_unique_twocode = ((c) + (d)) * S ((c) + (d)) + ((d) + (d))) /\ ((cfc_matrix_at_unique_twocode = ((cfc_left_at_unique_twocode) + (cfc_right_at_unique_twocode)) * S ((cfc_left_at_unique_twocode) + (cfc_right_at_unique_twocode)) + ((cfc_right_at_unique_twocode) + (cfc_right_at_unique_twocode))) /\ ((cfc_state_at_unique_two) = ((t) + (cfc_matrix_at_unique_twocode)) * S ((t) + (cfc_matrix_at_unique_twocode)) + ((cfc_matrix_at_unique_twocode) + (cfc_matrix_at_unique_twocode))))))) /\ (((exists ff_h_at_unique_twoentry. ff_h_at_unique_twoentry + S (cfc_state_at_unique_two) = S ((S (j)) * e)) /\ exists ff_q_at_unique_twoentry. h = ff_q_at_unique_twoentry * S ((S (j)) * e) + (cfc_state_at_unique_two))))) -> ((s = t) /\ ((u = a) /\ ((U = b) /\ ((v = c) /\ (V = d)))))

Complete tactic proof in conservative notation

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

43 script commands · 8 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 (1)
cf convergent state code injective
01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    intro b
  2. L12
    intro c
  3. L13
    intro d
  4. L14
    intro h1
  5. L15
    intro h2
03Separate the logical casesL16–19

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

  1. L16
    cases h1
  2. L17
    cases h2
  3. L18
    cases h1_witness
  4. L19
    cases h2_witness
04Establish hzL20–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L20
    have hz : x = x1
  2. L21
    specialize beta_at_unique (h)
  3. L22
    specialize beta_at_unique (e)
  4. L23
    specialize beta_at_unique (j)
  5. L24
    specialize beta_at_unique (x)
  6. L25
    specialize beta_at_unique (x1)
  7. L26
    apply beta_at_unique
  8. L27
    exact h1_witness_right
  9. L28
    exact h2_witness_right
  10. L29
    specialize cf_convergent_state_code_injective (s)
05Use earlier factsL30–39

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

  1. L30
    specialize cf_convergent_state_code_injective (u)
  2. L31
    specialize cf_convergent_state_code_injective (U)
  3. L32
    specialize cf_convergent_state_code_injective (v)
  4. L33
    specialize cf_convergent_state_code_injective (V)
  5. L34
    specialize cf_convergent_state_code_injective (t)
  6. L35
    specialize cf_convergent_state_code_injective (a)
  7. L36
    specialize cf_convergent_state_code_injective (b)
  8. L37
    specialize cf_convergent_state_code_injective (c)
  9. L38
    specialize cf_convergent_state_code_injective (d)
  10. L39
    specialize cf_convergent_state_code_injective (x)
06Use earlier factsL40–41

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

  1. L40
    apply cf_convergent_state_code_injective
  2. L41
    exact h1_witness_left
07Calculate and transport equalitiesL42–42

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

  1. L42
    rewrite hz
08Use earlier factsL43–43

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

  1. L43
    exact h2_witness_left

Library-wide reading audit

Original defined command ledger · 43 lines
  1. 0001intro h
  2. 0002intro e
  3. 0003intro j
  4. 0004intro s
  5. 0005intro u
  6. 0006intro U
  7. 0007intro v
  8. 0008intro V
  9. 0009intro t
  10. 0010intro a
  11. 0011intro b
  12. 0012intro c
  13. 0013intro d
  14. 0014intro h1
  15. 0015intro h2
  16. 0016cases h1
  17. 0017cases h2
  18. 0018cases h1_witness
  19. 0019cases h2_witness
  20. 0020have hz : x = x1
  21. 0021specialize beta_at_unique (h)
  22. 0022specialize beta_at_unique (e)
  23. 0023specialize beta_at_unique (j)
  24. 0024specialize beta_at_unique (x)
  25. 0025specialize beta_at_unique (x1)
  26. 0026apply beta_at_unique
  27. 0027exact h1_witness_right
  28. 0028exact h2_witness_right
  29. 0029specialize cf_convergent_state_code_injective (s)
  30. 0030specialize cf_convergent_state_code_injective (u)
  31. 0031specialize cf_convergent_state_code_injective (U)
  32. 0032specialize cf_convergent_state_code_injective (v)
  33. 0033specialize cf_convergent_state_code_injective (V)
  34. 0034specialize cf_convergent_state_code_injective (t)
  35. 0035specialize cf_convergent_state_code_injective (a)
  36. 0036specialize cf_convergent_state_code_injective (b)
  37. 0037specialize cf_convergent_state_code_injective (c)
  38. 0038specialize cf_convergent_state_code_injective (d)
  39. 0039specialize cf_convergent_state_code_injective (x)
  40. 0040apply cf_convergent_state_code_injective
  41. 0041exact h1_witness_left
  42. 0042rewrite hz
  43. 0043exact h2_witness_left