BA0047

cf_convergent_full_matrix_is_exact

HA induction proves the complete quotient product represents the input rational exactly, including the empty zero-divisor boundary and the terminal zero error.

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

∀ k. ∀ a. ∀ b. ∀ s. ∀ h. ∀ e. ∀ H. ∀ E. ∀ u. ∀ U. ∀ v. ∀ V. ContinuedFractionTrace(a,b,s,h,e,k) → ConvergentMatrixTrace(s,H,E,k,u,U,v,V) → a · v = b · u

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

Definition DAG

ContinuedFractionTrace(a,b,s,u,v,ell) · 2ConvergentMatrixTrace(s,h,e,k,u,U,v,V) · 2Lt(a,b) · 1

Actual proof prerequisites

cf_convergent_old_history_zero_eliminationcf_convergent_matrix_empty_eliminationcf_convergent_euclidean_matrix_step_alignmentsucc_injective · checked external prerequisitecf_convergent_old_history_length_transportcf_approximation_exact_value_prepend
Original expanded first-order statement 
forall k a b s h e H E u U v V. (exists cf_gcd_exact_history. ((((exists ff_h_cf_exact_history_initial_state. ff_h_cf_exact_history_initial_state + S (((cf_gcd_exact_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_exact_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * e)) /\ exists ff_q_cf_exact_history_initial_state. h = ff_q_cf_exact_history_initial_state * S ((S (0)) * e) + (((cf_gcd_exact_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_exact_history) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_exact_history_terminal_state. ff_h_cf_exact_history_terminal_state + S (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))) = S ((S (k)) * e)) /\ exists ff_q_cf_exact_history_terminal_state. h = ff_q_cf_exact_history_terminal_state * S ((S (k)) * e) + (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))))) /\ forall cf_index_exact_history. (exists ff_lt_cf_exact_history_index. ff_lt_cf_exact_history_index + S cf_index_exact_history = k) -> exists cf_old_a_exact_history cf_old_b_exact_history cf_tail_exact_history cf_new_a_exact_history cf_new_b_exact_history cf_head_exact_history cf_quotient_exact_history. ((((exists ff_h_cf_exact_history_previous_state. ff_h_cf_exact_history_previous_state + S (((cf_old_a_exact_history) + (((cf_old_b_exact_history) + (cf_tail_exact_history)) * S ((cf_old_b_exact_history) + (cf_tail_exact_history)) + ((cf_tail_exact_history) + (cf_tail_exact_history)))) * S ((cf_old_a_exact_history) + (((cf_old_b_exact_history) + (cf_tail_exact_history)) * S ((cf_old_b_exact_history) + (cf_tail_exact_history)) + ((cf_tail_exact_history) + (cf_tail_exact_history)))) + ((((cf_old_b_exact_history) + (cf_tail_exact_history)) * S ((cf_old_b_exact_history) + (cf_tail_exact_history)) + ((cf_tail_exact_history) + (cf_tail_exact_history))) + (((cf_old_b_exact_history) + (cf_tail_exact_history)) * S ((cf_old_b_exact_history) + (cf_tail_exact_history)) + ((cf_tail_exact_history) + (cf_tail_exact_history))))) = S ((S (cf_index_exact_history)) * e)) /\ exists ff_q_cf_exact_history_previous_state. h = ff_q_cf_exact_history_previous_state * S ((S (cf_index_exact_history)) * e) + (((cf_old_a_exact_history) + (((cf_old_b_exact_history) + (cf_tail_exact_history)) * S ((cf_old_b_exact_history) + (cf_tail_exact_history)) + ((cf_tail_exact_history) + (cf_tail_exact_history)))) * S ((cf_old_a_exact_history) + (((cf_old_b_exact_history) + (cf_tail_exact_history)) * S ((cf_old_b_exact_history) + (cf_tail_exact_history)) + ((cf_tail_exact_history) + (cf_tail_exact_history)))) + ((((cf_old_b_exact_history) + (cf_tail_exact_history)) * S ((cf_old_b_exact_history) + (cf_tail_exact_history)) + ((cf_tail_exact_history) + (cf_tail_exact_history))) + (((cf_old_b_exact_history) + (cf_tail_exact_history)) * S ((cf_old_b_exact_history) + (cf_tail_exact_history)) + ((cf_tail_exact_history) + (cf_tail_exact_history))))))) /\ ((((exists ff_h_cf_exact_history_following_state. ff_h_cf_exact_history_following_state + S (((cf_new_a_exact_history) + (((cf_new_b_exact_history) + (cf_head_exact_history)) * S ((cf_new_b_exact_history) + (cf_head_exact_history)) + ((cf_head_exact_history) + (cf_head_exact_history)))) * S ((cf_new_a_exact_history) + (((cf_new_b_exact_history) + (cf_head_exact_history)) * S ((cf_new_b_exact_history) + (cf_head_exact_history)) + ((cf_head_exact_history) + (cf_head_exact_history)))) + ((((cf_new_b_exact_history) + (cf_head_exact_history)) * S ((cf_new_b_exact_history) + (cf_head_exact_history)) + ((cf_head_exact_history) + (cf_head_exact_history))) + (((cf_new_b_exact_history) + (cf_head_exact_history)) * S ((cf_new_b_exact_history) + (cf_head_exact_history)) + ((cf_head_exact_history) + (cf_head_exact_history))))) = S ((S (S cf_index_exact_history)) * e)) /\ exists ff_q_cf_exact_history_following_state. h = ff_q_cf_exact_history_following_state * S ((S (S cf_index_exact_history)) * e) + (((cf_new_a_exact_history) + (((cf_new_b_exact_history) + (cf_head_exact_history)) * S ((cf_new_b_exact_history) + (cf_head_exact_history)) + ((cf_head_exact_history) + (cf_head_exact_history)))) * S ((cf_new_a_exact_history) + (((cf_new_b_exact_history) + (cf_head_exact_history)) * S ((cf_new_b_exact_history) + (cf_head_exact_history)) + ((cf_head_exact_history) + (cf_head_exact_history)))) + ((((cf_new_b_exact_history) + (cf_head_exact_history)) * S ((cf_new_b_exact_history) + (cf_head_exact_history)) + ((cf_head_exact_history) + (cf_head_exact_history))) + (((cf_new_b_exact_history) + (cf_head_exact_history)) * S ((cf_new_b_exact_history) + (cf_head_exact_history)) + ((cf_head_exact_history) + (cf_head_exact_history))))))) /\ (cf_new_b_exact_history = cf_old_a_exact_history /\ (cf_new_a_exact_history = cf_new_b_exact_history * cf_quotient_exact_history + cf_old_b_exact_history /\ ((exists ff_lt_cf_exact_history_remainder. ff_lt_cf_exact_history_remainder + S cf_old_b_exact_history = cf_new_b_exact_history) /\ (cf_head_exact_history = S ((cf_quotient_exact_history + cf_tail_exact_history) * S (cf_quotient_exact_history + cf_tail_exact_history) + (cf_tail_exact_history + cf_tail_exact_history))))))))))) -> (exists cfc_tail_exact_computation. ((exists cfc_state_exact_computationinitial. ((exists cfc_left_exact_computationinitialcode cfc_right_exact_computationinitialcode cfc_matrix_exact_computationinitialcode. ((cfc_left_exact_computationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_exact_computationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_exact_computationinitialcode = ((cfc_left_exact_computationinitialcode) + (cfc_right_exact_computationinitialcode)) * S ((cfc_left_exact_computationinitialcode) + (cfc_right_exact_computationinitialcode)) + ((cfc_right_exact_computationinitialcode) + (cfc_right_exact_computationinitialcode))) /\ ((cfc_state_exact_computationinitial) = ((cfc_tail_exact_computation) + (cfc_matrix_exact_computationinitialcode)) * S ((cfc_tail_exact_computation) + (cfc_matrix_exact_computationinitialcode)) + ((cfc_matrix_exact_computationinitialcode) + (cfc_matrix_exact_computationinitialcode))))))) /\ (((exists ff_h_exact_computationinitialentry. ff_h_exact_computationinitialentry + S (cfc_state_exact_computationinitial) = S ((S (0)) * E)) /\ exists ff_q_exact_computationinitialentry. H = ff_q_exact_computationinitialentry * S ((S (0)) * E) + (cfc_state_exact_computationinitial))))) /\ ((exists cfc_state_exact_computationterminal. ((exists cfc_left_exact_computationterminalcode cfc_right_exact_computationterminalcode cfc_matrix_exact_computationterminalcode. ((cfc_left_exact_computationterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_exact_computationterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_exact_computationterminalcode = ((cfc_left_exact_computationterminalcode) + (cfc_right_exact_computationterminalcode)) * S ((cfc_left_exact_computationterminalcode) + (cfc_right_exact_computationterminalcode)) + ((cfc_right_exact_computationterminalcode) + (cfc_right_exact_computationterminalcode))) /\ ((cfc_state_exact_computationterminal) = ((s) + (cfc_matrix_exact_computationterminalcode)) * S ((s) + (cfc_matrix_exact_computationterminalcode)) + ((cfc_matrix_exact_computationterminalcode) + (cfc_matrix_exact_computationterminalcode))))))) /\ (((exists ff_h_exact_computationterminalentry. ff_h_exact_computationterminalentry + S (cfc_state_exact_computationterminal) = S ((S (k)) * E)) /\ exists ff_q_exact_computationterminalentry. H = ff_q_exact_computationterminalentry * S ((S (k)) * E) + (cfc_state_exact_computationterminal))))) /\ (forall cfc_index_exact_computation. (exists cfba_gap_exact_computationbound. cfba_gap_exact_computationbound + S (cfc_index_exact_computation) = (k)) -> exists cfc_old_exact_computation cfc_a_exact_computation cfc_b_exact_computation cfc_c_exact_computation cfc_d_exact_computation cfc_new_exact_computation cfc_quotient_exact_computation. ((exists cfc_state_exact_computationprevious. ((exists cfc_left_exact_computationpreviouscode cfc_right_exact_computationpreviouscode cfc_matrix_exact_computationpreviouscode. ((cfc_left_exact_computationpreviouscode = ((cfc_a_exact_computation) + (cfc_b_exact_computation)) * S ((cfc_a_exact_computation) + (cfc_b_exact_computation)) + ((cfc_b_exact_computation) + (cfc_b_exact_computation))) /\ ((cfc_right_exact_computationpreviouscode = ((cfc_c_exact_computation) + (cfc_d_exact_computation)) * S ((cfc_c_exact_computation) + (cfc_d_exact_computation)) + ((cfc_d_exact_computation) + (cfc_d_exact_computation))) /\ ((cfc_matrix_exact_computationpreviouscode = ((cfc_left_exact_computationpreviouscode) + (cfc_right_exact_computationpreviouscode)) * S ((cfc_left_exact_computationpreviouscode) + (cfc_right_exact_computationpreviouscode)) + ((cfc_right_exact_computationpreviouscode) + (cfc_right_exact_computationpreviouscode))) /\ ((cfc_state_exact_computationprevious) = ((cfc_old_exact_computation) + (cfc_matrix_exact_computationpreviouscode)) * S ((cfc_old_exact_computation) + (cfc_matrix_exact_computationpreviouscode)) + ((cfc_matrix_exact_computationpreviouscode) + (cfc_matrix_exact_computationpreviouscode))))))) /\ (((exists ff_h_exact_computationpreviousentry. ff_h_exact_computationpreviousentry + S (cfc_state_exact_computationprevious) = S ((S (cfc_index_exact_computation)) * E)) /\ exists ff_q_exact_computationpreviousentry. H = ff_q_exact_computationpreviousentry * S ((S (cfc_index_exact_computation)) * E) + (cfc_state_exact_computationprevious))))) /\ ((exists cfc_state_exact_computationfollowing. ((exists cfc_left_exact_computationfollowingcode cfc_right_exact_computationfollowingcode cfc_matrix_exact_computationfollowingcode. ((cfc_left_exact_computationfollowingcode = (((cfc_quotient_exact_computation * cfc_a_exact_computation + cfc_c_exact_computation)) + ((cfc_quotient_exact_computation * cfc_b_exact_computation + cfc_d_exact_computation))) * S (((cfc_quotient_exact_computation * cfc_a_exact_computation + cfc_c_exact_computation)) + ((cfc_quotient_exact_computation * cfc_b_exact_computation + cfc_d_exact_computation))) + (((cfc_quotient_exact_computation * cfc_b_exact_computation + cfc_d_exact_computation)) + ((cfc_quotient_exact_computation * cfc_b_exact_computation + cfc_d_exact_computation)))) /\ ((cfc_right_exact_computationfollowingcode = ((cfc_a_exact_computation) + (cfc_b_exact_computation)) * S ((cfc_a_exact_computation) + (cfc_b_exact_computation)) + ((cfc_b_exact_computation) + (cfc_b_exact_computation))) /\ ((cfc_matrix_exact_computationfollowingcode = ((cfc_left_exact_computationfollowingcode) + (cfc_right_exact_computationfollowingcode)) * S ((cfc_left_exact_computationfollowingcode) + (cfc_right_exact_computationfollowingcode)) + ((cfc_right_exact_computationfollowingcode) + (cfc_right_exact_computationfollowingcode))) /\ ((cfc_state_exact_computationfollowing) = ((cfc_new_exact_computation) + (cfc_matrix_exact_computationfollowingcode)) * S ((cfc_new_exact_computation) + (cfc_matrix_exact_computationfollowingcode)) + ((cfc_matrix_exact_computationfollowingcode) + (cfc_matrix_exact_computationfollowingcode))))))) /\ (((exists ff_h_exact_computationfollowingentry. ff_h_exact_computationfollowingentry + S (cfc_state_exact_computationfollowing) = S ((S (S cfc_index_exact_computation)) * E)) /\ exists ff_q_exact_computationfollowingentry. H = ff_q_exact_computationfollowingentry * S ((S (S cfc_index_exact_computation)) * E) + (cfc_state_exact_computationfollowing))))) /\ (cfc_new_exact_computation = S ((cfc_quotient_exact_computation + cfc_old_exact_computation) * S (cfc_quotient_exact_computation + cfc_old_exact_computation) + (cfc_old_exact_computation + cfc_old_exact_computation))))))))) -> a * v = b * u

