BA0033

cf_convergent_matrix_successor_elimination

Every nonempty actual prefix computation exposes a tagged first quotient and the exact four matrix recurrence equations.

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) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ i. ConvergentMatrixTrace(x,h,e,k,y,z,n,m) ∧ (ListCell(s,i,x) ∧ (u = i · y + n ∧ (U = i · z + m ∧ (v = y ∧ V = z))))

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

Definition DAG

ListCell(s,q,t) · 2ConvergentMatrixAt(h,e,j,s,u,U,v,V) · 2ConvergentMatrixTrace(s,h,e,k,u,U,v,V) · 2

Actual proof prerequisites

cf_convergent_matrix_state_uniquezero_add · checked external prerequisitelt_of_lt_of_le · checked external prerequisitele_succ_self · checked external prerequisite
Original expanded first-order statement 
forall s h e k u U v V. (exists cfc_tail_matrix_successor. ((exists cfc_state_matrix_successorinitial. ((exists cfc_left_matrix_successorinitialcode cfc_right_matrix_successorinitialcode cfc_matrix_matrix_successorinitialcode. ((cfc_left_matrix_successorinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_matrix_successorinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_matrix_successorinitialcode = ((cfc_left_matrix_successorinitialcode) + (cfc_right_matrix_successorinitialcode)) * S ((cfc_left_matrix_successorinitialcode) + (cfc_right_matrix_successorinitialcode)) + ((cfc_right_matrix_successorinitialcode) + (cfc_right_matrix_successorinitialcode))) /\ ((cfc_state_matrix_successorinitial) = ((cfc_tail_matrix_successor) + (cfc_matrix_matrix_successorinitialcode)) * S ((cfc_tail_matrix_successor) + (cfc_matrix_matrix_successorinitialcode)) + ((cfc_matrix_matrix_successorinitialcode) + (cfc_matrix_matrix_successorinitialcode))))))) /\ (((exists ff_h_matrix_successorinitialentry. ff_h_matrix_successorinitialentry + S (cfc_state_matrix_successorinitial) = S ((S (0)) * e)) /\ exists ff_q_matrix_successorinitialentry. h = ff_q_matrix_successorinitialentry * S ((S (0)) * e) + (cfc_state_matrix_successorinitial))))) /\ ((exists cfc_state_matrix_successorterminal. ((exists cfc_left_matrix_successorterminalcode cfc_right_matrix_successorterminalcode cfc_matrix_matrix_successorterminalcode. ((cfc_left_matrix_successorterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_matrix_successorterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_matrix_successorterminalcode = ((cfc_left_matrix_successorterminalcode) + (cfc_right_matrix_successorterminalcode)) * S ((cfc_left_matrix_successorterminalcode) + (cfc_right_matrix_successorterminalcode)) + ((cfc_right_matrix_successorterminalcode) + (cfc_right_matrix_successorterminalcode))) /\ ((cfc_state_matrix_successorterminal) = ((s) + (cfc_matrix_matrix_successorterminalcode)) * S ((s) + (cfc_matrix_matrix_successorterminalcode)) + ((cfc_matrix_matrix_successorterminalcode) + (cfc_matrix_matrix_successorterminalcode))))))) /\ (((exists ff_h_matrix_successorterminalentry. ff_h_matrix_successorterminalentry + S (cfc_state_matrix_successorterminal) = S ((S (S k)) * e)) /\ exists ff_q_matrix_successorterminalentry. h = ff_q_matrix_successorterminalentry * S ((S (S k)) * e) + (cfc_state_matrix_successorterminal))))) /\ (forall cfc_index_matrix_successor. (exists cfba_gap_matrix_successorbound. cfba_gap_matrix_successorbound + S (cfc_index_matrix_successor) = (S k)) -> exists cfc_old_matrix_successor cfc_a_matrix_successor cfc_b_matrix_successor cfc_c_matrix_successor cfc_d_matrix_successor cfc_new_matrix_successor cfc_quotient_matrix_successor. ((exists cfc_state_matrix_successorprevious. ((exists cfc_left_matrix_successorpreviouscode cfc_right_matrix_successorpreviouscode cfc_matrix_matrix_successorpreviouscode. ((cfc_left_matrix_successorpreviouscode = ((cfc_a_matrix_successor) + (cfc_b_matrix_successor)) * S ((cfc_a_matrix_successor) + (cfc_b_matrix_successor)) + ((cfc_b_matrix_successor) + (cfc_b_matrix_successor))) /\ ((cfc_right_matrix_successorpreviouscode = ((cfc_c_matrix_successor) + (cfc_d_matrix_successor)) * S ((cfc_c_matrix_successor) + (cfc_d_matrix_successor)) + ((cfc_d_matrix_successor) + (cfc_d_matrix_successor))) /\ ((cfc_matrix_matrix_successorpreviouscode = ((cfc_left_matrix_successorpreviouscode) + (cfc_right_matrix_successorpreviouscode)) * S ((cfc_left_matrix_successorpreviouscode) + (cfc_right_matrix_successorpreviouscode)) + ((cfc_right_matrix_successorpreviouscode) + (cfc_right_matrix_successorpreviouscode))) /\ ((cfc_state_matrix_successorprevious) = ((cfc_old_matrix_successor) + (cfc_matrix_matrix_successorpreviouscode)) * S ((cfc_old_matrix_successor) + (cfc_matrix_matrix_successorpreviouscode)) + ((cfc_matrix_matrix_successorpreviouscode) + (cfc_matrix_matrix_successorpreviouscode))))))) /\ (((exists ff_h_matrix_successorpreviousentry. ff_h_matrix_successorpreviousentry + S (cfc_state_matrix_successorprevious) = S ((S (cfc_index_matrix_successor)) * e)) /\ exists ff_q_matrix_successorpreviousentry. h = ff_q_matrix_successorpreviousentry * S ((S (cfc_index_matrix_successor)) * e) + (cfc_state_matrix_successorprevious))))) /\ ((exists cfc_state_matrix_successorfollowing. ((exists cfc_left_matrix_successorfollowingcode cfc_right_matrix_successorfollowingcode cfc_matrix_matrix_successorfollowingcode. ((cfc_left_matrix_successorfollowingcode = (((cfc_quotient_matrix_successor * cfc_a_matrix_successor + cfc_c_matrix_successor)) + ((cfc_quotient_matrix_successor * cfc_b_matrix_successor + cfc_d_matrix_successor))) * S (((cfc_quotient_matrix_successor * cfc_a_matrix_successor + cfc_c_matrix_successor)) + ((cfc_quotient_matrix_successor * cfc_b_matrix_successor + cfc_d_matrix_successor))) + (((cfc_quotient_matrix_successor * cfc_b_matrix_successor + cfc_d_matrix_successor)) + ((cfc_quotient_matrix_successor * cfc_b_matrix_successor + cfc_d_matrix_successor)))) /\ ((cfc_right_matrix_successorfollowingcode = ((cfc_a_matrix_successor) + (cfc_b_matrix_successor)) * S ((cfc_a_matrix_successor) + (cfc_b_matrix_successor)) + ((cfc_b_matrix_successor) + (cfc_b_matrix_successor))) /\ ((cfc_matrix_matrix_successorfollowingcode = ((cfc_left_matrix_successorfollowingcode) + (cfc_right_matrix_successorfollowingcode)) * S ((cfc_left_matrix_successorfollowingcode) + (cfc_right_matrix_successorfollowingcode)) + ((cfc_right_matrix_successorfollowingcode) + (cfc_right_matrix_successorfollowingcode))) /\ ((cfc_state_matrix_successorfollowing) = ((cfc_new_matrix_successor) + (cfc_matrix_matrix_successorfollowingcode)) * S ((cfc_new_matrix_successor) + (cfc_matrix_matrix_successorfollowingcode)) + ((cfc_matrix_matrix_successorfollowingcode) + (cfc_matrix_matrix_successorfollowingcode))))))) /\ (((exists ff_h_matrix_successorfollowingentry. ff_h_matrix_successorfollowingentry + S (cfc_state_matrix_successorfollowing) = S ((S (S cfc_index_matrix_successor)) * e)) /\ exists ff_q_matrix_successorfollowingentry. h = ff_q_matrix_successorfollowingentry * S ((S (S cfc_index_matrix_successor)) * e) + (cfc_state_matrix_successorfollowing))))) /\ (cfc_new_matrix_successor = S ((cfc_quotient_matrix_successor + cfc_old_matrix_successor) * S (cfc_quotient_matrix_successor + cfc_old_matrix_successor) + (cfc_old_matrix_successor + cfc_old_matrix_successor))))))))) -> (exists cfc_tail_matrix_predecessor cfc_a_matrix_predecessor cfc_b_matrix_predecessor cfc_c_matrix_predecessor cfc_d_matrix_predecessor cfc_q_matrix_predecessor. ((exists cfc_tail_matrix_predecessorprefix. ((exists cfc_state_matrix_predecessorprefixinitial. ((exists cfc_left_matrix_predecessorprefixinitialcode cfc_right_matrix_predecessorprefixinitialcode cfc_matrix_matrix_predecessorprefixinitialcode. ((cfc_left_matrix_predecessorprefixinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_matrix_predecessorprefixinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_matrix_predecessorprefixinitialcode = ((cfc_left_matrix_predecessorprefixinitialcode) + (cfc_right_matrix_predecessorprefixinitialcode)) * S ((cfc_left_matrix_predecessorprefixinitialcode) + (cfc_right_matrix_predecessorprefixinitialcode)) + ((cfc_right_matrix_predecessorprefixinitialcode) + (cfc_right_matrix_predecessorprefixinitialcode))) /\ ((cfc_state_matrix_predecessorprefixinitial) = ((cfc_tail_matrix_predecessorprefix) + (cfc_matrix_matrix_predecessorprefixinitialcode)) * S ((cfc_tail_matrix_predecessorprefix) + (cfc_matrix_matrix_predecessorprefixinitialcode)) + ((cfc_matrix_matrix_predecessorprefixinitialcode) + (cfc_matrix_matrix_predecessorprefixinitialcode))))))) /\ (((exists ff_h_matrix_predecessorprefixinitialentry. ff_h_matrix_predecessorprefixinitialentry + S (cfc_state_matrix_predecessorprefixinitial) = S ((S (0)) * e)) /\ exists ff_q_matrix_predecessorprefixinitialentry. h = ff_q_matrix_predecessorprefixinitialentry * S ((S (0)) * e) + (cfc_state_matrix_predecessorprefixinitial))))) /\ ((exists cfc_state_matrix_predecessorprefixterminal. ((exists cfc_left_matrix_predecessorprefixterminalcode cfc_right_matrix_predecessorprefixterminalcode cfc_matrix_matrix_predecessorprefixterminalcode. ((cfc_left_matrix_predecessorprefixterminalcode = ((cfc_a_matrix_predecessor) + (cfc_b_matrix_predecessor)) * S ((cfc_a_matrix_predecessor) + (cfc_b_matrix_predecessor)) + ((cfc_b_matrix_predecessor) + (cfc_b_matrix_predecessor))) /\ ((cfc_right_matrix_predecessorprefixterminalcode = ((cfc_c_matrix_predecessor) + (cfc_d_matrix_predecessor)) * S ((cfc_c_matrix_predecessor) + (cfc_d_matrix_predecessor)) + ((cfc_d_matrix_predecessor) + (cfc_d_matrix_predecessor))) /\ ((cfc_matrix_matrix_predecessorprefixterminalcode = ((cfc_left_matrix_predecessorprefixterminalcode) + (cfc_right_matrix_predecessorprefixterminalcode)) * S ((cfc_left_matrix_predecessorprefixterminalcode) + (cfc_right_matrix_predecessorprefixterminalcode)) + ((cfc_right_matrix_predecessorprefixterminalcode) + (cfc_right_matrix_predecessorprefixterminalcode))) /\ ((cfc_state_matrix_predecessorprefixterminal) = ((cfc_tail_matrix_predecessor) + (cfc_matrix_matrix_predecessorprefixterminalcode)) * S ((cfc_tail_matrix_predecessor) + (cfc_matrix_matrix_predecessorprefixterminalcode)) + ((cfc_matrix_matrix_predecessorprefixterminalcode) + (cfc_matrix_matrix_predecessorprefixterminalcode))))))) /\ (((exists ff_h_matrix_predecessorprefixterminalentry. ff_h_matrix_predecessorprefixterminalentry + S (cfc_state_matrix_predecessorprefixterminal) = S ((S (k)) * e)) /\ exists ff_q_matrix_predecessorprefixterminalentry. h = ff_q_matrix_predecessorprefixterminalentry * S ((S (k)) * e) + (cfc_state_matrix_predecessorprefixterminal))))) /\ (forall cfc_index_matrix_predecessorprefix. (exists cfba_gap_matrix_predecessorprefixbound. cfba_gap_matrix_predecessorprefixbound + S (cfc_index_matrix_predecessorprefix) = (k)) -> exists cfc_old_matrix_predecessorprefix cfc_a_matrix_predecessorprefix cfc_b_matrix_predecessorprefix cfc_c_matrix_predecessorprefix cfc_d_matrix_predecessorprefix cfc_new_matrix_predecessorprefix cfc_quotient_matrix_predecessorprefix. ((exists cfc_state_matrix_predecessorprefixprevious. ((exists cfc_left_matrix_predecessorprefixpreviouscode cfc_right_matrix_predecessorprefixpreviouscode cfc_matrix_matrix_predecessorprefixpreviouscode. ((cfc_left_matrix_predecessorprefixpreviouscode = ((cfc_a_matrix_predecessorprefix) + (cfc_b_matrix_predecessorprefix)) * S ((cfc_a_matrix_predecessorprefix) + (cfc_b_matrix_predecessorprefix)) + ((cfc_b_matrix_predecessorprefix) + (cfc_b_matrix_predecessorprefix))) /\ ((cfc_right_matrix_predecessorprefixpreviouscode = ((cfc_c_matrix_predecessorprefix) + (cfc_d_matrix_predecessorprefix)) * S ((cfc_c_matrix_predecessorprefix) + (cfc_d_matrix_predecessorprefix)) + ((cfc_d_matrix_predecessorprefix) + (cfc_d_matrix_predecessorprefix))) /\ ((cfc_matrix_matrix_predecessorprefixpreviouscode = ((cfc_left_matrix_predecessorprefixpreviouscode) + (cfc_right_matrix_predecessorprefixpreviouscode)) * S ((cfc_left_matrix_predecessorprefixpreviouscode) + (cfc_right_matrix_predecessorprefixpreviouscode)) + ((cfc_right_matrix_predecessorprefixpreviouscode) + (cfc_right_matrix_predecessorprefixpreviouscode))) /\ ((cfc_state_matrix_predecessorprefixprevious) = ((cfc_old_matrix_predecessorprefix) + (cfc_matrix_matrix_predecessorprefixpreviouscode)) * S ((cfc_old_matrix_predecessorprefix) + (cfc_matrix_matrix_predecessorprefixpreviouscode)) + ((cfc_matrix_matrix_predecessorprefixpreviouscode) + (cfc_matrix_matrix_predecessorprefixpreviouscode))))))) /\ (((exists ff_h_matrix_predecessorprefixpreviousentry. ff_h_matrix_predecessorprefixpreviousentry + S (cfc_state_matrix_predecessorprefixprevious) = S ((S (cfc_index_matrix_predecessorprefix)) * e)) /\ exists ff_q_matrix_predecessorprefixpreviousentry. h = ff_q_matrix_predecessorprefixpreviousentry * S ((S (cfc_index_matrix_predecessorprefix)) * e) + (cfc_state_matrix_predecessorprefixprevious))))) /\ ((exists cfc_state_matrix_predecessorprefixfollowing. ((exists cfc_left_matrix_predecessorprefixfollowingcode cfc_right_matrix_predecessorprefixfollowingcode cfc_matrix_matrix_predecessorprefixfollowingcode. ((cfc_left_matrix_predecessorprefixfollowingcode = (((cfc_quotient_matrix_predecessorprefix * cfc_a_matrix_predecessorprefix + cfc_c_matrix_predecessorprefix)) + ((cfc_quotient_matrix_predecessorprefix * cfc_b_matrix_predecessorprefix + cfc_d_matrix_predecessorprefix))) * S (((cfc_quotient_matrix_predecessorprefix * cfc_a_matrix_predecessorprefix + cfc_c_matrix_predecessorprefix)) + ((cfc_quotient_matrix_predecessorprefix * cfc_b_matrix_predecessorprefix + cfc_d_matrix_predecessorprefix))) + (((cfc_quotient_matrix_predecessorprefix * cfc_b_matrix_predecessorprefix + cfc_d_matrix_predecessorprefix)) + ((cfc_quotient_matrix_predecessorprefix * cfc_b_matrix_predecessorprefix + cfc_d_matrix_predecessorprefix)))) /\ ((cfc_right_matrix_predecessorprefixfollowingcode = ((cfc_a_matrix_predecessorprefix) + (cfc_b_matrix_predecessorprefix)) * S ((cfc_a_matrix_predecessorprefix) + (cfc_b_matrix_predecessorprefix)) + ((cfc_b_matrix_predecessorprefix) + (cfc_b_matrix_predecessorprefix))) /\ ((cfc_matrix_matrix_predecessorprefixfollowingcode = ((cfc_left_matrix_predecessorprefixfollowingcode) + (cfc_right_matrix_predecessorprefixfollowingcode)) * S ((cfc_left_matrix_predecessorprefixfollowingcode) + (cfc_right_matrix_predecessorprefixfollowingcode)) + ((cfc_right_matrix_predecessorprefixfollowingcode) + (cfc_right_matrix_predecessorprefixfollowingcode))) /\ ((cfc_state_matrix_predecessorprefixfollowing) = ((cfc_new_matrix_predecessorprefix) + (cfc_matrix_matrix_predecessorprefixfollowingcode)) * S ((cfc_new_matrix_predecessorprefix) + (cfc_matrix_matrix_predecessorprefixfollowingcode)) + ((cfc_matrix_matrix_predecessorprefixfollowingcode) + (cfc_matrix_matrix_predecessorprefixfollowingcode))))))) /\ (((exists ff_h_matrix_predecessorprefixfollowingentry. ff_h_matrix_predecessorprefixfollowingentry + S (cfc_state_matrix_predecessorprefixfollowing) = S ((S (S cfc_index_matrix_predecessorprefix)) * e)) /\ exists ff_q_matrix_predecessorprefixfollowingentry. h = ff_q_matrix_predecessorprefixfollowingentry * S ((S (S cfc_index_matrix_predecessorprefix)) * e) + (cfc_state_matrix_predecessorprefixfollowing))))) /\ (cfc_new_matrix_predecessorprefix = S ((cfc_quotient_matrix_predecessorprefix + cfc_old_matrix_predecessorprefix) * S (cfc_quotient_matrix_predecessorprefix + cfc_old_matrix_predecessorprefix) + (cfc_old_matrix_predecessorprefix + cfc_old_matrix_predecessorprefix))))))))) /\ ((s = S ((cfc_q_matrix_predecessor + cfc_tail_matrix_predecessor) * S (cfc_q_matrix_predecessor + cfc_tail_matrix_predecessor) + (cfc_tail_matrix_predecessor + cfc_tail_matrix_predecessor))) /\ (((u) = cfc_q_matrix_predecessor * cfc_a_matrix_predecessor + cfc_c_matrix_predecessor) /\ (((U) = cfc_q_matrix_predecessor * cfc_b_matrix_predecessor + cfc_d_matrix_predecessor) /\ (((v) = cfc_a_matrix_predecessor) /\ ((V) = cfc_b_matrix_predecessor)))))))

