EL000F

euclidean_log_execution_strong

Every bit-length witness constructs a genuine complete beta execution whose actual terminal state is its gcd and whose exact step count is at most twice that length.

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

The exact G101 milestone is fully proved, including the stronger checked bound k≤2·BitLen(b), a real beta-coded execution, and its actual terminal gcd. The independent T13 determinant/rank/integer-span substrate is now closed in the separate Alpha-v27 integer-linear-algebra branch. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ l. BitLen(b,l) → ∃ x. ∃ y. EuclideanAnchoredExecution(a,b,x,y) ∧ Le(y,l + l)

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

Definition DAG

BitLen(n,ell) · 1EuclideanAnchoredExecution(a,b,g,k) · 1Le(a,b) · 1

Actual proof prerequisites

euclidean_log_trace_boundeuclidean_trace_terminal_gcd_exists · checked external prerequisite
Original expanded first-order statement 
forall a b l. ((((b) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_elb_length ff_lower_bl_elb_length ff_upper_bl_elb_length. (((l) = S ff_exponent_bl_elb_length) /\ ((exists ff_positive_bl_elb_length. ff_positive_bl_elb_length + 1 = (b)) /\ ((exists pa_b_bl_elb_length_lower pa_c_bl_elb_length_lower. ((forall pa_i_bl_elb_length_lower_repeat. (exists pa_lt_bl_elb_length_lower_repeat_bound. pa_lt_bl_elb_length_lower_repeat_bound + S pa_i_bl_elb_length_lower_repeat = ff_exponent_bl_elb_length) -> (((exists pa_h_bl_elb_length_lower_repeat_decoded. pa_h_bl_elb_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_elb_length_lower_repeat)) * pa_c_bl_elb_length_lower)) /\ exists pa_q_bl_elb_length_lower_repeat_decoded. pa_b_bl_elb_length_lower = pa_q_bl_elb_length_lower_repeat_decoded * S ((S (pa_i_bl_elb_length_lower_repeat)) * pa_c_bl_elb_length_lower) + (2)))) /\ (exists pa_u_bl_elb_length_lower_product pa_v_bl_elb_length_lower_product. ((((exists pa_h_bl_elb_length_lower_product_start. pa_h_bl_elb_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_start. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_start * S ((S (0)) * pa_v_bl_elb_length_lower_product) + (1))) /\ ((((exists pa_h_bl_elb_length_lower_product_terminal. pa_h_bl_elb_length_lower_product_terminal + S (ff_lower_bl_elb_length) = S ((S (ff_exponent_bl_elb_length)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_terminal. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_terminal * S ((S (ff_exponent_bl_elb_length)) * pa_v_bl_elb_length_lower_product) + (ff_lower_bl_elb_length))) /\ forall pa_i_bl_elb_length_lower_product. (exists pa_lt_bl_elb_length_lower_product_bound. pa_lt_bl_elb_length_lower_product_bound + S pa_i_bl_elb_length_lower_product = ff_exponent_bl_elb_length) -> exists pa_p_bl_elb_length_lower_product pa_r_bl_elb_length_lower_product pa_s_bl_elb_length_lower_product. ((((exists pa_h_bl_elb_length_lower_product_factor. pa_h_bl_elb_length_lower_product_factor + S (pa_p_bl_elb_length_lower_product) = S ((S (pa_i_bl_elb_length_lower_product)) * pa_c_bl_elb_length_lower)) /\ exists pa_q_bl_elb_length_lower_product_factor. pa_b_bl_elb_length_lower = pa_q_bl_elb_length_lower_product_factor * S ((S (pa_i_bl_elb_length_lower_product)) * pa_c_bl_elb_length_lower) + (pa_p_bl_elb_length_lower_product))) /\ ((((exists pa_h_bl_elb_length_lower_product_partial. pa_h_bl_elb_length_lower_product_partial + S (pa_r_bl_elb_length_lower_product) = S ((S (pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_partial. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_partial * S ((S (pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product) + (pa_r_bl_elb_length_lower_product))) /\ ((((exists pa_h_bl_elb_length_lower_product_successor. pa_h_bl_elb_length_lower_product_successor + S (pa_s_bl_elb_length_lower_product) = S ((S (S pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_successor. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_successor * S ((S (S pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product) + (pa_s_bl_elb_length_lower_product))) /\ pa_s_bl_elb_length_lower_product = pa_r_bl_elb_length_lower_product * pa_p_bl_elb_length_lower_product)))))))) /\ ((exists pa_b_bl_elb_length_upper pa_c_bl_elb_length_upper. ((forall pa_i_bl_elb_length_upper_repeat. (exists pa_lt_bl_elb_length_upper_repeat_bound. pa_lt_bl_elb_length_upper_repeat_bound + S pa_i_bl_elb_length_upper_repeat = l) -> (((exists pa_h_bl_elb_length_upper_repeat_decoded. pa_h_bl_elb_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_elb_length_upper_repeat)) * pa_c_bl_elb_length_upper)) /\ exists pa_q_bl_elb_length_upper_repeat_decoded. pa_b_bl_elb_length_upper = pa_q_bl_elb_length_upper_repeat_decoded * S ((S (pa_i_bl_elb_length_upper_repeat)) * pa_c_bl_elb_length_upper) + (2)))) /\ (exists pa_u_bl_elb_length_upper_product pa_v_bl_elb_length_upper_product. ((((exists pa_h_bl_elb_length_upper_product_start. pa_h_bl_elb_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_start. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_start * S ((S (0)) * pa_v_bl_elb_length_upper_product) + (1))) /\ ((((exists pa_h_bl_elb_length_upper_product_terminal. pa_h_bl_elb_length_upper_product_terminal + S (ff_upper_bl_elb_length) = S ((S (l)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_terminal. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_terminal * S ((S (l)) * pa_v_bl_elb_length_upper_product) + (ff_upper_bl_elb_length))) /\ forall pa_i_bl_elb_length_upper_product. (exists pa_lt_bl_elb_length_upper_product_bound. pa_lt_bl_elb_length_upper_product_bound + S pa_i_bl_elb_length_upper_product = l) -> exists pa_p_bl_elb_length_upper_product pa_r_bl_elb_length_upper_product pa_s_bl_elb_length_upper_product. ((((exists pa_h_bl_elb_length_upper_product_factor. pa_h_bl_elb_length_upper_product_factor + S (pa_p_bl_elb_length_upper_product) = S ((S (pa_i_bl_elb_length_upper_product)) * pa_c_bl_elb_length_upper)) /\ exists pa_q_bl_elb_length_upper_product_factor. pa_b_bl_elb_length_upper = pa_q_bl_elb_length_upper_product_factor * S ((S (pa_i_bl_elb_length_upper_product)) * pa_c_bl_elb_length_upper) + (pa_p_bl_elb_length_upper_product))) /\ ((((exists pa_h_bl_elb_length_upper_product_partial. pa_h_bl_elb_length_upper_product_partial + S (pa_r_bl_elb_length_upper_product) = S ((S (pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_partial. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_partial * S ((S (pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product) + (pa_r_bl_elb_length_upper_product))) /\ ((((exists pa_h_bl_elb_length_upper_product_successor. pa_h_bl_elb_length_upper_product_successor + S (pa_s_bl_elb_length_upper_product) = S ((S (S pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_successor. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_successor * S ((S (S pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product) + (pa_s_bl_elb_length_upper_product))) /\ pa_s_bl_elb_length_upper_product = pa_r_bl_elb_length_upper_product * pa_p_bl_elb_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_elb_length. ff_lower_gap_bl_elb_length + (ff_lower_bl_elb_length) = (b)) /\ (exists ff_upper_gap_bl_elb_length. ff_upper_gap_bl_elb_length + S (b) = (ff_upper_bl_elb_length))))))))) -> exists g k. ((exists egt_list_elb_anchored egt_history_elb_anchored egt_scale_elb_anchored. ((exists cf_gcd_egt_elb_anchored_trace. ((((exists ff_h_cf_egt_elb_anchored_trace_initial_state. ff_h_cf_egt_elb_anchored_trace_initial_state + S (((cf_gcd_egt_elb_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_elb_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_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_trace_initial_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_trace_initial_state * S ((S (0)) * egt_scale_elb_anchored) + (((cf_gcd_egt_elb_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_elb_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_elb_anchored_trace_terminal_state. ff_h_cf_egt_elb_anchored_trace_terminal_state + S (((a) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored)))) * S ((a) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored)))) + ((((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored))) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored))))) = S ((S (k)) * egt_scale_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_trace_terminal_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_trace_terminal_state * S ((S (k)) * egt_scale_elb_anchored) + (((a) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored)))) * S ((a) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored)))) + ((((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored))) + (((b) + (egt_list_elb_anchored)) * S ((b) + (egt_list_elb_anchored)) + ((egt_list_elb_anchored) + (egt_list_elb_anchored))))))) /\ forall cf_index_egt_elb_anchored_trace. (exists ff_lt_cf_egt_elb_anchored_trace_index. ff_lt_cf_egt_elb_anchored_trace_index + S cf_index_egt_elb_anchored_trace = k) -> exists cf_old_a_egt_elb_anchored_trace cf_old_b_egt_elb_anchored_trace cf_tail_egt_elb_anchored_trace cf_new_a_egt_elb_anchored_trace cf_new_b_egt_elb_anchored_trace cf_head_egt_elb_anchored_trace cf_quotient_egt_elb_anchored_trace. ((((exists ff_h_cf_egt_elb_anchored_trace_previous_state. ff_h_cf_egt_elb_anchored_trace_previous_state + S (((cf_old_a_egt_elb_anchored_trace) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)))) * S ((cf_old_a_egt_elb_anchored_trace) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)))) + ((((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace))) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace))))) = S ((S (cf_index_egt_elb_anchored_trace)) * egt_scale_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_trace_previous_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_trace_previous_state * S ((S (cf_index_egt_elb_anchored_trace)) * egt_scale_elb_anchored) + (((cf_old_a_egt_elb_anchored_trace) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)))) * S ((cf_old_a_egt_elb_anchored_trace) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)))) + ((((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace))) + (((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) * S ((cf_old_b_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace)) + ((cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace))))))) /\ ((((exists ff_h_cf_egt_elb_anchored_trace_following_state. ff_h_cf_egt_elb_anchored_trace_following_state + S (((cf_new_a_egt_elb_anchored_trace) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)))) * S ((cf_new_a_egt_elb_anchored_trace) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)))) + ((((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace))) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace))))) = S ((S (S cf_index_egt_elb_anchored_trace)) * egt_scale_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_trace_following_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_trace_following_state * S ((S (S cf_index_egt_elb_anchored_trace)) * egt_scale_elb_anchored) + (((cf_new_a_egt_elb_anchored_trace) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)))) * S ((cf_new_a_egt_elb_anchored_trace) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)))) + ((((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace))) + (((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) * S ((cf_new_b_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace)) + ((cf_head_egt_elb_anchored_trace) + (cf_head_egt_elb_anchored_trace))))))) /\ (cf_new_b_egt_elb_anchored_trace = cf_old_a_egt_elb_anchored_trace /\ (cf_new_a_egt_elb_anchored_trace = cf_new_b_egt_elb_anchored_trace * cf_quotient_egt_elb_anchored_trace + cf_old_b_egt_elb_anchored_trace /\ ((exists ff_lt_cf_egt_elb_anchored_trace_remainder. ff_lt_cf_egt_elb_anchored_trace_remainder + S cf_old_b_egt_elb_anchored_trace = cf_new_b_egt_elb_anchored_trace) /\ (cf_head_egt_elb_anchored_trace = S ((cf_quotient_egt_elb_anchored_trace + cf_tail_egt_elb_anchored_trace) * S (cf_quotient_egt_elb_anchored_trace + cf_tail_egt_elb_anchored_trace) + (cf_tail_egt_elb_anchored_trace + cf_tail_egt_elb_anchored_trace))))))))))) /\ ((((exists ff_h_cf_egt_elb_anchored_initial_state. ff_h_cf_egt_elb_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_elb_anchored)) /\ exists ff_q_cf_egt_elb_anchored_initial_state. egt_history_elb_anchored = ff_q_cf_egt_elb_anchored_initial_state * S ((S (0)) * egt_scale_elb_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_elb_anchored_result. a = g * ec_gcd_left_egt_elb_anchored_result) /\ (exists ec_gcd_right_egt_elb_anchored_result. b = g * ec_gcd_right_egt_elb_anchored_result)) /\ forall ec_gcd_common_egt_elb_anchored_result. (exists ec_gcd_common_left_egt_elb_anchored_result. a = ec_gcd_common_egt_elb_anchored_result * ec_gcd_common_left_egt_elb_anchored_result) -> (exists ec_gcd_common_right_egt_elb_anchored_result. b = ec_gcd_common_egt_elb_anchored_result * ec_gcd_common_right_egt_elb_anchored_result) -> exists ec_gcd_greatest_egt_elb_anchored_result. g = ec_gcd_common_egt_elb_anchored_result * ec_gcd_greatest_egt_elb_anchored_result))))) /\ exists gap. gap + k = l + l)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

