BA0031

cf_convergent_matrix_state_unique

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

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

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 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)))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 43 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_unique Stable theorem; checked-use authorized BA0030 cf_convergent_state_code_injective

Direct dependents

BA0032 cf_convergent_matrix_empty_elimination BA0033 cf_convergent_matrix_successor_elimination

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

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.

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 exact 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