Complete tactic proof in conservative notation

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

80 script commands · 27 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 (1)
cf convergent matrix state unique
01Fix variables and assumptionsL1–9

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
02Separate the logical casesL10–12

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

  1. L10
    cases ht
  2. L11
    cases ht_witness
  3. L12
    cases ht_witness_right
03Establish hsL13–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply ht witness right right.

  1. L13
    have hs · expand full local formula (672 characters)have hs : ∃ cfc_old_matrix_last_step. ∃ cfc_a_matrix_last_step. ∃ cfc_b_matrix_last_step. ∃ cfc_c_matrix_last_step. ∃ cfc_d_matrix_last_step. ∃ cfc_new_matrix_last_step. ∃ cfc_q_matrix_last_step. ConvergentMatrixAt(h,e,k,cfc_old_matrix_last_step,cfc_a_matrix_last_step,cfc_b_matrix_last_step,cfc_c_matrix_last_step,cfc_d_matrix_last_step) ∧ (ConvergentMatrixAt(h,e,S k,cfc_new_matrix_last_step,cfc_q_matrix_last_step · cfc_a_matrix_last_step + cfc_c_matrix_last_step,cfc_q_matrix_last_step · cfc_b_matrix_last_step + cfc_d_matrix_last_step,cfc_a_matrix_last_step,cfc_b_matrix_last_step) ∧ ListCell(cfc_new_matrix_last_step,cfc_q_matrix_last_step,cfc_old_matrix_last_step))
    Definitions: ConvergentMatrixAt(h,e,k,cfc_old_matrix_last_step,cfc_a_matrix_last_step,cfc_b_matrix_last_step,cfc_c_matrix_last_step,cfc_d_matrix_last_step)ConvergentMatrixAt(h,e,S k,cfc_new_matrix_last_step,cfc_q_matrix_last_step · cfc_a_matrix_last_step + cfc_c_matrix_last_step,cfc_q_matrix_last_step · cfc_b_matrix_last_step + cfc_d_matrix_last_step,cfc_a_matrix_last_step,cfc_b_matrix_last_step)ListCell(cfc_new_matrix_last_step,cfc_q_matrix_last_step,cfc_old_matrix_last_step)Original native command in the exact edition
  2. L14
    specialize ht_witness_right_right (k)
  3. L15
    apply ht_witness_right_right