Complete tactic proof in conservative notation

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

127 script commands · 21 reading checkpoints · 5 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 (5)
cf convergent old history zero eliminationcf convergent matrix empty eliminationcf convergent euclidean matrix step alignmentcf convergent old history length transportcf approximation exact value prepend
01Induction on kL1–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction k
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro s
  5. L5
    intro h
  6. L6
    intro e
  7. L7
    intro H
  8. L8
    intro E
  9. L9
    intro u
  10. L10
    intro U
02Fix variables and assumptionsL11–14

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

  1. L11
    intro v
  2. L12
    intro V
  3. L13
    intro hold
  4. L14
    intro hnew
03Establish hoL15–22

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

  1. L15
    have ho : b = 0 /\ s = 0
  2. L16
    specialize cf_convergent_old_history_zero_elimination (a)
  3. L17
    specialize cf_convergent_old_history_zero_elimination (b)
  4. L18
    specialize cf_convergent_old_history_zero_elimination (s)
  5. L19
    specialize cf_convergent_old_history_zero_elimination (h)
  6. L20
    specialize cf_convergent_old_history_zero_elimination (e)
  7. L21
    apply cf_convergent_old_history_zero_elimination
  8. L22
    exact hold
04Separate the logical casesL23–23

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

  1. L23
    cases ho
