BA0043

cf_convergent_initial_matrix_exists

Every actual first quotient cell constructs the exact initial matrix [[q,1],[1,0]], including q=0.

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. ∀ q. ∀ t. ListCell(s,q,t) → ∃ x. ∃ y. ConvergentMatrixTrace(s,x,y,1,q,1,1,0)

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

Definition DAG

ListCell(s,q,t) · 1ConvergentMatrixTrace(s,h,e,k,u,U,v,V) · 3

Actual proof prerequisites

cf_convergent_matrix_empty_existscf_convergent_matrix_prepend_existscf_convergent_matrix_entry_transportzero_add · checked external prerequisite
Original expanded first-order statement 
forall s q t. (s = S ((q + t) * S (q + t) + (t + t))) -> exists h e. (exists cfc_tail_initial_matrix. ((exists cfc_state_initial_matrixinitial. ((exists cfc_left_initial_matrixinitialcode cfc_right_initial_matrixinitialcode cfc_matrix_initial_matrixinitialcode. ((cfc_left_initial_matrixinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_initial_matrixinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_initial_matrixinitialcode = ((cfc_left_initial_matrixinitialcode) + (cfc_right_initial_matrixinitialcode)) * S ((cfc_left_initial_matrixinitialcode) + (cfc_right_initial_matrixinitialcode)) + ((cfc_right_initial_matrixinitialcode) + (cfc_right_initial_matrixinitialcode))) /\ ((cfc_state_initial_matrixinitial) = ((cfc_tail_initial_matrix) + (cfc_matrix_initial_matrixinitialcode)) * S ((cfc_tail_initial_matrix) + (cfc_matrix_initial_matrixinitialcode)) + ((cfc_matrix_initial_matrixinitialcode) + (cfc_matrix_initial_matrixinitialcode))))))) /\ (((exists ff_h_initial_matrixinitialentry. ff_h_initial_matrixinitialentry + S (cfc_state_initial_matrixinitial) = S ((S (0)) * e)) /\ exists ff_q_initial_matrixinitialentry. h = ff_q_initial_matrixinitialentry * S ((S (0)) * e) + (cfc_state_initial_matrixinitial))))) /\ ((exists cfc_state_initial_matrixterminal. ((exists cfc_left_initial_matrixterminalcode cfc_right_initial_matrixterminalcode cfc_matrix_initial_matrixterminalcode. ((cfc_left_initial_matrixterminalcode = ((q) + (1)) * S ((q) + (1)) + ((1) + (1))) /\ ((cfc_right_initial_matrixterminalcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_matrix_initial_matrixterminalcode = ((cfc_left_initial_matrixterminalcode) + (cfc_right_initial_matrixterminalcode)) * S ((cfc_left_initial_matrixterminalcode) + (cfc_right_initial_matrixterminalcode)) + ((cfc_right_initial_matrixterminalcode) + (cfc_right_initial_matrixterminalcode))) /\ ((cfc_state_initial_matrixterminal) = ((s) + (cfc_matrix_initial_matrixterminalcode)) * S ((s) + (cfc_matrix_initial_matrixterminalcode)) + ((cfc_matrix_initial_matrixterminalcode) + (cfc_matrix_initial_matrixterminalcode))))))) /\ (((exists ff_h_initial_matrixterminalentry. ff_h_initial_matrixterminalentry + S (cfc_state_initial_matrixterminal) = S ((S (1)) * e)) /\ exists ff_q_initial_matrixterminalentry. h = ff_q_initial_matrixterminalentry * S ((S (1)) * e) + (cfc_state_initial_matrixterminal))))) /\ (forall cfc_index_initial_matrix. (exists cfba_gap_initial_matrixbound. cfba_gap_initial_matrixbound + S (cfc_index_initial_matrix) = (1)) -> exists cfc_old_initial_matrix cfc_a_initial_matrix cfc_b_initial_matrix cfc_c_initial_matrix cfc_d_initial_matrix cfc_new_initial_matrix cfc_quotient_initial_matrix. ((exists cfc_state_initial_matrixprevious. ((exists cfc_left_initial_matrixpreviouscode cfc_right_initial_matrixpreviouscode cfc_matrix_initial_matrixpreviouscode. ((cfc_left_initial_matrixpreviouscode = ((cfc_a_initial_matrix) + (cfc_b_initial_matrix)) * S ((cfc_a_initial_matrix) + (cfc_b_initial_matrix)) + ((cfc_b_initial_matrix) + (cfc_b_initial_matrix))) /\ ((cfc_right_initial_matrixpreviouscode = ((cfc_c_initial_matrix) + (cfc_d_initial_matrix)) * S ((cfc_c_initial_matrix) + (cfc_d_initial_matrix)) + ((cfc_d_initial_matrix) + (cfc_d_initial_matrix))) /\ ((cfc_matrix_initial_matrixpreviouscode = ((cfc_left_initial_matrixpreviouscode) + (cfc_right_initial_matrixpreviouscode)) * S ((cfc_left_initial_matrixpreviouscode) + (cfc_right_initial_matrixpreviouscode)) + ((cfc_right_initial_matrixpreviouscode) + (cfc_right_initial_matrixpreviouscode))) /\ ((cfc_state_initial_matrixprevious) = ((cfc_old_initial_matrix) + (cfc_matrix_initial_matrixpreviouscode)) * S ((cfc_old_initial_matrix) + (cfc_matrix_initial_matrixpreviouscode)) + ((cfc_matrix_initial_matrixpreviouscode) + (cfc_matrix_initial_matrixpreviouscode))))))) /\ (((exists ff_h_initial_matrixpreviousentry. ff_h_initial_matrixpreviousentry + S (cfc_state_initial_matrixprevious) = S ((S (cfc_index_initial_matrix)) * e)) /\ exists ff_q_initial_matrixpreviousentry. h = ff_q_initial_matrixpreviousentry * S ((S (cfc_index_initial_matrix)) * e) + (cfc_state_initial_matrixprevious))))) /\ ((exists cfc_state_initial_matrixfollowing. ((exists cfc_left_initial_matrixfollowingcode cfc_right_initial_matrixfollowingcode cfc_matrix_initial_matrixfollowingcode. ((cfc_left_initial_matrixfollowingcode = (((cfc_quotient_initial_matrix * cfc_a_initial_matrix + cfc_c_initial_matrix)) + ((cfc_quotient_initial_matrix * cfc_b_initial_matrix + cfc_d_initial_matrix))) * S (((cfc_quotient_initial_matrix * cfc_a_initial_matrix + cfc_c_initial_matrix)) + ((cfc_quotient_initial_matrix * cfc_b_initial_matrix + cfc_d_initial_matrix))) + (((cfc_quotient_initial_matrix * cfc_b_initial_matrix + cfc_d_initial_matrix)) + ((cfc_quotient_initial_matrix * cfc_b_initial_matrix + cfc_d_initial_matrix)))) /\ ((cfc_right_initial_matrixfollowingcode = ((cfc_a_initial_matrix) + (cfc_b_initial_matrix)) * S ((cfc_a_initial_matrix) + (cfc_b_initial_matrix)) + ((cfc_b_initial_matrix) + (cfc_b_initial_matrix))) /\ ((cfc_matrix_initial_matrixfollowingcode = ((cfc_left_initial_matrixfollowingcode) + (cfc_right_initial_matrixfollowingcode)) * S ((cfc_left_initial_matrixfollowingcode) + (cfc_right_initial_matrixfollowingcode)) + ((cfc_right_initial_matrixfollowingcode) + (cfc_right_initial_matrixfollowingcode))) /\ ((cfc_state_initial_matrixfollowing) = ((cfc_new_initial_matrix) + (cfc_matrix_initial_matrixfollowingcode)) * S ((cfc_new_initial_matrix) + (cfc_matrix_initial_matrixfollowingcode)) + ((cfc_matrix_initial_matrixfollowingcode) + (cfc_matrix_initial_matrixfollowingcode))))))) /\ (((exists ff_h_initial_matrixfollowingentry. ff_h_initial_matrixfollowingentry + S (cfc_state_initial_matrixfollowing) = S ((S (S cfc_index_initial_matrix)) * e)) /\ exists ff_q_initial_matrixfollowingentry. h = ff_q_initial_matrixfollowingentry * S ((S (S cfc_index_initial_matrix)) * e) + (cfc_state_initial_matrixfollowing))))) /\ (cfc_new_initial_matrix = S ((cfc_quotient_initial_matrix + cfc_old_initial_matrix) * S (cfc_quotient_initial_matrix + cfc_old_initial_matrix) + (cfc_old_initial_matrix + cfc_old_initial_matrix)))))))))