04Construct an explicit witnessL16–16

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

  1. L16
    exists 0
05Use earlier factsL17–17

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

  1. L17
    apply zero_add
06Separate the logical casesL18–26

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

  1. L18
    cases hs
  2. L19
    cases hs_witness
  3. L20
    cases hs_witness_witness
  4. L21
    cases hs_witness_witness_witness
  5. L22
    cases hs_witness_witness_witness_witness
  6. L23
    cases hs_witness_witness_witness_witness_witness
  7. L24
    cases hs_witness_witness_witness_witness_witness_witness
  8. L25
    cases hs_witness_witness_witness_witness_witness_witness_witness
  9. L26
    cases hs_witness_witness_witness_witness_witness_witness_witness_right
07Establish heqL27–36

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

  1. L27
    have heq : ((s = x6) /\ ((u = x7 * x2 + x4) /\ ((U = x7 * x3 + x5) /\ ((v = x2) /\ (V = x3)))))
  2. L28
    specialize cf_convergent_matrix_state_unique (h)
  3. L29
    specialize cf_convergent_matrix_state_unique (e)
  4. L30
    specialize cf_convergent_matrix_state_unique (S k)
  5. L31
    specialize cf_convergent_matrix_state_unique (s)
  6. L32
    specialize cf_convergent_matrix_state_unique (u)
  7. L33
    specialize cf_convergent_matrix_state_unique (U)
  8. L34
    specialize cf_convergent_matrix_state_unique (v)
  9. L35
    specialize cf_convergent_matrix_state_unique (V)
  10. L36
    specialize cf_convergent_matrix_state_unique (x6)