05Establish hmL24–33

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

  1. L24
    have hm : ((u = 1) /\ ((U = 0) /\ ((v = 0) /\ (V = 1))))
  2. L25
    specialize cf_convergent_matrix_empty_elimination (s)
  3. L26
    specialize cf_convergent_matrix_empty_elimination (H)
  4. L27
    specialize cf_convergent_matrix_empty_elimination (E)
  5. L28
    specialize cf_convergent_matrix_empty_elimination (u)
  6. L29
    specialize cf_convergent_matrix_empty_elimination (U)
  7. L30
    specialize cf_convergent_matrix_empty_elimination (v)
  8. L31
    specialize cf_convergent_matrix_empty_elimination (V)
  9. L32
    apply cf_convergent_matrix_empty_elimination
  10. L33
    exact hnew
06Separate the logical casesL34–36

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

  1. L34
    cases hm
  2. L35
    cases hm_right
  3. L36
    cases hm_right_right
07Calculate and transport equalitiesL37–40

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

  1. L37
    rewrite ho_left
  2. L38
    rewrite hm_left
  3. L39
    rewrite hm_right_right_left
  4. L40
    simp
08Fix variables and assumptionsL41–50

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

  1. L41
    intro a
  2. L42
    intro b
  3. L43
    intro s
  4. L44
    intro h
  5. L45
    intro e
  6. L46
    intro H
  7. L47
    intro E
  8. L48
    intro u
  9. L49
    intro U
  10. L50
    intro v