Complete tactic proof in conservative notation

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

45 script commands · 11 reading checkpoints · 2 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 (3)
cf convergent matrix empty existscf convergent matrix prepend existscf convergent matrix entry transport
01Fix variables and assumptionsL1–4

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

  1. L1
    intro s
  2. L2
    intro q
  3. L3
    intro t
  4. L4
    intro hc
02Establish hzL5–7

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf convergent matrix empty exists.

  1. L5
    have hz : ∃ h. ∃ e. ConvergentMatrixTrace(t,h,e,0,1,0,0,1)Definitions: ConvergentMatrixTrace(t,h,e,0,1,0,0,1)Original native command in the exact edition
  2. L6
    specialize cf_convergent_matrix_empty_exists (t)
  3. L7
    apply cf_convergent_matrix_empty_exists
03Separate the logical casesL8–9

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

  1. L8
    cases hz
  2. L9
    cases hz_witness
04Establish hnL10–19

Establish this local claim before using it. It is not an additional assumption.

  1. L10
    have hn : ∃ h. ∃ e. ConvergentMatrixTrace(s,h,e,1,q · 1 + 0,q · 0 + 1,1,0)Definitions: ConvergentMatrixTrace(s,h,e,1,q · 1 + 0,q · 0 + 1,1,0)Original native command in the exact edition
  2. L11
    specialize cf_convergent_matrix_prepend_exists (t)
  3. L12
    specialize cf_convergent_matrix_prepend_exists (x)
  4. L13
    specialize cf_convergent_matrix_prepend_exists (x1)
  5. L14
    specialize cf_convergent_matrix_prepend_exists (0)
  6. L15
    specialize cf_convergent_matrix_prepend_exists (1)
  7. L16
    specialize cf_convergent_matrix_prepend_exists (0)
  8. L17
    specialize cf_convergent_matrix_prepend_exists (0)
  9. L18
    specialize cf_convergent_matrix_prepend_exists (1)
  10. L19
    specialize cf_convergent_matrix_prepend_exists (q)
