BA0035

cf_convergent_matrix_list_transport

Equality of actual tagged quotient lists transports the finite computation by ordinary substitution.

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

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

Definition DAG

ConvergentMatrixTrace(s,h,e,k,u,U,v,V) · 2

Actual proof prerequisites

none
Original expanded first-order statement 
forall s t h e k u U v V. s = t -> (exists cfc_tail_list_source. ((exists cfc_state_list_sourceinitial. ((exists cfc_left_list_sourceinitialcode cfc_right_list_sourceinitialcode cfc_matrix_list_sourceinitialcode. ((cfc_left_list_sourceinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_list_sourceinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_list_sourceinitialcode = ((cfc_left_list_sourceinitialcode) + (cfc_right_list_sourceinitialcode)) * S ((cfc_left_list_sourceinitialcode) + (cfc_right_list_sourceinitialcode)) + ((cfc_right_list_sourceinitialcode) + (cfc_right_list_sourceinitialcode))) /\ ((cfc_state_list_sourceinitial) = ((cfc_tail_list_source) + (cfc_matrix_list_sourceinitialcode)) * S ((cfc_tail_list_source) + (cfc_matrix_list_sourceinitialcode)) + ((cfc_matrix_list_sourceinitialcode) + (cfc_matrix_list_sourceinitialcode))))))) /\ (((exists ff_h_list_sourceinitialentry. ff_h_list_sourceinitialentry + S (cfc_state_list_sourceinitial) = S ((S (0)) * e)) /\ exists ff_q_list_sourceinitialentry. h = ff_q_list_sourceinitialentry * S ((S (0)) * e) + (cfc_state_list_sourceinitial))))) /\ ((exists cfc_state_list_sourceterminal. ((exists cfc_left_list_sourceterminalcode cfc_right_list_sourceterminalcode cfc_matrix_list_sourceterminalcode. ((cfc_left_list_sourceterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_list_sourceterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_list_sourceterminalcode = ((cfc_left_list_sourceterminalcode) + (cfc_right_list_sourceterminalcode)) * S ((cfc_left_list_sourceterminalcode) + (cfc_right_list_sourceterminalcode)) + ((cfc_right_list_sourceterminalcode) + (cfc_right_list_sourceterminalcode))) /\ ((cfc_state_list_sourceterminal) = ((s) + (cfc_matrix_list_sourceterminalcode)) * S ((s) + (cfc_matrix_list_sourceterminalcode)) + ((cfc_matrix_list_sourceterminalcode) + (cfc_matrix_list_sourceterminalcode))))))) /\ (((exists ff_h_list_sourceterminalentry. ff_h_list_sourceterminalentry + S (cfc_state_list_sourceterminal) = S ((S (k)) * e)) /\ exists ff_q_list_sourceterminalentry. h = ff_q_list_sourceterminalentry * S ((S (k)) * e) + (cfc_state_list_sourceterminal))))) /\ (forall cfc_index_list_source. (exists cfba_gap_list_sourcebound. cfba_gap_list_sourcebound + S (cfc_index_list_source) = (k)) -> exists cfc_old_list_source cfc_a_list_source cfc_b_list_source cfc_c_list_source cfc_d_list_source cfc_new_list_source cfc_quotient_list_source. ((exists cfc_state_list_sourceprevious. ((exists cfc_left_list_sourcepreviouscode cfc_right_list_sourcepreviouscode cfc_matrix_list_sourcepreviouscode. ((cfc_left_list_sourcepreviouscode = ((cfc_a_list_source) + (cfc_b_list_source)) * S ((cfc_a_list_source) + (cfc_b_list_source)) + ((cfc_b_list_source) + (cfc_b_list_source))) /\ ((cfc_right_list_sourcepreviouscode = ((cfc_c_list_source) + (cfc_d_list_source)) * S ((cfc_c_list_source) + (cfc_d_list_source)) + ((cfc_d_list_source) + (cfc_d_list_source))) /\ ((cfc_matrix_list_sourcepreviouscode = ((cfc_left_list_sourcepreviouscode) + (cfc_right_list_sourcepreviouscode)) * S ((cfc_left_list_sourcepreviouscode) + (cfc_right_list_sourcepreviouscode)) + ((cfc_right_list_sourcepreviouscode) + (cfc_right_list_sourcepreviouscode))) /\ ((cfc_state_list_sourceprevious) = ((cfc_old_list_source) + (cfc_matrix_list_sourcepreviouscode)) * S ((cfc_old_list_source) + (cfc_matrix_list_sourcepreviouscode)) + ((cfc_matrix_list_sourcepreviouscode) + (cfc_matrix_list_sourcepreviouscode))))))) /\ (((exists ff_h_list_sourcepreviousentry. ff_h_list_sourcepreviousentry + S (cfc_state_list_sourceprevious) = S ((S (cfc_index_list_source)) * e)) /\ exists ff_q_list_sourcepreviousentry. h = ff_q_list_sourcepreviousentry * S ((S (cfc_index_list_source)) * e) + (cfc_state_list_sourceprevious))))) /\ ((exists cfc_state_list_sourcefollowing. ((exists cfc_left_list_sourcefollowingcode cfc_right_list_sourcefollowingcode cfc_matrix_list_sourcefollowingcode. ((cfc_left_list_sourcefollowingcode = (((cfc_quotient_list_source * cfc_a_list_source + cfc_c_list_source)) + ((cfc_quotient_list_source * cfc_b_list_source + cfc_d_list_source))) * S (((cfc_quotient_list_source * cfc_a_list_source + cfc_c_list_source)) + ((cfc_quotient_list_source * cfc_b_list_source + cfc_d_list_source))) + (((cfc_quotient_list_source * cfc_b_list_source + cfc_d_list_source)) + ((cfc_quotient_list_source * cfc_b_list_source + cfc_d_list_source)))) /\ ((cfc_right_list_sourcefollowingcode = ((cfc_a_list_source) + (cfc_b_list_source)) * S ((cfc_a_list_source) + (cfc_b_list_source)) + ((cfc_b_list_source) + (cfc_b_list_source))) /\ ((cfc_matrix_list_sourcefollowingcode = ((cfc_left_list_sourcefollowingcode) + (cfc_right_list_sourcefollowingcode)) * S ((cfc_left_list_sourcefollowingcode) + (cfc_right_list_sourcefollowingcode)) + ((cfc_right_list_sourcefollowingcode) + (cfc_right_list_sourcefollowingcode))) /\ ((cfc_state_list_sourcefollowing) = ((cfc_new_list_source) + (cfc_matrix_list_sourcefollowingcode)) * S ((cfc_new_list_source) + (cfc_matrix_list_sourcefollowingcode)) + ((cfc_matrix_list_sourcefollowingcode) + (cfc_matrix_list_sourcefollowingcode))))))) /\ (((exists ff_h_list_sourcefollowingentry. ff_h_list_sourcefollowingentry + S (cfc_state_list_sourcefollowing) = S ((S (S cfc_index_list_source)) * e)) /\ exists ff_q_list_sourcefollowingentry. h = ff_q_list_sourcefollowingentry * S ((S (S cfc_index_list_source)) * e) + (cfc_state_list_sourcefollowing))))) /\ (cfc_new_list_source = S ((cfc_quotient_list_source + cfc_old_list_source) * S (cfc_quotient_list_source + cfc_old_list_source) + (cfc_old_list_source + cfc_old_list_source))))))))) -> (exists cfc_tail_list_target. ((exists cfc_state_list_targetinitial. ((exists cfc_left_list_targetinitialcode cfc_right_list_targetinitialcode cfc_matrix_list_targetinitialcode. ((cfc_left_list_targetinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_list_targetinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_list_targetinitialcode = ((cfc_left_list_targetinitialcode) + (cfc_right_list_targetinitialcode)) * S ((cfc_left_list_targetinitialcode) + (cfc_right_list_targetinitialcode)) + ((cfc_right_list_targetinitialcode) + (cfc_right_list_targetinitialcode))) /\ ((cfc_state_list_targetinitial) = ((cfc_tail_list_target) + (cfc_matrix_list_targetinitialcode)) * S ((cfc_tail_list_target) + (cfc_matrix_list_targetinitialcode)) + ((cfc_matrix_list_targetinitialcode) + (cfc_matrix_list_targetinitialcode))))))) /\ (((exists ff_h_list_targetinitialentry. ff_h_list_targetinitialentry + S (cfc_state_list_targetinitial) = S ((S (0)) * e)) /\ exists ff_q_list_targetinitialentry. h = ff_q_list_targetinitialentry * S ((S (0)) * e) + (cfc_state_list_targetinitial))))) /\ ((exists cfc_state_list_targetterminal. ((exists cfc_left_list_targetterminalcode cfc_right_list_targetterminalcode cfc_matrix_list_targetterminalcode. ((cfc_left_list_targetterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_list_targetterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_list_targetterminalcode = ((cfc_left_list_targetterminalcode) + (cfc_right_list_targetterminalcode)) * S ((cfc_left_list_targetterminalcode) + (cfc_right_list_targetterminalcode)) + ((cfc_right_list_targetterminalcode) + (cfc_right_list_targetterminalcode))) /\ ((cfc_state_list_targetterminal) = ((t) + (cfc_matrix_list_targetterminalcode)) * S ((t) + (cfc_matrix_list_targetterminalcode)) + ((cfc_matrix_list_targetterminalcode) + (cfc_matrix_list_targetterminalcode))))))) /\ (((exists ff_h_list_targetterminalentry. ff_h_list_targetterminalentry + S (cfc_state_list_targetterminal) = S ((S (k)) * e)) /\ exists ff_q_list_targetterminalentry. h = ff_q_list_targetterminalentry * S ((S (k)) * e) + (cfc_state_list_targetterminal))))) /\ (forall cfc_index_list_target. (exists cfba_gap_list_targetbound. cfba_gap_list_targetbound + S (cfc_index_list_target) = (k)) -> exists cfc_old_list_target cfc_a_list_target cfc_b_list_target cfc_c_list_target cfc_d_list_target cfc_new_list_target cfc_quotient_list_target. ((exists cfc_state_list_targetprevious. ((exists cfc_left_list_targetpreviouscode cfc_right_list_targetpreviouscode cfc_matrix_list_targetpreviouscode. ((cfc_left_list_targetpreviouscode = ((cfc_a_list_target) + (cfc_b_list_target)) * S ((cfc_a_list_target) + (cfc_b_list_target)) + ((cfc_b_list_target) + (cfc_b_list_target))) /\ ((cfc_right_list_targetpreviouscode = ((cfc_c_list_target) + (cfc_d_list_target)) * S ((cfc_c_list_target) + (cfc_d_list_target)) + ((cfc_d_list_target) + (cfc_d_list_target))) /\ ((cfc_matrix_list_targetpreviouscode = ((cfc_left_list_targetpreviouscode) + (cfc_right_list_targetpreviouscode)) * S ((cfc_left_list_targetpreviouscode) + (cfc_right_list_targetpreviouscode)) + ((cfc_right_list_targetpreviouscode) + (cfc_right_list_targetpreviouscode))) /\ ((cfc_state_list_targetprevious) = ((cfc_old_list_target) + (cfc_matrix_list_targetpreviouscode)) * S ((cfc_old_list_target) + (cfc_matrix_list_targetpreviouscode)) + ((cfc_matrix_list_targetpreviouscode) + (cfc_matrix_list_targetpreviouscode))))))) /\ (((exists ff_h_list_targetpreviousentry. ff_h_list_targetpreviousentry + S (cfc_state_list_targetprevious) = S ((S (cfc_index_list_target)) * e)) /\ exists ff_q_list_targetpreviousentry. h = ff_q_list_targetpreviousentry * S ((S (cfc_index_list_target)) * e) + (cfc_state_list_targetprevious))))) /\ ((exists cfc_state_list_targetfollowing. ((exists cfc_left_list_targetfollowingcode cfc_right_list_targetfollowingcode cfc_matrix_list_targetfollowingcode. ((cfc_left_list_targetfollowingcode = (((cfc_quotient_list_target * cfc_a_list_target + cfc_c_list_target)) + ((cfc_quotient_list_target * cfc_b_list_target + cfc_d_list_target))) * S (((cfc_quotient_list_target * cfc_a_list_target + cfc_c_list_target)) + ((cfc_quotient_list_target * cfc_b_list_target + cfc_d_list_target))) + (((cfc_quotient_list_target * cfc_b_list_target + cfc_d_list_target)) + ((cfc_quotient_list_target * cfc_b_list_target + cfc_d_list_target)))) /\ ((cfc_right_list_targetfollowingcode = ((cfc_a_list_target) + (cfc_b_list_target)) * S ((cfc_a_list_target) + (cfc_b_list_target)) + ((cfc_b_list_target) + (cfc_b_list_target))) /\ ((cfc_matrix_list_targetfollowingcode = ((cfc_left_list_targetfollowingcode) + (cfc_right_list_targetfollowingcode)) * S ((cfc_left_list_targetfollowingcode) + (cfc_right_list_targetfollowingcode)) + ((cfc_right_list_targetfollowingcode) + (cfc_right_list_targetfollowingcode))) /\ ((cfc_state_list_targetfollowing) = ((cfc_new_list_target) + (cfc_matrix_list_targetfollowingcode)) * S ((cfc_new_list_target) + (cfc_matrix_list_targetfollowingcode)) + ((cfc_matrix_list_targetfollowingcode) + (cfc_matrix_list_targetfollowingcode))))))) /\ (((exists ff_h_list_targetfollowingentry. ff_h_list_targetfollowingentry + S (cfc_state_list_targetfollowing) = S ((S (S cfc_index_list_target)) * e)) /\ exists ff_q_list_targetfollowingentry. h = ff_q_list_targetfollowingentry * S ((S (S cfc_index_list_target)) * e) + (cfc_state_list_targetfollowing))))) /\ (cfc_new_list_target = S ((cfc_quotient_list_target + cfc_old_list_target) * S (cfc_quotient_list_target + cfc_old_list_target) + (cfc_old_list_target + cfc_old_list_target)))))))))

Complete tactic proof in conservative notation

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

14 script commands · 4 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro s
  2. L2
    intro t
  3. L3
    intro h
  4. L4
    intro e
  5. L5
    intro k
  6. L6
    intro u
  7. L7
    intro U
  8. L8
    intro v
  9. L9
    intro V
  10. L10
    intro heq
02Fix variables and assumptionsL11–11

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

  1. L11
    intro ht
03Calculate and transport equalitiesL12–13

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

  1. L12
    rewrite <- heq
  2. L13
    rewrite <- heq
04Use earlier factsL14–14

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

  1. L14
    exact ht

Library-wide reading audit

Original defined command ledger · 14 lines
  1. 0001intro s
  2. 0002intro t
  3. 0003intro h
  4. 0004intro e
  5. 0005intro k
  6. 0006intro u
  7. 0007intro U
  8. 0008intro v
  9. 0009intro V
  10. 0010intro heq
  11. 0011intro ht
  12. 0012rewrite <- heq
  13. 0013rewrite <- heq
  14. 0014exact ht