38 script commands · 13 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 log trace bound

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–4

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro l
  4. L4
    intro hlength
02Use earlier factsL5–7

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

  1. L5
    specialize euclidean_log_trace_bound a
  2. L6
    specialize euclidean_log_trace_bound b
  3. L7
    specialize euclidean_log_trace_bound l
03Establish hboundedL8–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean log trace bound.

  1. L8
    have hbounded : EuclideanBoundedTrace(a,b,l + l)Definitions: EuclideanBoundedTraceOriginal native command in the exact edition
  2. L9
    apply euclidean_log_trace_bound
  3. L10
    exact hlength
04Separate the logical casesL11–15

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L11
    cases hbounded
  2. L12
    cases hbounded_witness
  3. L13
    cases hbounded_witness_witness
  4. L14
    cases hbounded_witness_witness_witness
  5. L15
    cases hbounded_witness_witness_witness_witness
05Establish hterminalL16–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean trace terminal gcd exists.

  1. L16
    have hterminal : ∃ g. EuclideanStateAt(x1,x2,0,g,0,0) ∧ IsGCD(g,a,b)Definitions: EuclideanStateAtIsGCDOriginal native command in the exact edition
  2. L17
    specialize euclidean_trace_terminal_gcd_exists a
  3. L18
    specialize euclidean_trace_terminal_gcd_exists b
  4. L19
    specialize euclidean_trace_terminal_gcd_exists x
  5. L20
    specialize euclidean_trace_terminal_gcd_exists x1
  6. L21
    specialize euclidean_trace_terminal_gcd_exists x2
  7. L22
    specialize euclidean_trace_terminal_gcd_exists x3
  8. L23
    apply euclidean_trace_terminal_gcd_exists
  9. L24
    exact hbounded_witness_witness_witness_witness_left