09Fix variables and assumptionsL51–53

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

  1. L51
    intro V
  2. L52
    intro hold
  3. L53
    intro hnew
10Establish haL54–63

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

  1. L54
    have ha · expand full local formula (754 characters)have ha : ∃ cfc_r_exact_aligned. ∃ cfc_tail_exact_aligned. ∃ cfc_length_exact_aligned. ∃ cfc_q_exact_aligned. ∃ cfc_p_exact_aligned. ∃ cfc_P_exact_aligned. ∃ cfc_n_exact_aligned. ∃ cfc_N_exact_aligned. S k = S cfc_length_exact_aligned ∧ (a = b · cfc_q_exact_aligned + cfc_r_exact_aligned ∧ (Lt(cfc_r_exact_aligned,b) ∧ (ContinuedFractionTrace(b,cfc_r_exact_aligned,cfc_tail_exact_aligned,h,e,cfc_length_exact_aligned) ∧ (ConvergentMatrixTrace(cfc_tail_exact_aligned,H,E,k,cfc_p_exact_aligned,cfc_P_exact_aligned,cfc_n_exact_aligned,cfc_N_exact_aligned) ∧ (u = cfc_q_exact_aligned · cfc_p_exact_aligned + cfc_n_exact_aligned ∧ (U = cfc_q_exact_aligned · cfc_P_exact_aligned + cfc_N_exact_aligned ∧ (v = cfc_p_exact_aligned ∧ V = cfc_P_exact_aligned)))))))
    Definitions: Lt(cfc_r_exact_aligned,b)ContinuedFractionTrace(b,cfc_r_exact_aligned,cfc_tail_exact_aligned,h,e,cfc_length_exact_aligned)ConvergentMatrixTrace(cfc_tail_exact_aligned,H,E,k,cfc_p_exact_aligned,cfc_P_exact_aligned,cfc_n_exact_aligned,cfc_N_exact_aligned)Original native command in the exact edition
  2. L55
    specialize cf_convergent_euclidean_matrix_step_alignment (a)
  3. L56
    specialize cf_convergent_euclidean_matrix_step_alignment (b)
  4. L57
    specialize cf_convergent_euclidean_matrix_step_alignment (s)
  5. L58
    specialize cf_convergent_euclidean_matrix_step_alignment (h)
  6. L59
    specialize cf_convergent_euclidean_matrix_step_alignment (e)
  7. L60
    specialize cf_convergent_euclidean_matrix_step_alignment (S k)
  8. L61
    specialize cf_convergent_euclidean_matrix_step_alignment (H)
  9. L62
    specialize cf_convergent_euclidean_matrix_step_alignment (E)
  10. L63
    specialize cf_convergent_euclidean_matrix_step_alignment (k)
