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 at this family's Alpha-v22 first admission: its complete anchored trace and actual terminal gcd were proved but its logarithmic bound was not. G101 is now CLOSED in Alpha v23, including the exact first-order bound steps≤2*BitLen(b)+1.
Exact theorem in conservative defined notation
∀ a. ∀ b. ∀ g. ∀ l. EuclideanAnchoredExecution(a,b,g,l) → ∃ x. ∃ y. ∃ z. ContinuedFractionTrace(a,b,x,y,z,l) ∧ EuclideanStateAt(y,z,0,g,0,0)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
none
Original expanded first-order statement
forall a b g l. (exists egt_list_egt_anchored egt_history_egt_anchored egt_scale_egt_anchored. ((exists cf_gcd_egt_egt_anchored_trace. ((((exists ff_h_cf_egt_egt_anchored_trace_initial_state. ff_h_cf_egt_egt_anchored_trace_initial_state + S (((cf_gcd_egt_egt_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_egt_anchored_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)) * egt_scale_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_trace_initial_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_trace_initial_state * S ((S (0)) * egt_scale_egt_anchored) + (((cf_gcd_egt_egt_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_egt_anchored_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_egt_egt_anchored_trace_terminal_state. ff_h_cf_egt_egt_anchored_trace_terminal_state + S (((a) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored)))) * S ((a) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored)))) + ((((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored))) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored))))) = S ((S (l)) * egt_scale_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_trace_terminal_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_trace_terminal_state * S ((S (l)) * egt_scale_egt_anchored) + (((a) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored)))) * S ((a) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored)))) + ((((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored))) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored))))))) /\ forall cf_index_egt_egt_anchored_trace. (exists ff_lt_cf_egt_egt_anchored_trace_index. ff_lt_cf_egt_egt_anchored_trace_index + S cf_index_egt_egt_anchored_trace = l) -> exists cf_old_a_egt_egt_anchored_trace cf_old_b_egt_egt_anchored_trace cf_tail_egt_egt_anchored_trace cf_new_a_egt_egt_anchored_trace cf_new_b_egt_egt_anchored_trace cf_head_egt_egt_anchored_trace cf_quotient_egt_egt_anchored_trace. ((((exists ff_h_cf_egt_egt_anchored_trace_previous_state. ff_h_cf_egt_egt_anchored_trace_previous_state + S (((cf_old_a_egt_egt_anchored_trace) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)))) * S ((cf_old_a_egt_egt_anchored_trace) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)))) + ((((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace))) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace))))) = S ((S (cf_index_egt_egt_anchored_trace)) * egt_scale_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_trace_previous_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_trace_previous_state * S ((S (cf_index_egt_egt_anchored_trace)) * egt_scale_egt_anchored) + (((cf_old_a_egt_egt_anchored_trace) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)))) * S ((cf_old_a_egt_egt_anchored_trace) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)))) + ((((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace))) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace))))))) /\ ((((exists ff_h_cf_egt_egt_anchored_trace_following_state. ff_h_cf_egt_egt_anchored_trace_following_state + S (((cf_new_a_egt_egt_anchored_trace) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)))) * S ((cf_new_a_egt_egt_anchored_trace) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)))) + ((((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace))) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace))))) = S ((S (S cf_index_egt_egt_anchored_trace)) * egt_scale_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_trace_following_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_trace_following_state * S ((S (S cf_index_egt_egt_anchored_trace)) * egt_scale_egt_anchored) + (((cf_new_a_egt_egt_anchored_trace) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)))) * S ((cf_new_a_egt_egt_anchored_trace) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)))) + ((((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace))) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace))))))) /\ (cf_new_b_egt_egt_anchored_trace = cf_old_a_egt_egt_anchored_trace /\ (cf_new_a_egt_egt_anchored_trace = cf_new_b_egt_egt_anchored_trace * cf_quotient_egt_egt_anchored_trace + cf_old_b_egt_egt_anchored_trace /\ ((exists ff_lt_cf_egt_egt_anchored_trace_remainder. ff_lt_cf_egt_egt_anchored_trace_remainder + S cf_old_b_egt_egt_anchored_trace = cf_new_b_egt_egt_anchored_trace) /\ (cf_head_egt_egt_anchored_trace = S ((cf_quotient_egt_egt_anchored_trace + cf_tail_egt_egt_anchored_trace) * S (cf_quotient_egt_egt_anchored_trace + cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace + cf_tail_egt_egt_anchored_trace))))))))))) /\ ((((exists ff_h_cf_egt_egt_anchored_initial_state. ff_h_cf_egt_egt_anchored_initial_state + S (((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * egt_scale_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_initial_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_initial_state * S ((S (0)) * egt_scale_egt_anchored) + (((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ec_gcd_left_egt_egt_anchored_result. a = g * ec_gcd_left_egt_egt_anchored_result) /\ (exists ec_gcd_right_egt_egt_anchored_result. b = g * ec_gcd_right_egt_egt_anchored_result)) /\ forall ec_gcd_common_egt_egt_anchored_result. (exists ec_gcd_common_left_egt_egt_anchored_result. a = ec_gcd_common_egt_egt_anchored_result * ec_gcd_common_left_egt_egt_anchored_result) -> (exists ec_gcd_common_right_egt_egt_anchored_result. b = ec_gcd_common_egt_egt_anchored_result * ec_gcd_common_right_egt_egt_anchored_result) -> exists ec_gcd_greatest_egt_egt_anchored_result. g = ec_gcd_common_egt_egt_anchored_result * ec_gcd_greatest_egt_egt_anchored_result))))) -> exists s h e. ((exists cf_gcd_egt_projected. ((((exists ff_h_cf_egt_projected_initial_state. ff_h_cf_egt_projected_initial_state + S (((cf_gcd_egt_projected) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_projected) + (((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_egt_projected_initial_state. h = ff_q_cf_egt_projected_initial_state * S ((S (0)) * e) + (((cf_gcd_egt_projected) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_projected) + (((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_egt_projected_terminal_state. ff_h_cf_egt_projected_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_egt_projected_terminal_state. h = ff_q_cf_egt_projected_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_egt_projected. (exists ff_lt_cf_egt_projected_index. ff_lt_cf_egt_projected_index + S cf_index_egt_projected = l) -> exists cf_old_a_egt_projected cf_old_b_egt_projected cf_tail_egt_projected cf_new_a_egt_projected cf_new_b_egt_projected cf_head_egt_projected cf_quotient_egt_projected. ((((exists ff_h_cf_egt_projected_previous_state. ff_h_cf_egt_projected_previous_state + S (((cf_old_a_egt_projected) + (((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected)))) * S ((cf_old_a_egt_projected) + (((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected)))) + ((((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected))) + (((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected))))) = S ((S (cf_index_egt_projected)) * e)) /\ exists ff_q_cf_egt_projected_previous_state. h = ff_q_cf_egt_projected_previous_state * S ((S (cf_index_egt_projected)) * e) + (((cf_old_a_egt_projected) + (((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected)))) * S ((cf_old_a_egt_projected) + (((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected)))) + ((((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected))) + (((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected))))))) /\ ((((exists ff_h_cf_egt_projected_following_state. ff_h_cf_egt_projected_following_state + S (((cf_new_a_egt_projected) + (((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected)))) * S ((cf_new_a_egt_projected) + (((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected)))) + ((((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected))) + (((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected))))) = S ((S (S cf_index_egt_projected)) * e)) /\ exists ff_q_cf_egt_projected_following_state. h = ff_q_cf_egt_projected_following_state * S ((S (S cf_index_egt_projected)) * e) + (((cf_new_a_egt_projected) + (((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected)))) * S ((cf_new_a_egt_projected) + (((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected)))) + ((((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected))) + (((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected))))))) /\ (cf_new_b_egt_projected = cf_old_a_egt_projected /\ (cf_new_a_egt_projected = cf_new_b_egt_projected * cf_quotient_egt_projected + cf_old_b_egt_projected /\ ((exists ff_lt_cf_egt_projected_remainder. ff_lt_cf_egt_projected_remainder + S cf_old_b_egt_projected = cf_new_b_egt_projected) /\ (cf_head_egt_projected = S ((cf_quotient_egt_projected + cf_tail_egt_projected) * S (cf_quotient_egt_projected + cf_tail_egt_projected) + (cf_tail_egt_projected + cf_tail_egt_projected))))))))))) /\ (((exists ff_h_cf_egt_projected_state. ff_h_cf_egt_projected_state + S (((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((g) + (((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_egt_projected_state. h = ff_q_cf_egt_projected_state * S ((S (0)) * e) + (((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))))Complete unchanged native tactic proof
All 16 lines are the exact independently kernel-checked original script.
Read the argument
Proof checkpoints
16 script commands · 5 reading checkpoints · 0 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.
01Fix variables and assumptionsL1–5
02Separate the logical casesL6–10
03Construct an explicit witnessL11–13
04Separate the logical casesL14–14
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L14
split
Original defined command ledger · 16 lines
- 0001
intro a - 0002
intro b - 0003
intro g - 0004
intro l - 0005
intro hanchored - 0006
cases hanchored - 0007
cases hanchored_witness - 0008
cases hanchored_witness_witness - 0009
cases hanchored_witness_witness_witness - 0010
cases hanchored_witness_witness_witness_right - 0011
exists x - 0012
exists x1 - 0013
exists x2 - 0014
split - 0015
exact hanchored_witness_witness_witness_left - 0016
exact hanchored_witness_witness_witness_right_left