CF0006

continued_fraction_trace_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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 expanded first-order arithmetic 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))))))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 11 exact native proof lines.

Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

le_refl Stable theorem; checked-use authorized CF0005 continued_fraction_trace_exists_up_to

Direct dependents

CF0007 continued_fraction_nonzero_divisor_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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: ContinuedFractionTrace
  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 exact 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