EC0009 — euclidean_trace_exists_linear

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.

G101 was OPEN when this family was first admitted in Alpha v21. It is now CLOSED in Alpha v23: the actual anchored Euclidean history, terminal gcd, and exact bound steps≤2*BitLen(b)+1 are proved.

Exact theorem in conservative defined notation

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

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 prerequisiteeuclidean_trace_exists_up_to_linear

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

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)

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.

L1
intro a
L2
intro b

02Use earlier factsL3–4

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

L3
specialize euclidean_trace_exists_up_to_linear b
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.

L5
have hbb : exists gap. gap + b = b
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.

L7
have hall : ∀ z. ∃ x. ∃ y. ∃ n. ∃ m. ContinuedFractionTrace(z,b,x,y,n,m) ∧ m ≤ bDefinitions: ContinuedFractionTraceOriginal native command in the exact edition
L8
apply euclidean_trace_exists_up_to_linear
L9
exact hbb
L10
specialize hall a
L11
exact hall

Library-wide reading audit

Original defined command ledger · 11 lines

0001intro a
0002intro b
0003specialize euclidean_trace_exists_up_to_linear b
0004specialize euclidean_trace_exists_up_to_linear b
0005have hbb : exists gap. gap + b = b
0006apply le_refl
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)))
0008apply euclidean_trace_exists_up_to_linear
0009exact hbb
0010specialize hall a
0011exact hall