EC0009

euclidean_trace_exists_linear

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

Every natural input pair admits an actual terminating Euclidean beta-trace whose exact division count is at most its initial divisor.

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_ec_total_bounded. ((((exists ff_h_cf_ec_total_bounded_initial_state. ff_h_cf_ec_total_bounded_initial_state + S (((cf_gcd_ec_total_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_total_bounded) + (((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_ec_total_bounded_initial_state. h = ff_q_cf_ec_total_bounded_initial_state * S ((S (0)) * e) + (((cf_gcd_ec_total_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_total_bounded) + (((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_ec_total_bounded_terminal_state. ff_h_cf_ec_total_bounded_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_ec_total_bounded_terminal_state. h = ff_q_cf_ec_total_bounded_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_ec_total_bounded. (exists ff_lt_cf_ec_total_bounded_index. ff_lt_cf_ec_total_bounded_index + S cf_index_ec_total_bounded = l) -> exists cf_old_a_ec_total_bounded cf_old_b_ec_total_bounded cf_tail_ec_total_bounded cf_new_a_ec_total_bounded cf_new_b_ec_total_bounded cf_head_ec_total_bounded cf_quotient_ec_total_bounded. ((((exists ff_h_cf_ec_total_bounded_previous_state. ff_h_cf_ec_total_bounded_previous_state + S (((cf_old_a_ec_total_bounded) + (((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) * S ((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) + ((cf_tail_ec_total_bounded) + (cf_tail_ec_total_bounded)))) * S ((cf_old_a_ec_total_bounded) + (((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) * S ((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) + ((cf_tail_ec_total_bounded) + (cf_tail_ec_total_bounded)))) + ((((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) * S ((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) + ((cf_tail_ec_total_bounded) + (cf_tail_ec_total_bounded))) + (((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) * S ((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) + ((cf_tail_ec_total_bounded) + (cf_tail_ec_total_bounded))))) = S ((S (cf_index_ec_total_bounded)) * e)) /\ exists ff_q_cf_ec_total_bounded_previous_state. h = ff_q_cf_ec_total_bounded_previous_state * S ((S (cf_index_ec_total_bounded)) * e) + (((cf_old_a_ec_total_bounded) + (((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) * S ((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) + ((cf_tail_ec_total_bounded) + (cf_tail_ec_total_bounded)))) * S ((cf_old_a_ec_total_bounded) + (((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) * S ((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) + ((cf_tail_ec_total_bounded) + (cf_tail_ec_total_bounded)))) + ((((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) * S ((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) + ((cf_tail_ec_total_bounded) + (cf_tail_ec_total_bounded))) + (((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) * S ((cf_old_b_ec_total_bounded) + (cf_tail_ec_total_bounded)) + ((cf_tail_ec_total_bounded) + (cf_tail_ec_total_bounded))))))) /\ ((((exists ff_h_cf_ec_total_bounded_following_state. ff_h_cf_ec_total_bounded_following_state + S (((cf_new_a_ec_total_bounded) + (((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) * S ((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) + ((cf_head_ec_total_bounded) + (cf_head_ec_total_bounded)))) * S ((cf_new_a_ec_total_bounded) + (((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) * S ((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) + ((cf_head_ec_total_bounded) + (cf_head_ec_total_bounded)))) + ((((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) * S ((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) + ((cf_head_ec_total_bounded) + (cf_head_ec_total_bounded))) + (((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) * S ((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) + ((cf_head_ec_total_bounded) + (cf_head_ec_total_bounded))))) = S ((S (S cf_index_ec_total_bounded)) * e)) /\ exists ff_q_cf_ec_total_bounded_following_state. h = ff_q_cf_ec_total_bounded_following_state * S ((S (S cf_index_ec_total_bounded)) * e) + (((cf_new_a_ec_total_bounded) + (((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) * S ((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) + ((cf_head_ec_total_bounded) + (cf_head_ec_total_bounded)))) * S ((cf_new_a_ec_total_bounded) + (((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) * S ((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) + ((cf_head_ec_total_bounded) + (cf_head_ec_total_bounded)))) + ((((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) * S ((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) + ((cf_head_ec_total_bounded) + (cf_head_ec_total_bounded))) + (((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) * S ((cf_new_b_ec_total_bounded) + (cf_head_ec_total_bounded)) + ((cf_head_ec_total_bounded) + (cf_head_ec_total_bounded))))))) /\ (cf_new_b_ec_total_bounded = cf_old_a_ec_total_bounded /\ (cf_new_a_ec_total_bounded = cf_new_b_ec_total_bounded * cf_quotient_ec_total_bounded + cf_old_b_ec_total_bounded /\ ((exists ff_lt_cf_ec_total_bounded_remainder. ff_lt_cf_ec_total_bounded_remainder + S cf_old_b_ec_total_bounded = cf_new_b_ec_total_bounded) /\ (cf_head_ec_total_bounded = S ((cf_quotient_ec_total_bounded + cf_tail_ec_total_bounded) * S (cf_quotient_ec_total_bounded + cf_tail_ec_total_bounded) + (cf_tail_ec_total_bounded + cf_tail_ec_total_bounded))))))))))) /\ (exists ec_bound_gap_total. ec_bound_gap_total + l = b)))

Constructive proof overview

Generated structural guide

Every natural input pair admits an actual terminating Euclidean beta-trace whose exact division count is at most its initial divisor.

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

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

Proof neighborhood

Direct dependencies

le_refl Stable theorem; checked-use authorized EC0008 euclidean_trace_exists_up_to_linear

Direct dependents

EC000F euclidean_gcd_execution_linear_bound

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)
euclidean trace exists up to linear

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 euclidean_trace_exists_up_to_linear b
  2. L4
    specialize euclidean_trace_exists_up_to_linear 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 euclidean trace exists up to linear.

  1. L7
    have hall : ∀ z. ∃ x. ∃ y. ∃ n. ∃ m. ContinuedFractionTrace(z,b,x,y,n,m) ∧ m ≤ bDefinitions: ContinuedFractionTrace
  2. L8
    apply euclidean_trace_exists_up_to_linear
  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 euclidean_trace_exists_up_to_linear b
  4. 0004specialize euclidean_trace_exists_up_to_linear 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_ec_total_all_bounded. ((((exists ff_h_cf_ec_total_all_bounded_initial_state. ff_h_cf_ec_total_all_bounded_initial_state + S (((cf_gcd_ec_total_all_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_total_all_bounded) + (((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_ec_total_all_bounded_initial_state. h = ff_q_cf_ec_total_all_bounded_initial_state * S ((S (0)) * e) + (((cf_gcd_ec_total_all_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_total_all_bounded) + (((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_ec_total_all_bounded_terminal_state. ff_h_cf_ec_total_all_bounded_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_ec_total_all_bounded_terminal_state. h = ff_q_cf_ec_total_all_bounded_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_ec_total_all_bounded. (exists ff_lt_cf_ec_total_all_bounded_index. ff_lt_cf_ec_total_all_bounded_index + S cf_index_ec_total_all_bounded = l) -> exists cf_old_a_ec_total_all_bounded cf_old_b_ec_total_all_bounded cf_tail_ec_total_all_bounded cf_new_a_ec_total_all_bounded cf_new_b_ec_total_all_bounded cf_head_ec_total_all_bounded cf_quotient_ec_total_all_bounded. ((((exists ff_h_cf_ec_total_all_bounded_previous_state. ff_h_cf_ec_total_all_bounded_previous_state + S (((cf_old_a_ec_total_all_bounded) + (((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) * S ((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) + ((cf_tail_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)))) * S ((cf_old_a_ec_total_all_bounded) + (((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) * S ((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) + ((cf_tail_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)))) + ((((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) * S ((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) + ((cf_tail_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded))) + (((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) * S ((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) + ((cf_tail_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded))))) = S ((S (cf_index_ec_total_all_bounded)) * e)) /\ exists ff_q_cf_ec_total_all_bounded_previous_state. h = ff_q_cf_ec_total_all_bounded_previous_state * S ((S (cf_index_ec_total_all_bounded)) * e) + (((cf_old_a_ec_total_all_bounded) + (((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) * S ((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) + ((cf_tail_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)))) * S ((cf_old_a_ec_total_all_bounded) + (((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) * S ((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) + ((cf_tail_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)))) + ((((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) * S ((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) + ((cf_tail_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded))) + (((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) * S ((cf_old_b_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded)) + ((cf_tail_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded))))))) /\ ((((exists ff_h_cf_ec_total_all_bounded_following_state. ff_h_cf_ec_total_all_bounded_following_state + S (((cf_new_a_ec_total_all_bounded) + (((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) * S ((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) + ((cf_head_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)))) * S ((cf_new_a_ec_total_all_bounded) + (((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) * S ((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) + ((cf_head_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)))) + ((((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) * S ((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) + ((cf_head_ec_total_all_bounded) + (cf_head_ec_total_all_bounded))) + (((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) * S ((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) + ((cf_head_ec_total_all_bounded) + (cf_head_ec_total_all_bounded))))) = S ((S (S cf_index_ec_total_all_bounded)) * e)) /\ exists ff_q_cf_ec_total_all_bounded_following_state. h = ff_q_cf_ec_total_all_bounded_following_state * S ((S (S cf_index_ec_total_all_bounded)) * e) + (((cf_new_a_ec_total_all_bounded) + (((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) * S ((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) + ((cf_head_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)))) * S ((cf_new_a_ec_total_all_bounded) + (((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) * S ((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) + ((cf_head_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)))) + ((((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) * S ((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) + ((cf_head_ec_total_all_bounded) + (cf_head_ec_total_all_bounded))) + (((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) * S ((cf_new_b_ec_total_all_bounded) + (cf_head_ec_total_all_bounded)) + ((cf_head_ec_total_all_bounded) + (cf_head_ec_total_all_bounded))))))) /\ (cf_new_b_ec_total_all_bounded = cf_old_a_ec_total_all_bounded /\ (cf_new_a_ec_total_all_bounded = cf_new_b_ec_total_all_bounded * cf_quotient_ec_total_all_bounded + cf_old_b_ec_total_all_bounded /\ ((exists ff_lt_cf_ec_total_all_bounded_remainder. ff_lt_cf_ec_total_all_bounded_remainder + S cf_old_b_ec_total_all_bounded = cf_new_b_ec_total_all_bounded) /\ (cf_head_ec_total_all_bounded = S ((cf_quotient_ec_total_all_bounded + cf_tail_ec_total_all_bounded) * S (cf_quotient_ec_total_all_bounded + cf_tail_ec_total_all_bounded) + (cf_tail_ec_total_all_bounded + cf_tail_ec_total_all_bounded))))))))))) /\ (exists ec_bound_gap_total_all. ec_bound_gap_total_all + l = b)))
  8. 0008apply euclidean_trace_exists_up_to_linear
  9. 0009exact hbb
  10. 0010specialize hall a
  11. 0011exact hall