BA002F

cf_convergent_state_code_exists

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

Every actual quotient-list/matrix state has a finite natural code with ordinary pairing witnesses.

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 s u U v V. exists z. (exists cfc_left_state_exists cfc_right_state_exists cfc_matrix_state_exists. ((cfc_left_state_exists = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_state_exists = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_state_exists = ((cfc_left_state_exists) + (cfc_right_state_exists)) * S ((cfc_left_state_exists) + (cfc_right_state_exists)) + ((cfc_right_state_exists) + (cfc_right_state_exists))) /\ ((z) = ((s) + (cfc_matrix_state_exists)) * S ((s) + (cfc_matrix_state_exists)) + ((cfc_matrix_state_exists) + (cfc_matrix_state_exists)))))))

Constructive proof overview

Generated structural guide

Every actual quotient-list/matrix state has a finite natural code with ordinary pairing witnesses.

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

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

Proof neighborhood

Direct dependencies

pair_code_constructor Alpha theorem; checked-use authorized BA002E cf_convergent_state_code_constructor

Direct dependents

BA003A cf_convergent_matrix_empty_exists BA003C cf_convergent_matrix_prepend_exists

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

40 script commands · 12 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.

Named ingredients (1)
cf convergent state code constructor
01Fix variables and assumptionsL1–5

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
02Establish hlL6–9

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

  1. L6
    have hl : exists l. l = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))
  2. L7
    specialize pair_code_constructor (u)
  3. L8
    specialize pair_code_constructor (U)
  4. L9
    apply pair_code_constructor
03Separate the logical casesL10–10

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

  1. L10
    cases hl
04Establish hrL11–14

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

  1. L11
    have hr : exists r. r = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))
  2. L12
    specialize pair_code_constructor (v)
  3. L13
    specialize pair_code_constructor (V)
  4. L14
    apply pair_code_constructor
05Separate the logical casesL15–15

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

  1. L15
    cases hr
06Establish hmL16–19

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

  1. L16
    have hm : exists m. m = ((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1))
  2. L17
    specialize pair_code_constructor (x)
  3. L18
    specialize pair_code_constructor (x1)
  4. L19
    apply pair_code_constructor
07Separate the logical casesL20–20

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

  1. L20
    cases hm
08Establish hzL21–24

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

  1. L21
    have hz : exists z. z = ((s) + (x2)) * S ((s) + (x2)) + ((x2) + (x2))
  2. L22
    specialize pair_code_constructor (s)
  3. L23
    specialize pair_code_constructor (x2)
  4. L24
    apply pair_code_constructor
09Separate the logical casesL25–25

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

  1. L25
    cases hz
10Construct an explicit witnessL26–26

Supply the displayed value, then prove that it has the required property.

  1. L26
    exists x3
11Use earlier factsL27–36

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

  1. L27
    specialize cf_convergent_state_code_constructor (s)
  2. L28
    specialize cf_convergent_state_code_constructor (u)
  3. L29
    specialize cf_convergent_state_code_constructor (U)
  4. L30
    specialize cf_convergent_state_code_constructor (v)
  5. L31
    specialize cf_convergent_state_code_constructor (V)
  6. L32
    specialize cf_convergent_state_code_constructor (x)
  7. L33
    specialize cf_convergent_state_code_constructor (x1)
  8. L34
    specialize cf_convergent_state_code_constructor (x2)
  9. L35
    specialize cf_convergent_state_code_constructor (x3)
  10. L36
    apply cf_convergent_state_code_constructor
12Use earlier factsL37–40

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

  1. L37
    exact hl_witness
  2. L38
    exact hr_witness
  3. L39
    exact hm_witness
  4. L40
    exact hz_witness

Library-wide reading audit

Original exact command ledger · 40 lines
  1. 0001intro s
  2. 0002intro u
  3. 0003intro U
  4. 0004intro v
  5. 0005intro V
  6. 0006have hl : exists l. l = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))
  7. 0007specialize pair_code_constructor (u)
  8. 0008specialize pair_code_constructor (U)
  9. 0009apply pair_code_constructor
  10. 0010cases hl
  11. 0011have hr : exists r. r = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))
  12. 0012specialize pair_code_constructor (v)
  13. 0013specialize pair_code_constructor (V)
  14. 0014apply pair_code_constructor
  15. 0015cases hr
  16. 0016have hm : exists m. m = ((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1))
  17. 0017specialize pair_code_constructor (x)
  18. 0018specialize pair_code_constructor (x1)
  19. 0019apply pair_code_constructor
  20. 0020cases hm
  21. 0021have hz : exists z. z = ((s) + (x2)) * S ((s) + (x2)) + ((x2) + (x2))
  22. 0022specialize pair_code_constructor (s)
  23. 0023specialize pair_code_constructor (x2)
  24. 0024apply pair_code_constructor
  25. 0025cases hz
  26. 0026exists x3
  27. 0027specialize cf_convergent_state_code_constructor (s)
  28. 0028specialize cf_convergent_state_code_constructor (u)
  29. 0029specialize cf_convergent_state_code_constructor (U)
  30. 0030specialize cf_convergent_state_code_constructor (v)
  31. 0031specialize cf_convergent_state_code_constructor (V)
  32. 0032specialize cf_convergent_state_code_constructor (x)
  33. 0033specialize cf_convergent_state_code_constructor (x1)
  34. 0034specialize cf_convergent_state_code_constructor (x2)
  35. 0035specialize cf_convergent_state_code_constructor (x3)
  36. 0036apply cf_convergent_state_code_constructor
  37. 0037exact hl_witness
  38. 0038exact hr_witness
  39. 0039exact hm_witness
  40. 0040exact hz_witness