BA0034

cf_convergent_matrix_nonempty_list

A nonempty convergent prefix must consume an actual tagged quotient cell; nil cannot be mistaken for an initial convergent.

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. ∀ h. ∀ e. ∀ k. ∀ u. ∀ U. ∀ v. ∀ V. ConvergentMatrixTrace(s,h,e,S k,u,U,v,V) → ¬s = 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) · 2

Actual proof prerequisites

cf_convergent_matrix_successor_eliminationcell_nonzero · checked external prerequisite
Original expanded first-order statement 
forall s h e k u U v V. (exists cfc_tail_matrix_nonempty. ((exists cfc_state_matrix_nonemptyinitial. ((exists cfc_left_matrix_nonemptyinitialcode cfc_right_matrix_nonemptyinitialcode cfc_matrix_matrix_nonemptyinitialcode. ((cfc_left_matrix_nonemptyinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_matrix_nonemptyinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_matrix_nonemptyinitialcode = ((cfc_left_matrix_nonemptyinitialcode) + (cfc_right_matrix_nonemptyinitialcode)) * S ((cfc_left_matrix_nonemptyinitialcode) + (cfc_right_matrix_nonemptyinitialcode)) + ((cfc_right_matrix_nonemptyinitialcode) + (cfc_right_matrix_nonemptyinitialcode))) /\ ((cfc_state_matrix_nonemptyinitial) = ((cfc_tail_matrix_nonempty) + (cfc_matrix_matrix_nonemptyinitialcode)) * S ((cfc_tail_matrix_nonempty) + (cfc_matrix_matrix_nonemptyinitialcode)) + ((cfc_matrix_matrix_nonemptyinitialcode) + (cfc_matrix_matrix_nonemptyinitialcode))))))) /\ (((exists ff_h_matrix_nonemptyinitialentry. ff_h_matrix_nonemptyinitialentry + S (cfc_state_matrix_nonemptyinitial) = S ((S (0)) * e)) /\ exists ff_q_matrix_nonemptyinitialentry. h = ff_q_matrix_nonemptyinitialentry * S ((S (0)) * e) + (cfc_state_matrix_nonemptyinitial))))) /\ ((exists cfc_state_matrix_nonemptyterminal. ((exists cfc_left_matrix_nonemptyterminalcode cfc_right_matrix_nonemptyterminalcode cfc_matrix_matrix_nonemptyterminalcode. ((cfc_left_matrix_nonemptyterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_matrix_nonemptyterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_matrix_nonemptyterminalcode = ((cfc_left_matrix_nonemptyterminalcode) + (cfc_right_matrix_nonemptyterminalcode)) * S ((cfc_left_matrix_nonemptyterminalcode) + (cfc_right_matrix_nonemptyterminalcode)) + ((cfc_right_matrix_nonemptyterminalcode) + (cfc_right_matrix_nonemptyterminalcode))) /\ ((cfc_state_matrix_nonemptyterminal) = ((s) + (cfc_matrix_matrix_nonemptyterminalcode)) * S ((s) + (cfc_matrix_matrix_nonemptyterminalcode)) + ((cfc_matrix_matrix_nonemptyterminalcode) + (cfc_matrix_matrix_nonemptyterminalcode))))))) /\ (((exists ff_h_matrix_nonemptyterminalentry. ff_h_matrix_nonemptyterminalentry + S (cfc_state_matrix_nonemptyterminal) = S ((S (S k)) * e)) /\ exists ff_q_matrix_nonemptyterminalentry. h = ff_q_matrix_nonemptyterminalentry * S ((S (S k)) * e) + (cfc_state_matrix_nonemptyterminal))))) /\ (forall cfc_index_matrix_nonempty. (exists cfba_gap_matrix_nonemptybound. cfba_gap_matrix_nonemptybound + S (cfc_index_matrix_nonempty) = (S k)) -> exists cfc_old_matrix_nonempty cfc_a_matrix_nonempty cfc_b_matrix_nonempty cfc_c_matrix_nonempty cfc_d_matrix_nonempty cfc_new_matrix_nonempty cfc_quotient_matrix_nonempty. ((exists cfc_state_matrix_nonemptyprevious. ((exists cfc_left_matrix_nonemptypreviouscode cfc_right_matrix_nonemptypreviouscode cfc_matrix_matrix_nonemptypreviouscode. ((cfc_left_matrix_nonemptypreviouscode = ((cfc_a_matrix_nonempty) + (cfc_b_matrix_nonempty)) * S ((cfc_a_matrix_nonempty) + (cfc_b_matrix_nonempty)) + ((cfc_b_matrix_nonempty) + (cfc_b_matrix_nonempty))) /\ ((cfc_right_matrix_nonemptypreviouscode = ((cfc_c_matrix_nonempty) + (cfc_d_matrix_nonempty)) * S ((cfc_c_matrix_nonempty) + (cfc_d_matrix_nonempty)) + ((cfc_d_matrix_nonempty) + (cfc_d_matrix_nonempty))) /\ ((cfc_matrix_matrix_nonemptypreviouscode = ((cfc_left_matrix_nonemptypreviouscode) + (cfc_right_matrix_nonemptypreviouscode)) * S ((cfc_left_matrix_nonemptypreviouscode) + (cfc_right_matrix_nonemptypreviouscode)) + ((cfc_right_matrix_nonemptypreviouscode) + (cfc_right_matrix_nonemptypreviouscode))) /\ ((cfc_state_matrix_nonemptyprevious) = ((cfc_old_matrix_nonempty) + (cfc_matrix_matrix_nonemptypreviouscode)) * S ((cfc_old_matrix_nonempty) + (cfc_matrix_matrix_nonemptypreviouscode)) + ((cfc_matrix_matrix_nonemptypreviouscode) + (cfc_matrix_matrix_nonemptypreviouscode))))))) /\ (((exists ff_h_matrix_nonemptypreviousentry. ff_h_matrix_nonemptypreviousentry + S (cfc_state_matrix_nonemptyprevious) = S ((S (cfc_index_matrix_nonempty)) * e)) /\ exists ff_q_matrix_nonemptypreviousentry. h = ff_q_matrix_nonemptypreviousentry * S ((S (cfc_index_matrix_nonempty)) * e) + (cfc_state_matrix_nonemptyprevious))))) /\ ((exists cfc_state_matrix_nonemptyfollowing. ((exists cfc_left_matrix_nonemptyfollowingcode cfc_right_matrix_nonemptyfollowingcode cfc_matrix_matrix_nonemptyfollowingcode. ((cfc_left_matrix_nonemptyfollowingcode = (((cfc_quotient_matrix_nonempty * cfc_a_matrix_nonempty + cfc_c_matrix_nonempty)) + ((cfc_quotient_matrix_nonempty * cfc_b_matrix_nonempty + cfc_d_matrix_nonempty))) * S (((cfc_quotient_matrix_nonempty * cfc_a_matrix_nonempty + cfc_c_matrix_nonempty)) + ((cfc_quotient_matrix_nonempty * cfc_b_matrix_nonempty + cfc_d_matrix_nonempty))) + (((cfc_quotient_matrix_nonempty * cfc_b_matrix_nonempty + cfc_d_matrix_nonempty)) + ((cfc_quotient_matrix_nonempty * cfc_b_matrix_nonempty + cfc_d_matrix_nonempty)))) /\ ((cfc_right_matrix_nonemptyfollowingcode = ((cfc_a_matrix_nonempty) + (cfc_b_matrix_nonempty)) * S ((cfc_a_matrix_nonempty) + (cfc_b_matrix_nonempty)) + ((cfc_b_matrix_nonempty) + (cfc_b_matrix_nonempty))) /\ ((cfc_matrix_matrix_nonemptyfollowingcode = ((cfc_left_matrix_nonemptyfollowingcode) + (cfc_right_matrix_nonemptyfollowingcode)) * S ((cfc_left_matrix_nonemptyfollowingcode) + (cfc_right_matrix_nonemptyfollowingcode)) + ((cfc_right_matrix_nonemptyfollowingcode) + (cfc_right_matrix_nonemptyfollowingcode))) /\ ((cfc_state_matrix_nonemptyfollowing) = ((cfc_new_matrix_nonempty) + (cfc_matrix_matrix_nonemptyfollowingcode)) * S ((cfc_new_matrix_nonempty) + (cfc_matrix_matrix_nonemptyfollowingcode)) + ((cfc_matrix_matrix_nonemptyfollowingcode) + (cfc_matrix_matrix_nonemptyfollowingcode))))))) /\ (((exists ff_h_matrix_nonemptyfollowingentry. ff_h_matrix_nonemptyfollowingentry + S (cfc_state_matrix_nonemptyfollowing) = S ((S (S cfc_index_matrix_nonempty)) * e)) /\ exists ff_q_matrix_nonemptyfollowingentry. h = ff_q_matrix_nonemptyfollowingentry * S ((S (S cfc_index_matrix_nonempty)) * e) + (cfc_state_matrix_nonemptyfollowing))))) /\ (cfc_new_matrix_nonempty = S ((cfc_quotient_matrix_nonempty + cfc_old_matrix_nonempty) * S (cfc_quotient_matrix_nonempty + cfc_old_matrix_nonempty) + (cfc_old_matrix_nonempty + cfc_old_matrix_nonempty))))))))) -> ~(s = 0)