11Use earlier factsL64–70

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

  1. L64
    specialize cf_convergent_euclidean_matrix_step_alignment (u)
  2. L65
    specialize cf_convergent_euclidean_matrix_step_alignment (U)
  3. L66
    specialize cf_convergent_euclidean_matrix_step_alignment (v)
  4. L67
    specialize cf_convergent_euclidean_matrix_step_alignment (V)
  5. L68
    apply cf_convergent_euclidean_matrix_step_alignment
  6. L69
    exact hold
  7. L70
    exact hnew
12Separate the logical casesL71–80

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

  1. L71
    cases ha
  2. L72
    cases ha_witness
  3. L73
    cases ha_witness_witness
  4. L74
    cases ha_witness_witness_witness
  5. L75
    cases ha_witness_witness_witness_witness
  6. L76
    cases ha_witness_witness_witness_witness_witness
  7. L77
    cases ha_witness_witness_witness_witness_witness_witness
  8. L78
    cases ha_witness_witness_witness_witness_witness_witness_witness
  9. L79
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness
  10. L80
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right
13Separate the logical casesL81–86

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

  1. L81
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  2. L82
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
  3. L83
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  4. L84
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  5. L85
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  6. L86
    cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right
14Establish hkL87–91

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ injective.

  1. L87
    have hk : k = x2
  2. L88
    specialize succ_injective (k)
  3. L89
    specialize succ_injective (x2)
  4. L90
    apply succ_injective
  5. L91
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_left
15Establish hvalueL92–101

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

  1. L92
    have hvalue : b * x6 = x * x4
  2. L93
    specialize IH (b)
  3. L94
    specialize IH (x)
  4. L95
    specialize IH (x1)
  5. L96
    specialize IH (h)
  6. L97
    specialize IH (e)
  7. L98
    specialize IH (H)
  8. L99
    specialize IH (E)
  9. L100
    specialize IH (x4)
  10. L101
    specialize IH (x5)