06Separate the logical casesL25–26

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L25
    cases hterminal
  2. L26
    cases hterminal_witness
07Construct an explicit witnessL27–28

Supply the displayed value, then prove that it has the required property.

  1. L27
    exists x4
  2. L28
    exists x3
08Separate the logical casesL29–29

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L29
    split
09Construct an explicit witnessL30–32

Supply the displayed value, then prove that it has the required property.

  1. L30
    exists x
  2. L31
    exists x1
  3. L32
    exists x2
10Separate the logical casesL33–33

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L33
    split
11Use earlier factsL34–34

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

  1. L34
    exact hbounded_witness_witness_witness_witness_left
12Separate the logical casesL35–35

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L35
    split
13Use earlier factsL36–38

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

  1. L36
    exact hterminal_witness_left
  2. L37
    exact hterminal_witness_right
  3. L38
    exact hbounded_witness_witness_witness_witness_right

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro l
  4. 0004intro hlength
  5. 0005specialize euclidean_log_trace_bound a
  6. 0006specialize euclidean_log_trace_bound b
  7. 0007specialize euclidean_log_trace_bound l
  8. 0008have hbounded : exists elb_list_length_budget elb_history_length_budget elb_scale_length_budget elb_steps_length_budget. ((exists cf_gcd_elb_length_budget_budget. ((((exists ff_h_cf_elb_length_budget_budget_initial_state. ff_h_cf_elb_length_budget_budget_initial_state + S (((cf_gcd_elb_length_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_length_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_length_budget)) /\ exists ff_q_cf_elb_length_budget_budget_initial_state. elb_history_length_budget = ff_q_cf_elb_length_budget_budget_initial_state * S ((S (0)) * elb_scale_length_budget) + (((cf_gcd_elb_length_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_length_budget_budget) + (((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_elb_length_budget_budget_terminal_state. ff_h_cf_elb_length_budget_budget_terminal_state + S (((a) + (((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget)))) * S ((a) + (((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget)))) + ((((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget))) + (((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget))))) = S ((S (elb_steps_length_budget)) * elb_scale_length_budget)) /\ exists ff_q_cf_elb_length_budget_budget_terminal_state. elb_history_length_budget = ff_q_cf_elb_length_budget_budget_terminal_state * S ((S (elb_steps_length_budget)) * elb_scale_length_budget) + (((a) + (((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget)))) * S ((a) + (((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget)))) + ((((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget))) + (((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget))))))) /\ forall cf_index_elb_length_budget_budget. (exists ff_lt_cf_elb_length_budget_budget_index. ff_lt_cf_elb_length_budget_budget_index + S cf_index_elb_length_budget_budget = elb_steps_length_budget) -> exists cf_old_a_elb_length_budget_budget cf_old_b_elb_length_budget_budget cf_tail_elb_length_budget_budget cf_new_a_elb_length_budget_budget cf_new_b_elb_length_budget_budget cf_head_elb_length_budget_budget cf_quotient_elb_length_budget_budget. ((((exists ff_h_cf_elb_length_budget_budget_previous_state. ff_h_cf_elb_length_budget_budget_previous_state + S (((cf_old_a_elb_length_budget_budget) + (((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)))) * S ((cf_old_a_elb_length_budget_budget) + (((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)))) + ((((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget))) + (((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget))))) = S ((S (cf_index_elb_length_budget_budget)) * elb_scale_length_budget)) /\ exists ff_q_cf_elb_length_budget_budget_previous_state. elb_history_length_budget = ff_q_cf_elb_length_budget_budget_previous_state * S ((S (cf_index_elb_length_budget_budget)) * elb_scale_length_budget) + (((cf_old_a_elb_length_budget_budget) + (((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)))) * S ((cf_old_a_elb_length_budget_budget) + (((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)))) + ((((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget))) + (((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget))))))) /\ ((((exists ff_h_cf_elb_length_budget_budget_following_state. ff_h_cf_elb_length_budget_budget_following_state + S (((cf_new_a_elb_length_budget_budget) + (((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)))) * S ((cf_new_a_elb_length_budget_budget) + (((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)))) + ((((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget))) + (((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget))))) = S ((S (S cf_index_elb_length_budget_budget)) * elb_scale_length_budget)) /\ exists ff_q_cf_elb_length_budget_budget_following_state. elb_history_length_budget = ff_q_cf_elb_length_budget_budget_following_state * S ((S (S cf_index_elb_length_budget_budget)) * elb_scale_length_budget) + (((cf_new_a_elb_length_budget_budget) + (((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)))) * S ((cf_new_a_elb_length_budget_budget) + (((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)))) + ((((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget))) + (((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget))))))) /\ (cf_new_b_elb_length_budget_budget = cf_old_a_elb_length_budget_budget /\ (cf_new_a_elb_length_budget_budget = cf_new_b_elb_length_budget_budget * cf_quotient_elb_length_budget_budget + cf_old_b_elb_length_budget_budget /\ ((exists ff_lt_cf_elb_length_budget_budget_remainder. ff_lt_cf_elb_length_budget_budget_remainder + S cf_old_b_elb_length_budget_budget = cf_new_b_elb_length_budget_budget) /\ (cf_head_elb_length_budget_budget = S ((cf_quotient_elb_length_budget_budget + cf_tail_elb_length_budget_budget) * S (cf_quotient_elb_length_budget_budget + cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget + cf_tail_elb_length_budget_budget))))))))))) /\ exists elb_gap_length_budget. elb_gap_length_budget + elb_steps_length_budget = ((l + l)))
  9. 0009apply euclidean_log_trace_bound
  10. 0010exact hlength
  11. 0011cases hbounded
  12. 0012cases hbounded_witness
  13. 0013cases hbounded_witness_witness
  14. 0014cases hbounded_witness_witness_witness
  15. 0015cases hbounded_witness_witness_witness_witness
  16. 0016have hterminal : exists g. ((((exists ff_h_cf_elb_terminal_state. ff_h_cf_elb_terminal_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)) * x2)) /\ exists ff_q_cf_elb_terminal_state. x1 = ff_q_cf_elb_terminal_state * S ((S (0)) * x2) + (((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 hag_left_factor_elb_terminal. a = g * hag_left_factor_elb_terminal) /\ (exists hag_right_factor_elb_terminal. b = g * hag_right_factor_elb_terminal)) /\ forall hag_divisor_elb_terminal. (exists hag_common_left_elb_terminal. a = hag_divisor_elb_terminal * hag_common_left_elb_terminal) -> (exists hag_common_right_elb_terminal. b = hag_divisor_elb_terminal * hag_common_right_elb_terminal) -> exists hag_greatest_factor_elb_terminal. g = hag_divisor_elb_terminal * hag_greatest_factor_elb_terminal)))
  17. 0017specialize euclidean_trace_terminal_gcd_exists a
  18. 0018specialize euclidean_trace_terminal_gcd_exists b
  19. 0019specialize euclidean_trace_terminal_gcd_exists x
  20. 0020specialize euclidean_trace_terminal_gcd_exists x1
  21. 0021specialize euclidean_trace_terminal_gcd_exists x2
  22. 0022specialize euclidean_trace_terminal_gcd_exists x3
  23. 0023apply euclidean_trace_terminal_gcd_exists
  24. 0024exact hbounded_witness_witness_witness_witness_left
  25. 0025cases hterminal
  26. 0026cases hterminal_witness
  27. 0027exists x4
  28. 0028exists x3
  29. 0029split
  30. 0030exists x
  31. 0031exists x1
  32. 0032exists x2
  33. 0033split
  34. 0034exact hbounded_witness_witness_witness_witness_left
  35. 0035split
  36. 0036exact hterminal_witness_left
  37. 0037exact hterminal_witness_right
  38. 0038exact hbounded_witness_witness_witness_witness_right