Complete tactic proof in conservative notation

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

38 script commands · 6 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 matrix successor elimination
01Fix variables and assumptionsL1–10

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

  1. L1
    intro s
  2. L2
    intro h
  3. L3
    intro e
  4. L4
    intro k
  5. L5
    intro u
  6. L6
    intro U
  7. L7
    intro v
  8. L8
    intro V
  9. L9
    intro ht
  10. L10
    intro hz
02Establish hpL11–20

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

  1. L11
    have hp · expand full local formula (686 characters)have hp : ∃ cfc_tail_matrix_nonempty_pred. ∃ cfc_a_matrix_nonempty_pred. ∃ cfc_b_matrix_nonempty_pred. ∃ cfc_c_matrix_nonempty_pred. ∃ cfc_d_matrix_nonempty_pred. ∃ cfc_q_matrix_nonempty_pred. ConvergentMatrixTrace(cfc_tail_matrix_nonempty_pred,h,e,k,cfc_a_matrix_nonempty_pred,cfc_b_matrix_nonempty_pred,cfc_c_matrix_nonempty_pred,cfc_d_matrix_nonempty_pred) ∧ (ListCell(s,cfc_q_matrix_nonempty_pred,cfc_tail_matrix_nonempty_pred) ∧ (u = cfc_q_matrix_nonempty_pred · cfc_a_matrix_nonempty_pred + cfc_c_matrix_nonempty_pred ∧ (U = cfc_q_matrix_nonempty_pred · cfc_b_matrix_nonempty_pred + cfc_d_matrix_nonempty_pred ∧ (v = cfc_a_matrix_nonempty_pred ∧ V = cfc_b_matrix_nonempty_pred))))
    Definitions: ConvergentMatrixTrace(cfc_tail_matrix_nonempty_pred,h,e,k,cfc_a_matrix_nonempty_pred,cfc_b_matrix_nonempty_pred,cfc_c_matrix_nonempty_pred,cfc_d_matrix_nonempty_pred)ListCell(s,cfc_q_matrix_nonempty_pred,cfc_tail_matrix_nonempty_pred)Original native command in the exact edition
  2. L12
    specialize cf_convergent_matrix_successor_elimination (s)
  3. L13
    specialize cf_convergent_matrix_successor_elimination (h)
  4. L14
    specialize cf_convergent_matrix_successor_elimination (e)
  5. L15
    specialize cf_convergent_matrix_successor_elimination (k)
  6. L16
    specialize cf_convergent_matrix_successor_elimination (u)
  7. L17
    specialize cf_convergent_matrix_successor_elimination (U)
  8. L18
    specialize cf_convergent_matrix_successor_elimination (v)
  9. L19
    specialize cf_convergent_matrix_successor_elimination (V)
  10. L20
    apply cf_convergent_matrix_successor_elimination