16Use earlier factsL102–111

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

  1. L102
    specialize IH (x6)
  2. L103
    specialize IH (x7)
  3. L104
    apply IH
  4. L105
    specialize cf_convergent_old_history_length_transport (b)
  5. L106
    specialize cf_convergent_old_history_length_transport (x)
  6. L107
    specialize cf_convergent_old_history_length_transport (x1)
  7. L108
    specialize cf_convergent_old_history_length_transport (h)
  8. L109
    specialize cf_convergent_old_history_length_transport (e)
  9. L110
    specialize cf_convergent_old_history_length_transport (x2)
  10. L111
    specialize cf_convergent_old_history_length_transport (k)
17Use earlier factsL112–112

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

  1. L112
    apply cf_convergent_old_history_length_transport
18Calculate and transport equalitiesL113–113

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

  1. L113
    symm
19Use earlier factsL114–116

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

  1. L114
    exact hk
  2. L115
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  3. L116
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
20Calculate and transport equalitiesL117–118

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

  1. L117
    rewrite ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right_left
  2. L118
    rewrite ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
21Use earlier factsL119–127

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

  1. L119
    specialize cf_approximation_exact_value_prepend (a)
  2. L120
    specialize cf_approximation_exact_value_prepend (b)
  3. L121
    specialize cf_approximation_exact_value_prepend (x3)
  4. L122
    specialize cf_approximation_exact_value_prepend (x)
  5. L123
    specialize cf_approximation_exact_value_prepend (x4)
  6. L124
    specialize cf_approximation_exact_value_prepend (x6)
  7. L125
    apply cf_approximation_exact_value_prepend
  8. L126
    exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  9. L127
    exact hvalue

