BA0046

continued_fraction_initial_zero_over_one

For every positive G071 fraction below one, the genuine initial convergent is 0/1. This checked theorem explicitly corrects the old planning-only numerator-positivity 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

∀ a. ∀ b. ∀ s. ContinuedFraction(a,b,s) → Lt(a,b) → Convergent(s,0,0,1)

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

Definition DAG

ListCell(s,q,t) · 1ContinuedFractionTrace(a,b,s,u,v,ell) · 1ContinuedFraction(a,b,s) · 1Convergent(s,i,u,v) · 1Lt(a,b) · 2

Actual proof prerequisites

cf_convergent_old_history_successor_eliminationdivision_remainder_unique · checked external prerequisitezero_add · checked external prerequisitecf_convergent_numerator_transportcontinued_fraction_first_cell_is_initial_convergent
Original expanded first-order statement 
forall a b s. (exists cf_a_pred_zero_initial_fraction cf_b_pred_zero_initial_fraction cf_code_zero_initial_fraction cf_scale_zero_initial_fraction cf_length_pred_zero_initial_fraction. (a = S cf_a_pred_zero_initial_fraction /\ (b = S cf_b_pred_zero_initial_fraction /\ (exists cf_gcd_zero_initial_fraction_trace. ((((exists ff_h_cf_zero_initial_fraction_trace_initial_state. ff_h_cf_zero_initial_fraction_trace_initial_state + S (((cf_gcd_zero_initial_fraction_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_zero_initial_fraction_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * cf_scale_zero_initial_fraction)) /\ exists ff_q_cf_zero_initial_fraction_trace_initial_state. cf_code_zero_initial_fraction = ff_q_cf_zero_initial_fraction_trace_initial_state * S ((S (0)) * cf_scale_zero_initial_fraction) + (((cf_gcd_zero_initial_fraction_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_zero_initial_fraction_trace) + (((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_zero_initial_fraction_trace_terminal_state. ff_h_cf_zero_initial_fraction_trace_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 (S cf_length_pred_zero_initial_fraction)) * cf_scale_zero_initial_fraction)) /\ exists ff_q_cf_zero_initial_fraction_trace_terminal_state. cf_code_zero_initial_fraction = ff_q_cf_zero_initial_fraction_trace_terminal_state * S ((S (S cf_length_pred_zero_initial_fraction)) * cf_scale_zero_initial_fraction) + (((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_zero_initial_fraction_trace. (exists ff_lt_cf_zero_initial_fraction_trace_index. ff_lt_cf_zero_initial_fraction_trace_index + S cf_index_zero_initial_fraction_trace = S cf_length_pred_zero_initial_fraction) -> exists cf_old_a_zero_initial_fraction_trace cf_old_b_zero_initial_fraction_trace cf_tail_zero_initial_fraction_trace cf_new_a_zero_initial_fraction_trace cf_new_b_zero_initial_fraction_trace cf_head_zero_initial_fraction_trace cf_quotient_zero_initial_fraction_trace. ((((exists ff_h_cf_zero_initial_fraction_trace_previous_state. ff_h_cf_zero_initial_fraction_trace_previous_state + S (((cf_old_a_zero_initial_fraction_trace) + (((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)))) * S ((cf_old_a_zero_initial_fraction_trace) + (((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)))) + ((((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace))) + (((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace))))) = S ((S (cf_index_zero_initial_fraction_trace)) * cf_scale_zero_initial_fraction)) /\ exists ff_q_cf_zero_initial_fraction_trace_previous_state. cf_code_zero_initial_fraction = ff_q_cf_zero_initial_fraction_trace_previous_state * S ((S (cf_index_zero_initial_fraction_trace)) * cf_scale_zero_initial_fraction) + (((cf_old_a_zero_initial_fraction_trace) + (((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)))) * S ((cf_old_a_zero_initial_fraction_trace) + (((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)))) + ((((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace))) + (((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) * S ((cf_old_b_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace)) + ((cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace))))))) /\ ((((exists ff_h_cf_zero_initial_fraction_trace_following_state. ff_h_cf_zero_initial_fraction_trace_following_state + S (((cf_new_a_zero_initial_fraction_trace) + (((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)))) * S ((cf_new_a_zero_initial_fraction_trace) + (((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)))) + ((((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace))) + (((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace))))) = S ((S (S cf_index_zero_initial_fraction_trace)) * cf_scale_zero_initial_fraction)) /\ exists ff_q_cf_zero_initial_fraction_trace_following_state. cf_code_zero_initial_fraction = ff_q_cf_zero_initial_fraction_trace_following_state * S ((S (S cf_index_zero_initial_fraction_trace)) * cf_scale_zero_initial_fraction) + (((cf_new_a_zero_initial_fraction_trace) + (((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)))) * S ((cf_new_a_zero_initial_fraction_trace) + (((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)))) + ((((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace))) + (((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) * S ((cf_new_b_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace)) + ((cf_head_zero_initial_fraction_trace) + (cf_head_zero_initial_fraction_trace))))))) /\ (cf_new_b_zero_initial_fraction_trace = cf_old_a_zero_initial_fraction_trace /\ (cf_new_a_zero_initial_fraction_trace = cf_new_b_zero_initial_fraction_trace * cf_quotient_zero_initial_fraction_trace + cf_old_b_zero_initial_fraction_trace /\ ((exists ff_lt_cf_zero_initial_fraction_trace_remainder. ff_lt_cf_zero_initial_fraction_trace_remainder + S cf_old_b_zero_initial_fraction_trace = cf_new_b_zero_initial_fraction_trace) /\ (cf_head_zero_initial_fraction_trace = S ((cf_quotient_zero_initial_fraction_trace + cf_tail_zero_initial_fraction_trace) * S (cf_quotient_zero_initial_fraction_trace + cf_tail_zero_initial_fraction_trace) + (cf_tail_zero_initial_fraction_trace + cf_tail_zero_initial_fraction_trace)))))))))))))) -> (exists cfba_gap_zero_initial_input. cfba_gap_zero_initial_input + S (a) = (b)) -> (exists cfc_previous_numerator_zero_initial_actual cfc_previous_denominator_zero_initial_actual cfc_code_zero_initial_actual cfc_scale_zero_initial_actual. ((~(1 = 0)) /\ (exists cfc_tail_zero_initial_actualcomputation. ((exists cfc_state_zero_initial_actualcomputationinitial. ((exists cfc_left_zero_initial_actualcomputationinitialcode cfc_right_zero_initial_actualcomputationinitialcode cfc_matrix_zero_initial_actualcomputationinitialcode. ((cfc_left_zero_initial_actualcomputationinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_zero_initial_actualcomputationinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_zero_initial_actualcomputationinitialcode = ((cfc_left_zero_initial_actualcomputationinitialcode) + (cfc_right_zero_initial_actualcomputationinitialcode)) * S ((cfc_left_zero_initial_actualcomputationinitialcode) + (cfc_right_zero_initial_actualcomputationinitialcode)) + ((cfc_right_zero_initial_actualcomputationinitialcode) + (cfc_right_zero_initial_actualcomputationinitialcode))) /\ ((cfc_state_zero_initial_actualcomputationinitial) = ((cfc_tail_zero_initial_actualcomputation) + (cfc_matrix_zero_initial_actualcomputationinitialcode)) * S ((cfc_tail_zero_initial_actualcomputation) + (cfc_matrix_zero_initial_actualcomputationinitialcode)) + ((cfc_matrix_zero_initial_actualcomputationinitialcode) + (cfc_matrix_zero_initial_actualcomputationinitialcode))))))) /\ (((exists ff_h_zero_initial_actualcomputationinitialentry. ff_h_zero_initial_actualcomputationinitialentry + S (cfc_state_zero_initial_actualcomputationinitial) = S ((S (0)) * cfc_scale_zero_initial_actual)) /\ exists ff_q_zero_initial_actualcomputationinitialentry. cfc_code_zero_initial_actual = ff_q_zero_initial_actualcomputationinitialentry * S ((S (0)) * cfc_scale_zero_initial_actual) + (cfc_state_zero_initial_actualcomputationinitial))))) /\ ((exists cfc_state_zero_initial_actualcomputationterminal. ((exists cfc_left_zero_initial_actualcomputationterminalcode cfc_right_zero_initial_actualcomputationterminalcode cfc_matrix_zero_initial_actualcomputationterminalcode. ((cfc_left_zero_initial_actualcomputationterminalcode = ((0) + (cfc_previous_numerator_zero_initial_actual)) * S ((0) + (cfc_previous_numerator_zero_initial_actual)) + ((cfc_previous_numerator_zero_initial_actual) + (cfc_previous_numerator_zero_initial_actual))) /\ ((cfc_right_zero_initial_actualcomputationterminalcode = ((1) + (cfc_previous_denominator_zero_initial_actual)) * S ((1) + (cfc_previous_denominator_zero_initial_actual)) + ((cfc_previous_denominator_zero_initial_actual) + (cfc_previous_denominator_zero_initial_actual))) /\ ((cfc_matrix_zero_initial_actualcomputationterminalcode = ((cfc_left_zero_initial_actualcomputationterminalcode) + (cfc_right_zero_initial_actualcomputationterminalcode)) * S ((cfc_left_zero_initial_actualcomputationterminalcode) + (cfc_right_zero_initial_actualcomputationterminalcode)) + ((cfc_right_zero_initial_actualcomputationterminalcode) + (cfc_right_zero_initial_actualcomputationterminalcode))) /\ ((cfc_state_zero_initial_actualcomputationterminal) = ((s) + (cfc_matrix_zero_initial_actualcomputationterminalcode)) * S ((s) + (cfc_matrix_zero_initial_actualcomputationterminalcode)) + ((cfc_matrix_zero_initial_actualcomputationterminalcode) + (cfc_matrix_zero_initial_actualcomputationterminalcode))))))) /\ (((exists ff_h_zero_initial_actualcomputationterminalentry. ff_h_zero_initial_actualcomputationterminalentry + S (cfc_state_zero_initial_actualcomputationterminal) = S ((S (S (0))) * cfc_scale_zero_initial_actual)) /\ exists ff_q_zero_initial_actualcomputationterminalentry. cfc_code_zero_initial_actual = ff_q_zero_initial_actualcomputationterminalentry * S ((S (S (0))) * cfc_scale_zero_initial_actual) + (cfc_state_zero_initial_actualcomputationterminal))))) /\ (forall cfc_index_zero_initial_actualcomputation. (exists cfba_gap_zero_initial_actualcomputationbound. cfba_gap_zero_initial_actualcomputationbound + S (cfc_index_zero_initial_actualcomputation) = (S (0))) -> exists cfc_old_zero_initial_actualcomputation cfc_a_zero_initial_actualcomputation cfc_b_zero_initial_actualcomputation cfc_c_zero_initial_actualcomputation cfc_d_zero_initial_actualcomputation cfc_new_zero_initial_actualcomputation cfc_quotient_zero_initial_actualcomputation. ((exists cfc_state_zero_initial_actualcomputationprevious. ((exists cfc_left_zero_initial_actualcomputationpreviouscode cfc_right_zero_initial_actualcomputationpreviouscode cfc_matrix_zero_initial_actualcomputationpreviouscode. ((cfc_left_zero_initial_actualcomputationpreviouscode = ((cfc_a_zero_initial_actualcomputation) + (cfc_b_zero_initial_actualcomputation)) * S ((cfc_a_zero_initial_actualcomputation) + (cfc_b_zero_initial_actualcomputation)) + ((cfc_b_zero_initial_actualcomputation) + (cfc_b_zero_initial_actualcomputation))) /\ ((cfc_right_zero_initial_actualcomputationpreviouscode = ((cfc_c_zero_initial_actualcomputation) + (cfc_d_zero_initial_actualcomputation)) * S ((cfc_c_zero_initial_actualcomputation) + (cfc_d_zero_initial_actualcomputation)) + ((cfc_d_zero_initial_actualcomputation) + (cfc_d_zero_initial_actualcomputation))) /\ ((cfc_matrix_zero_initial_actualcomputationpreviouscode = ((cfc_left_zero_initial_actualcomputationpreviouscode) + (cfc_right_zero_initial_actualcomputationpreviouscode)) * S ((cfc_left_zero_initial_actualcomputationpreviouscode) + (cfc_right_zero_initial_actualcomputationpreviouscode)) + ((cfc_right_zero_initial_actualcomputationpreviouscode) + (cfc_right_zero_initial_actualcomputationpreviouscode))) /\ ((cfc_state_zero_initial_actualcomputationprevious) = ((cfc_old_zero_initial_actualcomputation) + (cfc_matrix_zero_initial_actualcomputationpreviouscode)) * S ((cfc_old_zero_initial_actualcomputation) + (cfc_matrix_zero_initial_actualcomputationpreviouscode)) + ((cfc_matrix_zero_initial_actualcomputationpreviouscode) + (cfc_matrix_zero_initial_actualcomputationpreviouscode))))))) /\ (((exists ff_h_zero_initial_actualcomputationpreviousentry. ff_h_zero_initial_actualcomputationpreviousentry + S (cfc_state_zero_initial_actualcomputationprevious) = S ((S (cfc_index_zero_initial_actualcomputation)) * cfc_scale_zero_initial_actual)) /\ exists ff_q_zero_initial_actualcomputationpreviousentry. cfc_code_zero_initial_actual = ff_q_zero_initial_actualcomputationpreviousentry * S ((S (cfc_index_zero_initial_actualcomputation)) * cfc_scale_zero_initial_actual) + (cfc_state_zero_initial_actualcomputationprevious))))) /\ ((exists cfc_state_zero_initial_actualcomputationfollowing. ((exists cfc_left_zero_initial_actualcomputationfollowingcode cfc_right_zero_initial_actualcomputationfollowingcode cfc_matrix_zero_initial_actualcomputationfollowingcode. ((cfc_left_zero_initial_actualcomputationfollowingcode = (((cfc_quotient_zero_initial_actualcomputation * cfc_a_zero_initial_actualcomputation + cfc_c_zero_initial_actualcomputation)) + ((cfc_quotient_zero_initial_actualcomputation * cfc_b_zero_initial_actualcomputation + cfc_d_zero_initial_actualcomputation))) * S (((cfc_quotient_zero_initial_actualcomputation * cfc_a_zero_initial_actualcomputation + cfc_c_zero_initial_actualcomputation)) + ((cfc_quotient_zero_initial_actualcomputation * cfc_b_zero_initial_actualcomputation + cfc_d_zero_initial_actualcomputation))) + (((cfc_quotient_zero_initial_actualcomputation * cfc_b_zero_initial_actualcomputation + cfc_d_zero_initial_actualcomputation)) + ((cfc_quotient_zero_initial_actualcomputation * cfc_b_zero_initial_actualcomputation + cfc_d_zero_initial_actualcomputation)))) /\ ((cfc_right_zero_initial_actualcomputationfollowingcode = ((cfc_a_zero_initial_actualcomputation) + (cfc_b_zero_initial_actualcomputation)) * S ((cfc_a_zero_initial_actualcomputation) + (cfc_b_zero_initial_actualcomputation)) + ((cfc_b_zero_initial_actualcomputation) + (cfc_b_zero_initial_actualcomputation))) /\ ((cfc_matrix_zero_initial_actualcomputationfollowingcode = ((cfc_left_zero_initial_actualcomputationfollowingcode) + (cfc_right_zero_initial_actualcomputationfollowingcode)) * S ((cfc_left_zero_initial_actualcomputationfollowingcode) + (cfc_right_zero_initial_actualcomputationfollowingcode)) + ((cfc_right_zero_initial_actualcomputationfollowingcode) + (cfc_right_zero_initial_actualcomputationfollowingcode))) /\ ((cfc_state_zero_initial_actualcomputationfollowing) = ((cfc_new_zero_initial_actualcomputation) + (cfc_matrix_zero_initial_actualcomputationfollowingcode)) * S ((cfc_new_zero_initial_actualcomputation) + (cfc_matrix_zero_initial_actualcomputationfollowingcode)) + ((cfc_matrix_zero_initial_actualcomputationfollowingcode) + (cfc_matrix_zero_initial_actualcomputationfollowingcode))))))) /\ (((exists ff_h_zero_initial_actualcomputationfollowingentry. ff_h_zero_initial_actualcomputationfollowingentry + S (cfc_state_zero_initial_actualcomputationfollowing) = S ((S (S cfc_index_zero_initial_actualcomputation)) * cfc_scale_zero_initial_actual)) /\ exists ff_q_zero_initial_actualcomputationfollowingentry. cfc_code_zero_initial_actual = ff_q_zero_initial_actualcomputationfollowingentry * S ((S (S cfc_index_zero_initial_actualcomputation)) * cfc_scale_zero_initial_actual) + (cfc_state_zero_initial_actualcomputationfollowing))))) /\ (cfc_new_zero_initial_actualcomputation = S ((cfc_quotient_zero_initial_actualcomputation + cfc_old_zero_initial_actualcomputation) * S (cfc_quotient_zero_initial_actualcomputation + cfc_old_zero_initial_actualcomputation) + (cfc_old_zero_initial_actualcomputation + cfc_old_zero_initial_actualcomputation)))))))))))

Complete tactic proof in conservative notation

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

52 script commands · 10 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 old history successor eliminationcf convergent numerator transportcontinued fraction first cell is initial convergent
01Fix variables and assumptionsL1–5

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro s
  4. L4
    intro hcf
  5. L5
    intro hlt
02Separate the logical casesL6–12

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

  1. L6
    cases hcf
  2. L7
    cases hcf_witness
  3. L8
    cases hcf_witness_witness
  4. L9
    cases hcf_witness_witness_witness
  5. L10
    cases hcf_witness_witness_witness_witness
  6. L11
    cases hcf_witness_witness_witness_witness_witness
  7. L12
    cases hcf_witness_witness_witness_witness_witness_right
03Establish hpL13–21

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

  1. L13
    have hp : ∃ q. ∃ r. ∃ t. a = b · q + r ∧ (Lt(r,b) ∧ (ListCell(s,q,t) ∧ ContinuedFractionTrace(b,r,t,x2,x3,x4)))Definitions: Lt(r,b)ListCell(s,q,t)ContinuedFractionTrace(b,r,t,x2,x3,x4)Original native command in the exact edition
  2. L14
    specialize cf_convergent_old_history_successor_elimination (a)
  3. L15
    specialize cf_convergent_old_history_successor_elimination (b)
  4. L16
    specialize cf_convergent_old_history_successor_elimination (s)
  5. L17
    specialize cf_convergent_old_history_successor_elimination (x2)
  6. L18
    specialize cf_convergent_old_history_successor_elimination (x3)
  7. L19
    specialize cf_convergent_old_history_successor_elimination (x4)
  8. L20
    apply cf_convergent_old_history_successor_elimination
  9. L21
    exact hcf_witness_witness_witness_witness_witness_right_right
04Separate the logical casesL22–27

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_right
  6. L27
    cases hp_witness_witness_witness_right_right
05Establish hqL28–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder unique.

  1. L28
    have hq : x5 = 0 /\ x6 = a
  2. L29
    specialize division_remainder_unique (b)
  3. L30
    specialize division_remainder_unique (a)
  4. L31
    specialize division_remainder_unique (x5)
  5. L32
    specialize division_remainder_unique (x6)
  6. L33
    specialize division_remainder_unique (0)
  7. L34
    specialize division_remainder_unique (a)
  8. L35
    apply division_remainder_unique
  9. L36
    exact hp_witness_witness_witness_left
  10. L37
    exact hp_witness_witness_witness_right_left
06Calculate and transport equalitiesL38–38

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

  1. L38
    simp [zero_add]
07Use earlier factsL39–39

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

  1. L39
    exact hlt
08Separate the logical casesL40–40

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

  1. L40
    cases hq
09Use earlier factsL41–50

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

  1. L41
    specialize cf_convergent_numerator_transport (s)
  2. L42
    specialize cf_convergent_numerator_transport (0)
  3. L43
    specialize cf_convergent_numerator_transport (x5)
  4. L44
    specialize cf_convergent_numerator_transport (0)
  5. L45
    specialize cf_convergent_numerator_transport (1)
  6. L46
    apply cf_convergent_numerator_transport
  7. L47
    exact hq_left
  8. L48
    specialize continued_fraction_first_cell_is_initial_convergent (s)
  9. L49
    specialize continued_fraction_first_cell_is_initial_convergent (x5)
  10. L50
    specialize continued_fraction_first_cell_is_initial_convergent (x7)
10Use earlier factsL51–52

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

  1. L51
    apply continued_fraction_first_cell_is_initial_convergent
  2. L52
    exact hp_witness_witness_witness_right_right_left

Library-wide reading audit

Original defined command ledger · 52 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro s
  4. 0004intro hcf
  5. 0005intro hlt
  6. 0006cases hcf
  7. 0007cases hcf_witness
  8. 0008cases hcf_witness_witness
  9. 0009cases hcf_witness_witness_witness
  10. 0010cases hcf_witness_witness_witness_witness
  11. 0011cases hcf_witness_witness_witness_witness_witness
  12. 0012cases hcf_witness_witness_witness_witness_witness_right
  13. 0013have hp : ∃ q. ∃ r. ∃ t. a = b · q + r ∧ (Lt(r,b) ∧ (ListCell(s,q,t) ∧ ContinuedFractionTrace(b,r,t,x2,x3,x4)))
  14. 0014specialize cf_convergent_old_history_successor_elimination (a)
  15. 0015specialize cf_convergent_old_history_successor_elimination (b)
  16. 0016specialize cf_convergent_old_history_successor_elimination (s)
  17. 0017specialize cf_convergent_old_history_successor_elimination (x2)
  18. 0018specialize cf_convergent_old_history_successor_elimination (x3)
  19. 0019specialize cf_convergent_old_history_successor_elimination (x4)
  20. 0020apply cf_convergent_old_history_successor_elimination
  21. 0021exact hcf_witness_witness_witness_witness_witness_right_right
  22. 0022cases hp
  23. 0023cases hp_witness
  24. 0024cases hp_witness_witness
  25. 0025cases hp_witness_witness_witness
  26. 0026cases hp_witness_witness_witness_right
  27. 0027cases hp_witness_witness_witness_right_right
  28. 0028have hq : x5 = 0 /\ x6 = a
  29. 0029specialize division_remainder_unique (b)
  30. 0030specialize division_remainder_unique (a)
  31. 0031specialize division_remainder_unique (x5)
  32. 0032specialize division_remainder_unique (x6)
  33. 0033specialize division_remainder_unique (0)
  34. 0034specialize division_remainder_unique (a)
  35. 0035apply division_remainder_unique
  36. 0036exact hp_witness_witness_witness_left
  37. 0037exact hp_witness_witness_witness_right_left
  38. 0038simp [zero_add]
  39. 0039exact hlt
  40. 0040cases hq
  41. 0041specialize cf_convergent_numerator_transport (s)
  42. 0042specialize cf_convergent_numerator_transport (0)
  43. 0043specialize cf_convergent_numerator_transport (x5)
  44. 0044specialize cf_convergent_numerator_transport (0)
  45. 0045specialize cf_convergent_numerator_transport (1)
  46. 0046apply cf_convergent_numerator_transport
  47. 0047exact hq_left
  48. 0048specialize continued_fraction_first_cell_is_initial_convergent (s)
  49. 0049specialize continued_fraction_first_cell_is_initial_convergent (x5)
  50. 0050specialize continued_fraction_first_cell_is_initial_convergent (x7)
  51. 0051apply continued_fraction_first_cell_is_initial_convergent
  52. 0052exact hp_witness_witness_witness_right_right_left