03Use earlier factsL21–21

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

  1. L21
    exact ht
04Separate the logical casesL22–31

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

  1. L22
    cases hp
  2. L23
    cases hp_witness
  3. L24
    cases hp_witness_witness
  4. L25
    cases hp_witness_witness_witness
  5. L26
    cases hp_witness_witness_witness_witness
  6. L27
    cases hp_witness_witness_witness_witness_witness
  7. L28
    cases hp_witness_witness_witness_witness_witness_witness
  8. L29
    cases hp_witness_witness_witness_witness_witness_witness_right
  9. L30
    cases hp_witness_witness_witness_witness_witness_witness_right_right
  10. L31
    cases hp_witness_witness_witness_witness_witness_witness_right_right_right
05Separate the logical casesL32–32

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

  1. L32
    cases hp_witness_witness_witness_witness_witness_witness_right_right_right_right
06Use earlier factsL33–38

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

  1. L33
    specialize cell_nonzero (s)
  2. L34
    specialize cell_nonzero (x5)
  3. L35
    specialize cell_nonzero (x)
  4. L36
    apply cell_nonzero
  5. L37
    exact hp_witness_witness_witness_witness_witness_witness_right_left
  6. L38
    exact hz

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro s
  2. 0002intro h
  3. 0003intro e
  4. 0004intro k
  5. 0005intro u
  6. 0006intro U
  7. 0007intro v
  8. 0008intro V
  9. 0009intro ht
  10. 0010intro hz
  11. 0011have hp : ∃ cfc_tail_matrix_nonempty_pred. ∃ cfc_a_matrix_nonempty_pred. ∃ cfc_b_matrix_nonempty_pred. ∃ cfc_c_matrix_nonempty_pred. ∃ cfc_d_matrix_nonempty_pred. ∃ cfc_q_matrix_nonempty_pred. ConvergentMatrixTrace(cfc_tail_matrix_nonempty_pred,h,e,k,cfc_a_matrix_nonempty_pred,cfc_b_matrix_nonempty_pred,cfc_c_matrix_nonempty_pred,cfc_d_matrix_nonempty_pred) ∧ (ListCell(s,cfc_q_matrix_nonempty_pred,cfc_tail_matrix_nonempty_pred) ∧ (u = cfc_q_matrix_nonempty_pred · cfc_a_matrix_nonempty_pred + cfc_c_matrix_nonempty_pred ∧ (U = cfc_q_matrix_nonempty_pred · cfc_b_matrix_nonempty_pred + cfc_d_matrix_nonempty_pred ∧ (v = cfc_a_matrix_nonempty_pred ∧ V = cfc_b_matrix_nonempty_pred))))
  12. 0012specialize cf_convergent_matrix_successor_elimination (s)
  13. 0013specialize cf_convergent_matrix_successor_elimination (h)
  14. 0014specialize cf_convergent_matrix_successor_elimination (e)
  15. 0015specialize cf_convergent_matrix_successor_elimination (k)
  16. 0016specialize cf_convergent_matrix_successor_elimination (u)
  17. 0017specialize cf_convergent_matrix_successor_elimination (U)
  18. 0018specialize cf_convergent_matrix_successor_elimination (v)
  19. 0019specialize cf_convergent_matrix_successor_elimination (V)
  20. 0020apply cf_convergent_matrix_successor_elimination
  21. 0021exact ht
  22. 0022cases hp
  23. 0023cases hp_witness
  24. 0024cases hp_witness_witness
  25. 0025cases hp_witness_witness_witness
  26. 0026cases hp_witness_witness_witness_witness
  27. 0027cases hp_witness_witness_witness_witness_witness
  28. 0028cases hp_witness_witness_witness_witness_witness_witness
  29. 0029cases hp_witness_witness_witness_witness_witness_witness_right
  30. 0030cases hp_witness_witness_witness_witness_witness_witness_right_right
  31. 0031cases hp_witness_witness_witness_witness_witness_witness_right_right_right
  32. 0032cases hp_witness_witness_witness_witness_witness_witness_right_right_right_right
  33. 0033specialize cell_nonzero (s)
  34. 0034specialize cell_nonzero (x5)
  35. 0035specialize cell_nonzero (x)
  36. 0036apply cell_nonzero
  37. 0037exact hp_witness_witness_witness_witness_witness_witness_right_left
  38. 0038exact hz