CF0006

continued_fraction_trace_exists

Every pair of natural numbers, including zero-input boundaries, has a finite completely witnessed Euclidean quotient trace.

Alpha v34 checked-use · first admitted v20 · 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.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∃ x. ∃ y. ∃ z. ∃ n. ContinuedFractionTrace(a,b,x,y,z,n)

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

Definition DAG

ContinuedFractionTrace(a,b,s,u,v,ell) · 1

Actual proof prerequisites

le_refl · checked external prerequisitecontinued_fraction_trace_exists_up_to
Original expanded first-order statement 
forall a b. (exists s h e l. (exists cf_gcd_total. ((((exists ff_h_cf_total_initial_state. ff_h_cf_total_initial_state + S (((cf_gcd_total) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_total) + (((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_total_initial_state. h = ff_q_cf_total_initial_state * S ((S (0)) * e) + (((cf_gcd_total) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_total) + (((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_total_terminal_state. ff_h_cf_total_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 (l)) * e)) /\ exists ff_q_cf_total_terminal_state. h = ff_q_cf_total_terminal_state * S ((S (l)) * 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_total. (exists ff_lt_cf_total_index. ff_lt_cf_total_index + S cf_index_total = l) -> exists cf_old_a_total cf_old_b_total cf_tail_total cf_new_a_total cf_new_b_total cf_head_total cf_quotient_total. ((((exists ff_h_cf_total_previous_state. ff_h_cf_total_previous_state + S (((cf_old_a_total) + (((cf_old_b_total) + (cf_tail_total)) * S ((cf_old_b_total) + (cf_tail_total)) + ((cf_tail_total) + (cf_tail_total)))) * S ((cf_old_a_total) + (((cf_old_b_total) + (cf_tail_total)) * S ((cf_old_b_total) + (cf_tail_total)) + ((cf_tail_total) + (cf_tail_total)))) + ((((cf_old_b_total) + (cf_tail_total)) * S ((cf_old_b_total) + (cf_tail_total)) + ((cf_tail_total) + (cf_tail_total))) + (((cf_old_b_total) + (cf_tail_total)) * S ((cf_old_b_total) + (cf_tail_total)) + ((cf_tail_total) + (cf_tail_total))))) = S ((S (cf_index_total)) * e)) /\ exists ff_q_cf_total_previous_state. h = ff_q_cf_total_previous_state * S ((S (cf_index_total)) * e) + (((cf_old_a_total) + (((cf_old_b_total) + (cf_tail_total)) * S ((cf_old_b_total) + (cf_tail_total)) + ((cf_tail_total) + (cf_tail_total)))) * S ((cf_old_a_total) + (((cf_old_b_total) + (cf_tail_total)) * S ((cf_old_b_total) + (cf_tail_total)) + ((cf_tail_total) + (cf_tail_total)))) + ((((cf_old_b_total) + (cf_tail_total)) * S ((cf_old_b_total) + (cf_tail_total)) + ((cf_tail_total) + (cf_tail_total))) + (((cf_old_b_total) + (cf_tail_total)) * S ((cf_old_b_total) + (cf_tail_total)) + ((cf_tail_total) + (cf_tail_total))))))) /\ ((((exists ff_h_cf_total_following_state. ff_h_cf_total_following_state + S (((cf_new_a_total) + (((cf_new_b_total) + (cf_head_total)) * S ((cf_new_b_total) + (cf_head_total)) + ((cf_head_total) + (cf_head_total)))) * S ((cf_new_a_total) + (((cf_new_b_total) + (cf_head_total)) * S ((cf_new_b_total) + (cf_head_total)) + ((cf_head_total) + (cf_head_total)))) + ((((cf_new_b_total) + (cf_head_total)) * S ((cf_new_b_total) + (cf_head_total)) + ((cf_head_total) + (cf_head_total))) + (((cf_new_b_total) + (cf_head_total)) * S ((cf_new_b_total) + (cf_head_total)) + ((cf_head_total) + (cf_head_total))))) = S ((S (S cf_index_total)) * e)) /\ exists ff_q_cf_total_following_state. h = ff_q_cf_total_following_state * S ((S (S cf_index_total)) * e) + (((cf_new_a_total) + (((cf_new_b_total) + (cf_head_total)) * S ((cf_new_b_total) + (cf_head_total)) + ((cf_head_total) + (cf_head_total)))) * S ((cf_new_a_total) + (((cf_new_b_total) + (cf_head_total)) * S ((cf_new_b_total) + (cf_head_total)) + ((cf_head_total) + (cf_head_total)))) + ((((cf_new_b_total) + (cf_head_total)) * S ((cf_new_b_total) + (cf_head_total)) + ((cf_head_total) + (cf_head_total))) + (((cf_new_b_total) + (cf_head_total)) * S ((cf_new_b_total) + (cf_head_total)) + ((cf_head_total) + (cf_head_total))))))) /\ (cf_new_b_total = cf_old_a_total /\ (cf_new_a_total = cf_new_b_total * cf_quotient_total + cf_old_b_total /\ ((exists ff_lt_cf_total_remainder. ff_lt_cf_total_remainder + S cf_old_b_total = cf_new_b_total) /\ (cf_head_total = S ((cf_quotient_total + cf_tail_total) * S (cf_quotient_total + cf_tail_total) + (cf_tail_total + cf_tail_total))))))))))))

Complete unchanged native tactic proof

All 11 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

11 script commands · 4 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)
continued fraction trace exists up to

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–2

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

  1. L1
    intro a
  2. L2
    intro b
02Use earlier factsL3–4

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

  1. L3
    specialize continued_fraction_trace_exists_up_to b
  2. L4
    specialize continued_fraction_trace_exists_up_to b
03Establish hbbL5–6

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

  1. L5
    have hbb : exists gap. gap + b = b
  2. L6
    apply le_refl
04Establish hallL7–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply continued fraction trace exists up to.

  1. L7
    have hall : ∀ z. ∃ x. ∃ y. ∃ n. ∃ m. ContinuedFractionTrace(z,b,x,y,n,m)Definitions: ContinuedFractionTraceOriginal native command in the exact edition
  2. L8
    apply continued_fraction_trace_exists_up_to
  3. L9
    exact hbb
  4. L10
    specialize hall a
  5. L11
    exact hall

Library-wide reading audit

Original defined command ledger · 11 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003specialize continued_fraction_trace_exists_up_to b
  4. 0004specialize continued_fraction_trace_exists_up_to b
  5. 0005have hbb : exists gap. gap + b = b
  6. 0006apply le_refl
  7. 0007have hall : forall z. (exists s h e l. (exists cf_gcd_total_all. ((((exists ff_h_cf_total_all_initial_state. ff_h_cf_total_all_initial_state + S (((cf_gcd_total_all) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_total_all) + (((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_total_all_initial_state. h = ff_q_cf_total_all_initial_state * S ((S (0)) * e) + (((cf_gcd_total_all) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_total_all) + (((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_total_all_terminal_state. ff_h_cf_total_all_terminal_state + S (((z) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((z) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))) = S ((S (l)) * e)) /\ exists ff_q_cf_total_all_terminal_state. h = ff_q_cf_total_all_terminal_state * S ((S (l)) * e) + (((z) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((z) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))))) /\ forall cf_index_total_all. (exists ff_lt_cf_total_all_index. ff_lt_cf_total_all_index + S cf_index_total_all = l) -> exists cf_old_a_total_all cf_old_b_total_all cf_tail_total_all cf_new_a_total_all cf_new_b_total_all cf_head_total_all cf_quotient_total_all. ((((exists ff_h_cf_total_all_previous_state. ff_h_cf_total_all_previous_state + S (((cf_old_a_total_all) + (((cf_old_b_total_all) + (cf_tail_total_all)) * S ((cf_old_b_total_all) + (cf_tail_total_all)) + ((cf_tail_total_all) + (cf_tail_total_all)))) * S ((cf_old_a_total_all) + (((cf_old_b_total_all) + (cf_tail_total_all)) * S ((cf_old_b_total_all) + (cf_tail_total_all)) + ((cf_tail_total_all) + (cf_tail_total_all)))) + ((((cf_old_b_total_all) + (cf_tail_total_all)) * S ((cf_old_b_total_all) + (cf_tail_total_all)) + ((cf_tail_total_all) + (cf_tail_total_all))) + (((cf_old_b_total_all) + (cf_tail_total_all)) * S ((cf_old_b_total_all) + (cf_tail_total_all)) + ((cf_tail_total_all) + (cf_tail_total_all))))) = S ((S (cf_index_total_all)) * e)) /\ exists ff_q_cf_total_all_previous_state. h = ff_q_cf_total_all_previous_state * S ((S (cf_index_total_all)) * e) + (((cf_old_a_total_all) + (((cf_old_b_total_all) + (cf_tail_total_all)) * S ((cf_old_b_total_all) + (cf_tail_total_all)) + ((cf_tail_total_all) + (cf_tail_total_all)))) * S ((cf_old_a_total_all) + (((cf_old_b_total_all) + (cf_tail_total_all)) * S ((cf_old_b_total_all) + (cf_tail_total_all)) + ((cf_tail_total_all) + (cf_tail_total_all)))) + ((((cf_old_b_total_all) + (cf_tail_total_all)) * S ((cf_old_b_total_all) + (cf_tail_total_all)) + ((cf_tail_total_all) + (cf_tail_total_all))) + (((cf_old_b_total_all) + (cf_tail_total_all)) * S ((cf_old_b_total_all) + (cf_tail_total_all)) + ((cf_tail_total_all) + (cf_tail_total_all))))))) /\ ((((exists ff_h_cf_total_all_following_state. ff_h_cf_total_all_following_state + S (((cf_new_a_total_all) + (((cf_new_b_total_all) + (cf_head_total_all)) * S ((cf_new_b_total_all) + (cf_head_total_all)) + ((cf_head_total_all) + (cf_head_total_all)))) * S ((cf_new_a_total_all) + (((cf_new_b_total_all) + (cf_head_total_all)) * S ((cf_new_b_total_all) + (cf_head_total_all)) + ((cf_head_total_all) + (cf_head_total_all)))) + ((((cf_new_b_total_all) + (cf_head_total_all)) * S ((cf_new_b_total_all) + (cf_head_total_all)) + ((cf_head_total_all) + (cf_head_total_all))) + (((cf_new_b_total_all) + (cf_head_total_all)) * S ((cf_new_b_total_all) + (cf_head_total_all)) + ((cf_head_total_all) + (cf_head_total_all))))) = S ((S (S cf_index_total_all)) * e)) /\ exists ff_q_cf_total_all_following_state. h = ff_q_cf_total_all_following_state * S ((S (S cf_index_total_all)) * e) + (((cf_new_a_total_all) + (((cf_new_b_total_all) + (cf_head_total_all)) * S ((cf_new_b_total_all) + (cf_head_total_all)) + ((cf_head_total_all) + (cf_head_total_all)))) * S ((cf_new_a_total_all) + (((cf_new_b_total_all) + (cf_head_total_all)) * S ((cf_new_b_total_all) + (cf_head_total_all)) + ((cf_head_total_all) + (cf_head_total_all)))) + ((((cf_new_b_total_all) + (cf_head_total_all)) * S ((cf_new_b_total_all) + (cf_head_total_all)) + ((cf_head_total_all) + (cf_head_total_all))) + (((cf_new_b_total_all) + (cf_head_total_all)) * S ((cf_new_b_total_all) + (cf_head_total_all)) + ((cf_head_total_all) + (cf_head_total_all))))))) /\ (cf_new_b_total_all = cf_old_a_total_all /\ (cf_new_a_total_all = cf_new_b_total_all * cf_quotient_total_all + cf_old_b_total_all /\ ((exists ff_lt_cf_total_all_remainder. ff_lt_cf_total_all_remainder + S cf_old_b_total_all = cf_new_b_total_all) /\ (cf_head_total_all = S ((cf_quotient_total_all + cf_tail_total_all) * S (cf_quotient_total_all + cf_tail_total_all) + (cf_tail_total_all + cf_tail_total_all))))))))))))
  8. 0008apply continued_fraction_trace_exists_up_to
  9. 0009exact hbb
  10. 0010specialize hall a
  11. 0011exact hall