08Use earlier factsL37–43

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

  1. L37
    specialize cf_convergent_matrix_state_unique (x7 * x2 + x4)
  2. L38
    specialize cf_convergent_matrix_state_unique (x7 * x3 + x5)
  3. L39
    specialize cf_convergent_matrix_state_unique (x2)
  4. L40
    specialize cf_convergent_matrix_state_unique (x3)
  5. L41
    apply cf_convergent_matrix_state_unique
  6. L42
    exact ht_witness_right_left
  7. L43
    exact hs_witness_witness_witness_witness_witness_witness_witness_right_left
09Separate the logical casesL44–47

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

  1. L44
    cases heq
  2. L45
    cases heq_right
  3. L46
    cases heq_right_right
  4. L47
    cases heq_right_right_right
10Construct an explicit witnessL48–53

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

  1. L48
    exists x1
  2. L49
    exists x2
  3. L50
    exists x3
  4. L51
    exists x4
  5. L52
    exists x5
  6. L53
    exists x7
11Separate the logical casesL54–54

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

  1. L54
    split
12Construct an explicit witnessL55–55

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

  1. L55
    exists x
13Separate the logical casesL56–56

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

  1. L56
    split
14Use earlier factsL57–57

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

  1. L57
    exact ht_witness_left
15Separate the logical casesL58–58

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

  1. L58
    split