Library-wide reading audit

Original defined command ledger · 127 lines
  1. 0001induction k
  2. 0002intro a
  3. 0003intro b
  4. 0004intro s
  5. 0005intro h
  6. 0006intro e
  7. 0007intro H
  8. 0008intro E
  9. 0009intro u
  10. 0010intro U
  11. 0011intro v
  12. 0012intro V
  13. 0013intro hold
  14. 0014intro hnew
  15. 0015have ho : b = 0 /\ s = 0
  16. 0016specialize cf_convergent_old_history_zero_elimination (a)
  17. 0017specialize cf_convergent_old_history_zero_elimination (b)
  18. 0018specialize cf_convergent_old_history_zero_elimination (s)
  19. 0019specialize cf_convergent_old_history_zero_elimination (h)
  20. 0020specialize cf_convergent_old_history_zero_elimination (e)
  21. 0021apply cf_convergent_old_history_zero_elimination
  22. 0022exact hold
  23. 0023cases ho
  24. 0024have hm : ((u = 1) /\ ((U = 0) /\ ((v = 0) /\ (V = 1))))
  25. 0025specialize cf_convergent_matrix_empty_elimination (s)
  26. 0026specialize cf_convergent_matrix_empty_elimination (H)
  27. 0027specialize cf_convergent_matrix_empty_elimination (E)
  28. 0028specialize cf_convergent_matrix_empty_elimination (u)
  29. 0029specialize cf_convergent_matrix_empty_elimination (U)
  30. 0030specialize cf_convergent_matrix_empty_elimination (v)
  31. 0031specialize cf_convergent_matrix_empty_elimination (V)
  32. 0032apply cf_convergent_matrix_empty_elimination
  33. 0033exact hnew
  34. 0034cases hm
  35. 0035cases hm_right
  36. 0036cases hm_right_right
  37. 0037rewrite ho_left
  38. 0038rewrite hm_left
  39. 0039rewrite hm_right_right_left
  40. 0040simp
  41. 0041intro a
  42. 0042intro b
  43. 0043intro s
  44. 0044intro h
  45. 0045intro e
  46. 0046intro H
  47. 0047intro E
  48. 0048intro u
  49. 0049intro U
  50. 0050intro v
  51. 0051intro V
  52. 0052intro hold
  53. 0053intro hnew
  54. 0054have ha : ∃ cfc_r_exact_aligned. ∃ cfc_tail_exact_aligned. ∃ cfc_length_exact_aligned. ∃ cfc_q_exact_aligned. ∃ cfc_p_exact_aligned. ∃ cfc_P_exact_aligned. ∃ cfc_n_exact_aligned. ∃ cfc_N_exact_aligned. S k = S cfc_length_exact_aligned ∧ (a = b · cfc_q_exact_aligned + cfc_r_exact_aligned ∧ (Lt(cfc_r_exact_aligned,b) ∧ (ContinuedFractionTrace(b,cfc_r_exact_aligned,cfc_tail_exact_aligned,h,e,cfc_length_exact_aligned) ∧ (ConvergentMatrixTrace(cfc_tail_exact_aligned,H,E,k,cfc_p_exact_aligned,cfc_P_exact_aligned,cfc_n_exact_aligned,cfc_N_exact_aligned) ∧ (u = cfc_q_exact_aligned · cfc_p_exact_aligned + cfc_n_exact_aligned ∧ (U = cfc_q_exact_aligned · cfc_P_exact_aligned + cfc_N_exact_aligned ∧ (v = cfc_p_exact_aligned ∧ V = cfc_P_exact_aligned)))))))
  55. 0055specialize cf_convergent_euclidean_matrix_step_alignment (a)
  56. 0056specialize cf_convergent_euclidean_matrix_step_alignment (b)
  57. 0057specialize cf_convergent_euclidean_matrix_step_alignment (s)
  58. 0058specialize cf_convergent_euclidean_matrix_step_alignment (h)
  59. 0059specialize cf_convergent_euclidean_matrix_step_alignment (e)
  60. 0060specialize cf_convergent_euclidean_matrix_step_alignment (S k)
  61. 0061specialize cf_convergent_euclidean_matrix_step_alignment (H)
  62. 0062specialize cf_convergent_euclidean_matrix_step_alignment (E)
  63. 0063specialize cf_convergent_euclidean_matrix_step_alignment (k)
  64. 0064specialize cf_convergent_euclidean_matrix_step_alignment (u)
  65. 0065specialize cf_convergent_euclidean_matrix_step_alignment (U)
  66. 0066specialize cf_convergent_euclidean_matrix_step_alignment (v)
  67. 0067specialize cf_convergent_euclidean_matrix_step_alignment (V)
  68. 0068apply cf_convergent_euclidean_matrix_step_alignment
  69. 0069exact hold
  70. 0070exact hnew
  71. 0071cases ha
  72. 0072cases ha_witness
  73. 0073cases ha_witness_witness
  74. 0074cases ha_witness_witness_witness
  75. 0075cases ha_witness_witness_witness_witness
  76. 0076cases ha_witness_witness_witness_witness_witness
  77. 0077cases ha_witness_witness_witness_witness_witness_witness
  78. 0078cases ha_witness_witness_witness_witness_witness_witness_witness
  79. 0079cases ha_witness_witness_witness_witness_witness_witness_witness_witness
  80. 0080cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right
  81. 0081cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  82. 0082cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
  83. 0083cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  84. 0084cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  85. 0085cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  86. 0086cases ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right
  87. 0087have hk : k = x2
  88. 0088specialize succ_injective (k)
  89. 0089specialize succ_injective (x2)
  90. 0090apply succ_injective
  91. 0091exact ha_witness_witness_witness_witness_witness_witness_witness_witness_left
  92. 0092have hvalue : b * x6 = x * x4
  93. 0093specialize IH (b)
  94. 0094specialize IH (x)
  95. 0095specialize IH (x1)
  96. 0096specialize IH (h)
  97. 0097specialize IH (e)
  98. 0098specialize IH (H)
  99. 0099specialize IH (E)
  100. 0100specialize IH (x4)
  101. 0101specialize IH (x5)
  102. 0102specialize IH (x6)
  103. 0103specialize IH (x7)
  104. 0104apply IH
  105. 0105specialize cf_convergent_old_history_length_transport (b)
  106. 0106specialize cf_convergent_old_history_length_transport (x)
  107. 0107specialize cf_convergent_old_history_length_transport (x1)
  108. 0108specialize cf_convergent_old_history_length_transport (h)
  109. 0109specialize cf_convergent_old_history_length_transport (e)
  110. 0110specialize cf_convergent_old_history_length_transport (x2)
  111. 0111specialize cf_convergent_old_history_length_transport (k)
  112. 0112apply cf_convergent_old_history_length_transport
  113. 0113symm
  114. 0114exact hk
  115. 0115exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  116. 0116exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  117. 0117rewrite ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right_right_left
  118. 0118rewrite ha_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  119. 0119specialize cf_approximation_exact_value_prepend (a)
  120. 0120specialize cf_approximation_exact_value_prepend (b)
  121. 0121specialize cf_approximation_exact_value_prepend (x3)
  122. 0122specialize cf_approximation_exact_value_prepend (x)
  123. 0123specialize cf_approximation_exact_value_prepend (x4)
  124. 0124specialize cf_approximation_exact_value_prepend (x6)
  125. 0125apply cf_approximation_exact_value_prepend
  126. 0126exact ha_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  127. 0127exact hvalue