BA002F

cf_convergent_state_code_exists

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

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. ∃ z. ConvergentMatrixCode(s,u,U,v,V,z)

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

Definition DAG

NaturalPair(z,a,b) · 4ConvergentMatrixCode(s,u,U,v,V,z) · 1

Actual proof prerequisites

pair_code_constructor · checked external prerequisitecf_convergent_state_code_constructor
Original expanded first-order 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)))))))

Complete tactic proof in conservative notation

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

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.

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 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 : ∃ l. NaturalPair(l,u,U)Definitions: NaturalPair(l,u,U)Original native command in the exact edition
  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 : ∃ r. NaturalPair(r,v,V)Definitions: NaturalPair(r,v,V)Original native command in the exact edition
  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 : ∃ m. NaturalPair(m,x,x1)Definitions: NaturalPair(m,x,x1)Original native command in the exact edition
  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 : ∃ z. NaturalPair(z,s,x2)Definitions: NaturalPair(z,s,x2)Original native command in the exact edition
  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 defined command ledger · 40 lines
  1. 0001intro s
  2. 0002intro u
  3. 0003intro U
  4. 0004intro v
  5. 0005intro V
  6. 0006have hl : ∃ l. NaturalPair(l,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 : ∃ r. NaturalPair(r,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 : ∃ m. NaturalPair(m,x,x1)
  17. 0017specialize pair_code_constructor (x)
  18. 0018specialize pair_code_constructor (x1)
  19. 0019apply pair_code_constructor
  20. 0020cases hm
  21. 0021have hz : ∃ z. NaturalPair(z,s,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