16Use earlier factsL59–59

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

  1. L59
    exact hs_witness_witness_witness_witness_witness_witness_witness_left
17Fix variables and assumptionsL60–61

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

  1. L60
    intro j
  2. L61
    intro hj
18Use earlier factsL62–70

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

  1. L62
    specialize ht_witness_right_right (j)
  2. L63
    apply ht_witness_right_right
  3. L64
    specialize lt_of_lt_of_le (j)
  4. L65
    specialize lt_of_lt_of_le (k)
  5. L66
    specialize lt_of_lt_of_le (S k)
  6. L67
    apply lt_of_lt_of_le
  7. L68
    exact hj
  8. L69
    specialize le_succ_self (k)
  9. L70
    apply le_succ_self
19Separate the logical casesL71–71

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

  1. L71
    split
20Calculate and transport equalitiesL72–72

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

  1. L72
    rewrite heq_left
21Use earlier factsL73–73

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

  1. L73
    exact hs_witness_witness_witness_witness_witness_witness_witness_right_right
22Separate the logical casesL74–74

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

  1. L74
    split
23Use earlier factsL75–75

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

  1. L75
    exact heq_right_left
24Separate the logical casesL76–76

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

  1. L76
    split
25Use earlier factsL77–77

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

  1. L77
    exact heq_right_right_left