05Use earlier factsL20–23

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

  1. L20
    specialize cf_convergent_matrix_prepend_exists (s)
  2. L21
    apply cf_convergent_matrix_prepend_exists
  3. L22
    exact hz_witness_witness
  4. L23
    exact hc
06Separate the logical casesL24–25

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

  1. L24
    cases hn
  2. L25
    cases hn_witness
07Construct an explicit witnessL26–27

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

  1. L26
    exists x2
  2. L27
    exists x3
08Use earlier factsL28–37

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

  1. L28
    specialize cf_convergent_matrix_entry_transport (s)
  2. L29
    specialize cf_convergent_matrix_entry_transport (x2)
  3. L30
    specialize cf_convergent_matrix_entry_transport (x3)
  4. L31
    specialize cf_convergent_matrix_entry_transport (1)
  5. L32
    specialize cf_convergent_matrix_entry_transport (q)
  6. L33
    specialize cf_convergent_matrix_entry_transport (1)
  7. L34
    specialize cf_convergent_matrix_entry_transport (1)
  8. L35
    specialize cf_convergent_matrix_entry_transport (0)
  9. L36
    specialize cf_convergent_matrix_entry_transport ((q * 1 + 0))
  10. L37
    specialize cf_convergent_matrix_entry_transport ((q * 0 + 1))
09Use earlier factsL38–40

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

  1. L38
    specialize cf_convergent_matrix_entry_transport (1)
  2. L39
    specialize cf_convergent_matrix_entry_transport (0)
  3. L40
    apply cf_convergent_matrix_entry_transport
10Calculate and transport equalitiesL41–44

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

  1. L41
    simp [zero_add]
  2. L42
    simp
  3. L43
    refl
  4. L44
    refl
11Use earlier factsL45–45

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

  1. L45
    exact hn_witness_witness

Library-wide reading audit

Original defined command ledger · 45 lines
  1. 0001intro s
  2. 0002intro q
  3. 0003intro t
  4. 0004intro hc
  5. 0005have hz : ∃ h. ∃ e. ConvergentMatrixTrace(t,h,e,0,1,0,0,1)
  6. 0006specialize cf_convergent_matrix_empty_exists (t)
  7. 0007apply cf_convergent_matrix_empty_exists
  8. 0008cases hz
  9. 0009cases hz_witness
  10. 0010have hn : ∃ h. ∃ e. ConvergentMatrixTrace(s,h,e,1,q · 1 + 0,q · 0 + 1,1,0)
  11. 0011specialize cf_convergent_matrix_prepend_exists (t)
  12. 0012specialize cf_convergent_matrix_prepend_exists (x)
  13. 0013specialize cf_convergent_matrix_prepend_exists (x1)
  14. 0014specialize cf_convergent_matrix_prepend_exists (0)
  15. 0015specialize cf_convergent_matrix_prepend_exists (1)
  16. 0016specialize cf_convergent_matrix_prepend_exists (0)
  17. 0017specialize cf_convergent_matrix_prepend_exists (0)
  18. 0018specialize cf_convergent_matrix_prepend_exists (1)
  19. 0019specialize cf_convergent_matrix_prepend_exists (q)
  20. 0020specialize cf_convergent_matrix_prepend_exists (s)
  21. 0021apply cf_convergent_matrix_prepend_exists
  22. 0022exact hz_witness_witness
  23. 0023exact hc
  24. 0024cases hn
  25. 0025cases hn_witness
  26. 0026exists x2
  27. 0027exists x3
  28. 0028specialize cf_convergent_matrix_entry_transport (s)
  29. 0029specialize cf_convergent_matrix_entry_transport (x2)
  30. 0030specialize cf_convergent_matrix_entry_transport (x3)
  31. 0031specialize cf_convergent_matrix_entry_transport (1)
  32. 0032specialize cf_convergent_matrix_entry_transport (q)
  33. 0033specialize cf_convergent_matrix_entry_transport (1)
  34. 0034specialize cf_convergent_matrix_entry_transport (1)
  35. 0035specialize cf_convergent_matrix_entry_transport (0)
  36. 0036specialize cf_convergent_matrix_entry_transport ((q * 1 + 0))
  37. 0037specialize cf_convergent_matrix_entry_transport ((q * 0 + 1))
  38. 0038specialize cf_convergent_matrix_entry_transport (1)
  39. 0039specialize cf_convergent_matrix_entry_transport (0)
  40. 0040apply cf_convergent_matrix_entry_transport
  41. 0041simp [zero_add]
  42. 0042simp
  43. 0043refl
  44. 0044refl
  45. 0045exact hn_witness_witness