26Separate the logical casesL78–78

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

  1. L78
    split
27Use earlier factsL79–80

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

  1. L79
    exact heq_right_right_right_left
  2. L80
    exact heq_right_right_right_right

Library-wide reading audit

Original defined command ledger · 80 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. 0010cases ht
  11. 0011cases ht_witness
  12. 0012cases ht_witness_right
  13. 0013have hs : ∃ cfc_old_matrix_last_step. ∃ cfc_a_matrix_last_step. ∃ cfc_b_matrix_last_step. ∃ cfc_c_matrix_last_step. ∃ cfc_d_matrix_last_step. ∃ cfc_new_matrix_last_step. ∃ cfc_q_matrix_last_step. ConvergentMatrixAt(h,e,k,cfc_old_matrix_last_step,cfc_a_matrix_last_step,cfc_b_matrix_last_step,cfc_c_matrix_last_step,cfc_d_matrix_last_step) ∧ (ConvergentMatrixAt(h,e,S k,cfc_new_matrix_last_step,cfc_q_matrix_last_step · cfc_a_matrix_last_step + cfc_c_matrix_last_step,cfc_q_matrix_last_step · cfc_b_matrix_last_step + cfc_d_matrix_last_step,cfc_a_matrix_last_step,cfc_b_matrix_last_step) ∧ ListCell(cfc_new_matrix_last_step,cfc_q_matrix_last_step,cfc_old_matrix_last_step))
  14. 0014specialize ht_witness_right_right (k)
  15. 0015apply ht_witness_right_right
  16. 0016exists 0
  17. 0017apply zero_add
  18. 0018cases hs
  19. 0019cases hs_witness
  20. 0020cases hs_witness_witness
  21. 0021cases hs_witness_witness_witness
  22. 0022cases hs_witness_witness_witness_witness
  23. 0023cases hs_witness_witness_witness_witness_witness
  24. 0024cases hs_witness_witness_witness_witness_witness_witness
  25. 0025cases hs_witness_witness_witness_witness_witness_witness_witness
  26. 0026cases hs_witness_witness_witness_witness_witness_witness_witness_right
  27. 0027have heq : ((s = x6) /\ ((u = x7 * x2 + x4) /\ ((U = x7 * x3 + x5) /\ ((v = x2) /\ (V = x3)))))
  28. 0028specialize cf_convergent_matrix_state_unique (h)
  29. 0029specialize cf_convergent_matrix_state_unique (e)
  30. 0030specialize cf_convergent_matrix_state_unique (S k)
  31. 0031specialize cf_convergent_matrix_state_unique (s)
  32. 0032specialize cf_convergent_matrix_state_unique (u)
  33. 0033specialize cf_convergent_matrix_state_unique (U)
  34. 0034specialize cf_convergent_matrix_state_unique (v)
  35. 0035specialize cf_convergent_matrix_state_unique (V)
  36. 0036specialize cf_convergent_matrix_state_unique (x6)
  37. 0037specialize cf_convergent_matrix_state_unique (x7 * x2 + x4)
  38. 0038specialize cf_convergent_matrix_state_unique (x7 * x3 + x5)
  39. 0039specialize cf_convergent_matrix_state_unique (x2)
  40. 0040specialize cf_convergent_matrix_state_unique (x3)
  41. 0041apply cf_convergent_matrix_state_unique
  42. 0042exact ht_witness_right_left
  43. 0043exact hs_witness_witness_witness_witness_witness_witness_witness_right_left
  44. 0044cases heq
  45. 0045cases heq_right
  46. 0046cases heq_right_right
  47. 0047cases heq_right_right_right
  48. 0048exists x1
  49. 0049exists x2
  50. 0050exists x3
  51. 0051exists x4
  52. 0052exists x5
  53. 0053exists x7
  54. 0054split
  55. 0055exists x
  56. 0056split
  57. 0057exact ht_witness_left
  58. 0058split
  59. 0059exact hs_witness_witness_witness_witness_witness_witness_witness_left
  60. 0060intro j
  61. 0061intro hj
  62. 0062specialize ht_witness_right_right (j)
  63. 0063apply ht_witness_right_right
  64. 0064specialize lt_of_lt_of_le (j)
  65. 0065specialize lt_of_lt_of_le (k)
  66. 0066specialize lt_of_lt_of_le (S k)
  67. 0067apply lt_of_lt_of_le
  68. 0068exact hj
  69. 0069specialize le_succ_self (k)
  70. 0070apply le_succ_self
  71. 0071split
  72. 0072rewrite heq_left
  73. 0073exact hs_witness_witness_witness_witness_witness_witness_witness_right_right
  74. 0074split
  75. 0075exact heq_right_left
  76. 0076split
  77. 0077exact heq_right_right_left
  78. 0078split
  79. 0079exact heq_right_right_right_left
  80. 0080exact heq_right_right_right_right